:: Regular Expression Quantifiers -- at least $m$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received October 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem :: FLANG_3:1
for E being set
for B, A being Subset of (E ^omega) st B c= A * holds
( (A *) ^^ B c= A * & B ^^ (A *) c= A * )
proofend;

begin

:: At least n Occurences
:: Definition of |^.. n
definition
let E be set ;
let A be Subset of (E ^omega);
let n be Nat;
funcA |^.. n ->  Subset of (E ^omega) equals :: FLANG_3:def 1
 union  {  B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m &amp; B = A |^ m )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m &amp; B = A |^ m )  }  is Subset of (E ^omega)
proofend;
end;

:: deftheorem  defines |^.. FLANG_3:def_1_:_
 for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. n = union  {  B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m &amp; B = A |^ m )  }  ;

:: At least n Occurences
:: Properties of |^.. n
theorem Th2: :: FLANG_3:2
for E, x being set
for A being Subset of (E ^omega)
for n being Nat holds
( x in A |^.. n iff ex m being Nat st
( n <= m &amp; x in A |^ m ) )
proofend;

theorem Th3: :: FLANG_3:3
for E being set
for A being Subset of (E ^omega)
for n, m being Nat st n <= m holds
A |^ m c= A |^.. n
proofend;

theorem Th4: :: FLANG_3:4
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {} iff ( n > 0 &amp; A = {} ) )
proofend;

theorem Th5: :: FLANG_3:5
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
A |^.. n c= A |^.. m
proofend;

theorem Th6: :: FLANG_3:6
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat st k <= m holds
A |^ (m,n) c= A |^.. k
proofend;

theorem Th7: :: FLANG_3:7
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
proofend;

theorem :: FLANG_3:8
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
proofend;

theorem Th9: :: FLANG_3:9
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. n c= A *
proofend;

theorem Th10: :: FLANG_3:10
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
proofend;

theorem Th11: :: FLANG_3:11
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = A * iff ( <%> E in A or n = 0 ) )
proofend;

theorem :: FLANG_3:12
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))
proofend;

theorem Th13: :: FLANG_3:13
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^.. n c= B |^.. n
proofend;

theorem Th14: :: FLANG_3:14
for x, E being set
for A being Subset of (E ^omega)
for n being Nat st x in A &amp; x <> <%> E holds
A |^.. n <> {(<%> E)}
proofend;

theorem Th15: :: FLANG_3:15
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 &amp; A = {} ) ) )
proofend;

theorem Th16: :: FLANG_3:16
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
proofend;

theorem Th17: :: FLANG_3:17
for E being set
for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m
proofend;

theorem Th18: :: FLANG_3:18
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
proofend;

theorem Th19: :: FLANG_3:19
for E being set
for A being Subset of (E ^omega)
for n, m being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)
proofend;

theorem :: FLANG_3:20
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^.. n) * = (A |^.. n) ?
proofend;

theorem Th21: :: FLANG_3:21
for E being set
for A, C, B being Subset of (E ^omega)
for m, n being Nat st A c= C |^.. m &amp; B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
proofend;

theorem Th22: :: FLANG_3:22
for E being set
for A being Subset of (E ^omega)
for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
proofend;

theorem Th23: :: FLANG_3:23
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A
proofend;

theorem Th24: :: FLANG_3:24
for E being set
for A being Subset of (E ^omega)
for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
proofend;

theorem Th25: :: FLANG_3:25
for E being set
for A being Subset of (E ^omega)
for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))
proofend;

theorem :: FLANG_3:26
for E being set
for B, A being Subset of (E ^omega)
for n being Nat st <%> E in B holds
( A c= A ^^ (B |^.. n) &amp; A c= (B |^.. n) ^^ A )
proofend;

theorem Th27: :: FLANG_3:27
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
proofend;

theorem Th28: :: FLANG_3:28
for E being set
for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k &amp; n > 0 holds
A |^ n c= B |^.. k
proofend;

theorem Th29: :: FLANG_3:29
for E being set
for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k &amp; n > 0 holds
A |^.. n c= B |^.. k
proofend;

