:: Regular Expression Quantifiers -- \$m\$ to \$n\$ Occurrences :: by Micha{\l} Trybulec :: :: Received June 6, 2007 :: Copyright (c) 2007-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, CARD_1, ORDINAL4, XBOOLE_0, FINSEQ_1, PRE_POLY, NEWTON, TARSKI, RELAT_1, SETFAM_1, MODAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, SETFAM_1, XXREAL_0, AFINSQ_1, FLANG_1; constructors NAT_1, XREAL_0, FLANG_1; registrations SUBSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0, XXREAL_0, FUNCT_1, RELAT_1, FINSET_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve E, x, y, X for set; reserve A, B, C for Subset of E^omega; reserve a, b for Element of E^omega; reserve i, k, l, kl, m, n, mn for Nat; :: Preliminaries - Numbers: theorem :: FLANG_2:1 m + k <= i & i <= n + k implies ex mn st mn + k = i & m <= mn & mn <= n; theorem :: FLANG_2:2 m <= n & k <= l & m + k <= i & i <= n + l implies ex mn, kl st mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l; theorem :: FLANG_2:3 m < n implies ex k st m + k = n & k > 0; :: Preliminaries - Sequences: theorem :: FLANG_2:4 a ^ b = a or b ^ a = a implies b = {}; begin :: Addenda - FLANG_1: theorem :: FLANG_2:5 (x in A or x in B) & x <> <%>E implies A ^^ B <> {<%>E}; theorem :: FLANG_2:6 <%x%> in A ^^ B iff <%>E in A & <%x%> in B or <%x%> in A & <%>E in B; theorem :: FLANG_2:7 x in A & x <> <%>E & n > 0 implies A |^ n <> {<%>E}; theorem :: FLANG_2:8 <%>E in A |^ n iff n = 0 or <%>E in A; theorem :: FLANG_2:9 <%x%> in A |^ n iff <%x%> in A & ( <%>E in A & n > 1 or n = 1); theorem :: FLANG_2:10 m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E; theorem :: FLANG_2:11 (A |^ m) |^ n = (A |^ n) |^ m; theorem :: FLANG_2:12 (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m); theorem :: FLANG_2:13 <%>E in B implies A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A; theorem :: FLANG_2:14 A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l); theorem :: FLANG_2:15 x in A & x <> <%>E implies A* <> {<%>E}; theorem :: FLANG_2:16 <%>E in A & n > 0 implies (A |^ n)* = A*; theorem :: FLANG_2:17 <%>E in A implies (A |^ n)* = (A*) |^ n; theorem :: FLANG_2:18 A c= A ^^ (B*) & A c= (B*) ^^ A; begin :: Union of a Range of Powers :: Definition of |^ (n, m) definition let E, A; let m, n; func A |^ (m, n) -> Subset of E^omega equals :: FLANG_2:def 1 union { B: ex k st m <= k & k <= n & B = A |^ k }; end; :: Union of a Range of Powers :: Properties of |^ (n, m) theorem :: FLANG_2:19 x in A |^ (m, n) iff ex k st m <= k & k <= n & x in A |^ k; theorem :: FLANG_2:20 m <= k & k <= n implies A |^ k c= A |^ (m, n); theorem :: FLANG_2:21 A |^ (m, n) = {} iff m > n or m > 0 & A = {}; theorem :: FLANG_2:22 A |^ (m, m) = A |^ m; theorem :: FLANG_2:23 m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n); theorem :: FLANG_2:24 m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n); theorem :: FLANG_2:25 m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1 , n); theorem :: FLANG_2:26 m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1 )); theorem :: FLANG_2:27 m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n); theorem :: FLANG_2:28 A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1); theorem :: FLANG_2:29 A c= B implies A |^ (m, n) c= B |^ (m, n); theorem :: FLANG_2:30 x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> { <%>E}; theorem :: FLANG_2:31 A |^ (m, n) = {<%>E} iff m <= n & A = {<%>E} or m = 0 & n = 0 or m = 0 & A = {}; theorem :: FLANG_2:32 A |^ (m, n) c= A*; theorem :: FLANG_2:33 <%>E in A |^ (m, n) iff m = 0 or m <= n & <%>E in A; theorem :: FLANG_2:34 <%>E in A & m <= n implies A |^ (m, n) = A |^ n; theorem :: FLANG_2:35 A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n)); theorem :: FLANG_2:36 (A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n)); theorem :: FLANG_2:37 m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l); theorem :: FLANG_2:38 A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A; theorem :: FLANG_2:39 (A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n)); theorem :: FLANG_2:40 (A |^ (m, n)) |^ k = A |^ (m * k, n * k); theorem :: FLANG_2:41 (A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n) ); theorem :: FLANG_2:42 (A |^ k) |^ (m, n) c= A |^ (k * m, k * n); theorem :: FLANG_2:43 (A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k; theorem :: FLANG_2:44 (A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n )); theorem :: FLANG_2:45 A |^ (0, 0) = {<%>E}; theorem :: FLANG_2:46 A |^ (0, 1) = {<%>E} \/ A; theorem :: FLANG_2:47 A |^ (1, 1) = A; theorem :: FLANG_2:48 A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A); theorem :: FLANG_2:49 A |^ (1, 2) = A \/ (A ^^ A); theorem :: FLANG_2:50 A |^ (2, 2) = A ^^ A; theorem :: FLANG_2:51 m > 0 & A |^ (m, n) = {x} implies for mn st m <= mn & mn <= n holds A |^ mn = {x}; theorem :: FLANG_2:52 m <> n & A |^ (m, n) = {x} implies x = <%>E; theorem :: FLANG_2:53 <%x%> in A |^ (m, n) iff <%x%> in A & m <= n & ( <%>E in A & n > 0 or m <= 1 & 1 <= n ); theorem :: FLANG_2:54 (A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n)); theorem :: FLANG_2:55 (A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n); theorem :: FLANG_2:56 (A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l); theorem :: FLANG_2:57 m <= n & <%>E in B implies A c= A ^^ (B |^ (m, n)) & A c= (B |^ (m, n) ) ^^ A ; theorem :: FLANG_2:58 m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l) implies A ^^ B c= C |^ (m + k, n + l); theorem :: FLANG_2:59 (A |^ (m, n))* c= A*; theorem :: FLANG_2:60 (A*) |^ (m, n) c= A*; theorem :: FLANG_2:61 m <= n & n > 0 implies (A*) |^ (m, n) = A*; theorem :: FLANG_2:62 m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*; theorem :: FLANG_2:63 m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n); theorem :: FLANG_2:64 A c= B* implies A |^ (m, n) c= B*; theorem :: FLANG_2:65 A c= B* implies B* = (B \/ (A |^ (m, n)))*; theorem :: FLANG_2:66 A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n)); theorem :: FLANG_2:67 <%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n)); theorem :: FLANG_2:68 A |^ (m, n) |^ k c= A*; theorem :: FLANG_2:69 A |^ k |^ (m, n) c= A*; theorem :: FLANG_2:70 m <= n implies (A |^ m)* c= (A |^ (m, n))*; theorem :: FLANG_2:71 (A |^ (m, n)) |^ (k, l) c= A*; theorem :: FLANG_2:72 <%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n); begin :: Optional Occurrence :: Definition of ? definition let E, A; func A? -> Subset of E^omega equals :: FLANG_2:def 2 union { B: ex k st k <= 1 & B = A |^ k }; end; :: Optional Occurrence :: Properties of ? theorem :: FLANG_2:73 x in A? iff ex k st k <= 1 & x in A |^ k; theorem :: FLANG_2:74 n <= 1 implies A |^ n c= A?; theorem :: FLANG_2:75 A? = (A |^ 0) \/ (A |^ 1); theorem :: FLANG_2:76 A? = {<%>E} \/ A; theorem :: FLANG_2:77 A c= A?; theorem :: FLANG_2:78 x in A? iff x = <%>E or x in A; theorem :: FLANG_2:79 A? = A |^ (0, 1); theorem :: FLANG_2:80 A? = A iff <%>E in A; registration let E, A; cluster A? -> non empty; end; theorem :: FLANG_2:81 A?? = A?; theorem :: FLANG_2:82 A c= B implies A? c= B?; theorem :: FLANG_2:83 x in A & x <> <%>E implies A? <> {<%>E}; theorem :: FLANG_2:84 A? = {<%>E} iff A = {} or A = {<%>E}; theorem :: FLANG_2:85 (A*)? = A* & (A?)* = A*; theorem :: FLANG_2:86 A? c= A*; theorem :: FLANG_2:87 (A /\ B)? = (A?) /\ (B?); theorem :: FLANG_2:88 (A?) \/ (B?) = (A \/ B)?; theorem :: FLANG_2:89 A? = {x} implies x = <%>E; theorem :: FLANG_2:90 <%x%> in A? iff <%x%> in A; theorem :: FLANG_2:91 (A?) ^^ A = A ^^ (A?); theorem :: FLANG_2:92 (A?) ^^ A = A |^ (1, 2); theorem :: FLANG_2:93 (A?) ^^ (A?) = A |^ (0, 2); theorem :: FLANG_2:94 (A?) |^ k = (A?) |^ (0, k); theorem :: FLANG_2:95 (A?) |^ k = A |^ (0, k); theorem :: FLANG_2:96 m <= n implies A? |^ (m, n) = A? |^ (0, n); theorem :: FLANG_2:97 A? |^ (0, n) = A |^ (0, n); theorem :: FLANG_2:98 m <= n implies A? |^ (m, n) = A |^ (0, n); theorem :: FLANG_2:99 (A |^ (1, n))? = A |^ (0, n); theorem :: FLANG_2:100 <%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A; theorem :: FLANG_2:101 A c= A ^^ (B?) & A c= (B?) ^^ A; theorem :: FLANG_2:102 A c= C? & B c= C? implies A ^^ B c= C |^ (0, 2); theorem :: FLANG_2:103 <%>E in A & n > 0 implies A? c= A |^ n; theorem :: FLANG_2:104 (A?) ^^ (A |^ k) = (A |^ k) ^^ (A?); theorem :: FLANG_2:105 A c= B* implies A? c= B*; theorem :: FLANG_2:106 A c= B* implies B* = (B \/ (A?))*; theorem :: FLANG_2:107 A? ^^ (A*) = A* ^^ (A?); theorem :: FLANG_2:108 A? ^^ (A*) = A*; theorem :: FLANG_2:109 A? |^ k c= A*; theorem :: FLANG_2:110 (A |^ k)? c= A*; theorem :: FLANG_2:111 (A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?); theorem :: FLANG_2:112 (A?) ^^ (A |^ k) = A |^ (k, k + 1); theorem :: FLANG_2:113 A? |^ (m, n) c= A*; theorem :: FLANG_2:114 (A |^ (m, n))? c= A*; theorem :: FLANG_2:115 A? = (A \ {<%>E})?; theorem :: FLANG_2:116 A c= B? implies A? c= B?; theorem :: FLANG_2:117 A c= B? implies B? = (B \/ A)?;