:: Regular Expression Quantifiers -- at least \$m\$ Occurrences :: by Micha{\l} Trybulec :: :: Received October 9, 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, TARSKI, RELAT_1, PRE_POLY, XXREAL_0, NEWTON, SETFAM_1, XBOOLE_0, CARD_1, ARYTM_3, ORDINAL4, MODAL_1, FLANG_3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, SETFAM_1, XXREAL_0, AFINSQ_1, FLANG_1, FLANG_2; constructors NAT_1, XREAL_0, FLANG_1, FLANG_2; registrations SUBSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0; 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, a1, a2, b for Element of E^omega; reserve i, k, l, m, n for Nat; theorem :: FLANG_3:1 B c= A* implies A* ^^ B c= A* & B ^^ (A*) c= A*; begin :: At least n Occurences :: Definition of |^.. n definition let E, A, n; func A |^.. n -> Subset of E^omega equals :: FLANG_3:def 1 union { B: ex m st n <= m & B = A |^ m }; end; :: At least n Occurences :: Properties of |^.. n theorem :: FLANG_3:2 x in A |^.. n iff ex m st n <= m & x in A |^ m; theorem :: FLANG_3:3 n <= m implies A |^ m c= A |^.. n; theorem :: FLANG_3:4 A |^.. n = {} iff n > 0 & A = {}; theorem :: FLANG_3:5 m <= n implies A |^.. n c= A |^.. m; theorem :: FLANG_3:6 k <= m implies A |^ (m, n) c= A |^.. k; theorem :: FLANG_3:7 m <= n + 1 implies A |^ (m, n) \/ A |^.. (n + 1) = A |^.. m; theorem :: FLANG_3:8 A |^ n \/ A |^.. (n + 1) = A |^.. n; theorem :: FLANG_3:9 A |^.. n c= A*; theorem :: FLANG_3:10 <%>E in A |^.. n iff n = 0 or <%>E in A; theorem :: FLANG_3:11 A |^.. n = A* iff <%>E in A or n = 0; theorem :: FLANG_3:12 A* = A |^ (0, n) \/ A |^.. (n + 1); theorem :: FLANG_3:13 A c= B implies A |^.. n c= B |^.. n; theorem :: FLANG_3:14 x in A & x <> <%>E implies A |^.. n <> {<%>E}; theorem :: FLANG_3:15 A |^.. n = {<%>E} iff A = {<%>E} or n = 0 & A = {}; theorem :: FLANG_3:16 A |^.. (n + 1) = (A |^.. n) ^^ A; theorem :: FLANG_3:17 (A |^.. m) ^^ (A*) = A |^.. m; theorem :: FLANG_3:18 (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n); theorem :: FLANG_3:19 n > 0 implies (A |^.. m) |^ n = A |^.. (m * n); theorem :: FLANG_3:20 (A |^.. n)* = (A |^.. n)?; theorem :: FLANG_3:21 A c= C |^.. m & B c= C |^.. n implies A ^^ B c= C |^.. (m + n); theorem :: FLANG_3:22 A |^.. (n + k) = (A |^.. n) ^^ (A |^ k); theorem :: FLANG_3:23 A ^^ (A |^.. n) = (A |^.. n) ^^ A; theorem :: FLANG_3:24 (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k); theorem :: FLANG_3:25 (A |^ (k, l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k, l)); theorem :: FLANG_3:26 <%>E in B implies A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A; theorem :: FLANG_3:27 (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m); theorem :: FLANG_3:28 A c= B |^.. k & n > 0 implies A |^ n c= B |^.. k; theorem :: FLANG_3:29 A c= B |^.. k & n > 0 implies A |^.. n c= B |^.. k; theorem :: FLANG_3:30 A* ^^ A = A |^.. 1; theorem :: FLANG_3:31 A* ^^ (A |^ k) = A |^.. k; theorem :: FLANG_3:32 (A |^.. m) ^^ (A*) = A* ^^ (A |^.. m); theorem :: FLANG_3:33 k <= l implies (A |^.. n) ^^ (A |^ (k, l)) = A |^.. (n + k); theorem :: FLANG_3:34 k <= l implies A* ^^ (A |^ (k, l)) = A |^.. k; theorem :: FLANG_3:35 (A |^ m) |^.. n c= A |^.. (m * n); theorem :: FLANG_3:36 (A |^ m) |^.. n c= (A |^.. n) |^ m; theorem :: FLANG_3:37 a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n); theorem :: FLANG_3:38 A |^.. k = {x} implies x = <%>E; theorem :: FLANG_3:39 A c= B* implies A |^.. n c= B*; theorem :: FLANG_3:40 A? c= A |^.. k iff k = 0 or <%>E in A; theorem :: FLANG_3:41 A |^.. k ^^ (A?) = A |^.. k; theorem :: FLANG_3:42 A |^.. k ^^ (A?) = A? ^^ (A |^.. k); theorem :: FLANG_3:43 B c= A* implies A |^.. k ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k; theorem :: FLANG_3:44 (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k); theorem :: FLANG_3:45 (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k; theorem :: FLANG_3:46 <%x%> in A |^.. k iff <%x%> in A & (<%>E in A or k <= 1); theorem :: FLANG_3:47 A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k; begin :: Positive Closure :: Definition of + definition let E, A; func A+ -> Subset of E^omega equals :: FLANG_3:def 2 union { B: ex n st n > 0 & B = A |^ n }; end; :: Positive Closure :: Properties of + theorem :: FLANG_3:48 x in A+ iff ex n st n > 0 & x in A |^ n; theorem :: FLANG_3:49 n > 0 implies A |^ n c= A+; theorem :: FLANG_3:50 A+ = A |^.. 1; theorem :: FLANG_3:51 A+ = {} iff A = {}; theorem :: FLANG_3:52 A+ = (A*) ^^ A; theorem :: FLANG_3:53 A* = {<%>E} \/ (A+); theorem :: FLANG_3:54 A+ = A |^ (1, n) \/ A |^.. (n + 1); theorem :: FLANG_3:55 A+ c= A*; theorem :: FLANG_3:56 <%>E in A+ iff <%>E in A; theorem :: FLANG_3:57 A+ = A* iff <%>E in A; theorem :: FLANG_3:58 A c= B implies A+ c= B+; theorem :: FLANG_3:59 A c= A+; theorem :: FLANG_3:60 (A*)+ = A* & (A+)* = A*; theorem :: FLANG_3:61 A c= B* implies A+ c= B*; theorem :: FLANG_3:62 (A+)+ = A+; theorem :: FLANG_3:63 x in A & x <> <%>E implies A+ <> {<%>E}; theorem :: FLANG_3:64 A+ = {<%>E} iff A = {<%>E}; theorem :: FLANG_3:65 (A+)? = A* & (A?)+ = A*; theorem :: FLANG_3:66 a in C+ & b in C+ implies a ^ b in C+; theorem :: FLANG_3:67 A c= C+ & B c= C+ implies A ^^ B c= C+; theorem :: FLANG_3:68 A ^^ A c= A+; theorem :: FLANG_3:69 A+ = {x} implies x = <%>E; theorem :: FLANG_3:70 A ^^ (A+) = (A+) ^^ A; theorem :: FLANG_3:71 (A |^ k) ^^ (A+) = (A+) ^^ (A |^ k); theorem :: FLANG_3:72 (A |^ (m, n)) ^^ (A+) = A+ ^^ (A |^ (m, n)); theorem :: FLANG_3:73 <%>E in B implies A c= A ^^ (B+) & A c= (B+) ^^ A; theorem :: FLANG_3:74 A+ ^^ (A+) = A |^.. 2; theorem :: FLANG_3:75 A+ ^^ (A |^ k) = A |^.. (k + 1); theorem :: FLANG_3:76 A+ ^^ A = A |^.. 2; theorem :: FLANG_3:77 k <= l implies A+ ^^ (A |^ (k, l)) = A |^.. (k + 1); theorem :: FLANG_3:78 A c= B+ & n > 0 implies A |^ n c= B+; theorem :: FLANG_3:79 A+ ^^ (A?) = A? ^^ (A+); theorem :: FLANG_3:80 A+ ^^ (A?) = A+; theorem :: FLANG_3:81 A? c= A+ iff <%>E in A; theorem :: FLANG_3:82 A c= B+ implies A+ c= B+; theorem :: FLANG_3:83 A c= B+ implies B+ = (B \/ A)+; theorem :: FLANG_3:84 n > 0 implies A |^.. n c= A+; theorem :: FLANG_3:85 m > 0 implies A |^ (m, n) c= A+; theorem :: FLANG_3:86 A* ^^ (A+) = A+ ^^ (A*); theorem :: FLANG_3:87 A+ |^ k c= A |^.. k; theorem :: FLANG_3:88 A+ |^ (m, n) c= A |^.. m; theorem :: FLANG_3:89 A c= B+ & n > 0 implies A |^.. n c= B+; theorem :: FLANG_3:90 A+ ^^ (A |^.. k) = A |^.. (k + 1); theorem :: FLANG_3:91 A+ ^^ (A |^.. k) = A |^.. k ^^ (A+); theorem :: FLANG_3:92 A+ ^^ (A*) = A+; theorem :: FLANG_3:93 B c= A* implies A+ ^^ B c= A+ & B ^^ (A+) c= A+; theorem :: FLANG_3:94 (A /\ B)+ c= (A+) /\ (B+); theorem :: FLANG_3:95 (A+) \/ (B+) c= (A \/ B)+; theorem :: FLANG_3:96 <%x%> in A+ iff <%x%> in A;