theorem Th30: :: FLANG_3:30
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1
proofend;

theorem :: FLANG_3:31
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k
proofend;

theorem Th32: :: FLANG_3:32
for E being set
for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)
proofend;

theorem Th33: :: FLANG_3:33
for E being set
for A being Subset of (E ^omega)
for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
proofend;

theorem :: FLANG_3:34
for E being set
for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A *) ^^ (A |^ (k,l)) = A |^.. k
proofend;

theorem Th35: :: FLANG_3:35
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)
proofend;

theorem :: FLANG_3:36
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
proofend;

theorem Th37: :: FLANG_3:37
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for m, n being Nat st a in C |^.. m &amp; b in C |^.. n holds
a ^ b in C |^.. (m + n)
proofend;

theorem Th38: :: FLANG_3:38
for x, E being set
for A being Subset of (E ^omega)
for k being Nat st A |^.. k = {x} holds
x = <%> E
proofend;

theorem :: FLANG_3:39
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^.. n c= B *
proofend;

theorem Th40: :: FLANG_3:40
for E being set
for A being Subset of (E ^omega)
for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
proofend;

theorem Th41: :: FLANG_3:41
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k
proofend;

theorem :: FLANG_3:42
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)
proofend;

theorem :: FLANG_3:43
for E being set
for B, A being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k &amp; B ^^ (A |^.. k) c= A |^.. k )
proofend;

theorem Th44: :: FLANG_3:44
for E being set
for A, B being Subset of (E ^omega)
for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
proofend;

theorem Th45: :: FLANG_3:45
for E being set
for A, B being Subset of (E ^omega)
for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
proofend;

theorem Th46: :: FLANG_3:46
for x, E being set
for A being Subset of (E ^omega)
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A &amp; ( <%> E in A or k <= 1 ) ) )
proofend;

theorem Th47: :: FLANG_3:47
for E being set
for A, B being Subset of (E ^omega)
for k being Nat st A c= B |^.. k holds
B |^.. k = (B \/ A) |^.. k
proofend;

begin

:: Positive Closure
:: Definition of +
definition
let E be set ;
let A be Subset of (E ^omega);
funcA +  ->  Subset of (E ^omega) equals :: FLANG_3:def 2
 union  {  B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 &amp; B = A |^ n )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 &amp; B = A |^ n )  }  is Subset of (E ^omega)
proofend;
end;

:: deftheorem  defines + FLANG_3:def_2_:_
 for E being set
for A being Subset of (E ^omega) holds A + = union  {  B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 &amp; B = A |^ n )  }  ;

:: Positive Closure
:: Properties of +
theorem Th48: :: FLANG_3:48
for E, x being set
for A being Subset of (E ^omega) holds
( x in A + iff ex n being Nat st
( n > 0 &amp; x in A |^ n ) )
proofend;

theorem Th49: :: FLANG_3:49
for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^ n c= A +
proofend;

theorem Th50: :: FLANG_3:50
for E being set
for A being Subset of (E ^omega) holds A + = A |^.. 1
proofend;

theorem :: FLANG_3:51
for E being set
for A being Subset of (E ^omega) holds
( A + = {} iff A = {} )
proofend;

theorem Th52: :: FLANG_3:52
for E being set
for A being Subset of (E ^omega) holds A + = (A *) ^^ A
proofend;

theorem Th53: :: FLANG_3:53
for E being set
for A being Subset of (E ^omega) holds A * = {(<%> E)} \/ (A +)
proofend;

theorem :: FLANG_3:54
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
proofend;

theorem Th55: :: FLANG_3:55
for E being set
for A being Subset of (E ^omega) holds A + c= A *
proofend;

theorem Th56: :: FLANG_3:56
for E being set
for A being Subset of (E ^omega) holds
( <%> E in A + iff <%> E in A )
proofend;

theorem Th57: :: FLANG_3:57
for E being set
for A being Subset of (E ^omega) holds
( A + = A * iff <%> E in A )
proofend;

theorem Th58: :: FLANG_3:58
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A + c= B +
proofend;

theorem Th59: :: FLANG_3:59
for E being set
for A being Subset of (E ^omega) holds A c= A +
proofend;

theorem Th60: :: FLANG_3:60
for E being set
for A being Subset of (E ^omega) holds
( (A *) + = A * &amp; (A +) * = A * )
proofend;

theorem Th61: :: FLANG_3:61
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A + c= B *
proofend;

theorem :: FLANG_3:62
for E being set
for A being Subset of (E ^omega) holds (A +) + = A +
proofend;

theorem :: FLANG_3:63
for x, E being set
for A being Subset of (E ^omega) st x in A &amp; x <> <%> E holds
A + <> {(<%> E)}
proofend;

theorem :: FLANG_3:64
for E being set
for A being Subset of (E ^omega) holds
( A + = {(<%> E)} iff A = {(<%> E)} )
proofend;

theorem :: FLANG_3:65
for E being set
for A being Subset of (E ^omega) holds
( (A +) ? = A * &amp; (A ?) + = A * )
proofend;

theorem Th66: :: FLANG_3:66
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C + &amp; b in C + holds
a ^ b in C +
proofend;

theorem :: FLANG_3:67
for E being set
for A, C, B being Subset of (E ^omega) st A c= C + &amp; B c= C + holds
A ^^ B c= C +
proofend;

theorem :: FLANG_3:68
for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A +
proofend;

theorem :: FLANG_3:69
for x, E being set
for A being Subset of (E ^omega) st A + = {x} holds
x = <%> E
proofend;

theorem :: FLANG_3:70
for E being set
for A being Subset of (E ^omega) holds A ^^ (A +) = (A +) ^^ A
proofend;

theorem :: FLANG_3:71
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k)
proofend;

theorem Th72: :: FLANG_3:72
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A +) = (A +) ^^ (A |^ (m,n))
proofend;

theorem :: FLANG_3:73
for E being set
for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) &amp; A c= (B +) ^^ A )
proofend;

theorem :: FLANG_3:74
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2
proofend;

theorem Th75: :: FLANG_3:75
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1)
proofend;

theorem :: FLANG_3:76
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2
proofend;

theorem :: FLANG_3:77
for E being set
for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)
proofend;

theorem :: FLANG_3:78
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + &amp; n > 0 holds
A |^ n c= B +
proofend;

theorem :: FLANG_3:79
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = (A ?) ^^ (A +)
proofend;

theorem :: FLANG_3:80
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = A +
proofend;

theorem :: FLANG_3:81
for E being set
for A being Subset of (E ^omega) holds
( A ? c= A + iff <%> E in A )
proofend;

theorem :: FLANG_3:82
for E being set
for A, B being Subset of (E ^omega) st A c= B + holds
A + c= B +
proofend;

theorem :: FLANG_3:83
for E being set
for A, B being Subset of (E ^omega) st A c= B + holds
B + = (B \/ A) +
proofend;

theorem :: FLANG_3:84
for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^.. n c= A +
proofend;

theorem :: FLANG_3:85
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m > 0 holds
A |^ (m,n) c= A +
proofend;

theorem Th86: :: FLANG_3:86
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A +) = (A +) ^^ (A *)
proofend;

theorem Th87: :: FLANG_3:87
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) |^ k c= A |^.. k
proofend;

theorem :: FLANG_3:88
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m
proofend;

theorem :: FLANG_3:89
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + &amp; n > 0 holds
A |^.. n c= B +
proofend;

theorem Th90: :: FLANG_3:90
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1)
proofend;

theorem :: FLANG_3:91
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = (A |^.. k) ^^ (A +)
proofend;

theorem Th92: :: FLANG_3:92
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A *) = A +
proofend;

theorem :: FLANG_3:93
for E being set
for B, A being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + &amp; B ^^ (A +) c= A + )
proofend;

theorem :: FLANG_3:94
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +)
proofend;

theorem :: FLANG_3:95
for E being set
for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) +
proofend;

theorem :: FLANG_3:96
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A + iff <%x%> in A )
proofend;