:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


:: Preliminaries - Numbers:
theorem Th1: :: FLANG_2:1
for i, k, m, n being Nat st m + k <= i & i <= n + k holds
ex mn being Nat st
( mn + k = i & m <= mn & mn <= n )
proof end;

theorem Th2: :: FLANG_2:2
for i, k, l, m, n being Nat st m <= n & k <= l & m + k <= i & i <= n + l holds
ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
proof end;

theorem Th3: :: FLANG_2:3
for m, n being Nat st m < n holds
ex k being Nat st
( m + k = n & k > 0 )
proof end;

:: Preliminaries - Sequences:
theorem Th4: :: FLANG_2:4
for E being set
for a, b being Element of E ^omega st ( a ^ b = a or b ^ a = a ) holds
b = {}
proof end;

:: Addenda - FLANG_1:
theorem :: FLANG_2:5
for E, x being set
for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds
A ^^ B <> {(<%> E)}
proof end;

theorem :: FLANG_2:6
for E, x being set
for A, B being Subset of (E ^omega) holds
( <%x%> in A ^^ B iff ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )
proof end;

theorem Th7: :: FLANG_2:7
for E, x being set
for A being Subset of (E ^omega)
for n being Nat st x in A & x <> <%> E & n > 0 holds
A |^ n <> {(<%> E)}
proof end;

theorem :: FLANG_2:8
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 ) )
proof end;

theorem Th9: :: FLANG_2:9
for E, x being set
for A being Subset of (E ^omega)
for n being Nat holds
( <%x%> in A |^ n iff ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) )
proof end;

theorem Th10: :: FLANG_2:10
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
proof end;

theorem :: FLANG_2:11
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
proof end;

theorem Th12: :: FLANG_2:12
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)
proof end;

theorem :: FLANG_2:13
for E being set
for A, B being Subset of (E ^omega)
for l being Nat st <%> E in B holds
( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )
proof end;

theorem :: FLANG_2:14
for E being set
for A, B, C being Subset of (E ^omega)
for k, l being Nat st A c= C |^ k & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
proof end;

theorem :: FLANG_2:15
for E, x being set
for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A * <> {(<%> E)}
proof end;

theorem Th16: :: FLANG_2:16
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
(A |^ n) * = A *
proof end;

theorem Th17: :: FLANG_2:17
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
(A |^ n) * = (A *) |^ n
proof end;

theorem :: FLANG_2:18
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B *) & A c= (B *) ^^ A )
proof end;

:: Union of a Range of Powers
:: Definition of |^ (n, m)
definition
let E be set ;
let A be Subset of (E ^omega);
let m, n be Nat;
func A |^ (m,n) -> Subset of (E ^omega) equals :: FLANG_2:def 1
union { B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )
}
;
coherence
union { B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )
}
is Subset of (E ^omega)
proof end;
end;

:: deftheorem defines |^ FLANG_2:def 1 :
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) = union { B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )
}
;

:: Union of a Range of Powers
:: Properties of |^ (n, m)
theorem Th19: :: FLANG_2:19
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( x in A |^ (m,n) iff ex k being Nat st
( m <= k & k <= n & x in A |^ k ) )
proof end;

theorem Th20: :: FLANG_2:20
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat st m <= k & k <= n holds
A |^ k c= A |^ (m,n) by Th19;

theorem Th21: :: FLANG_2:21
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
proof end;

theorem Th22: :: FLANG_2:22
for E being set
for A being Subset of (E ^omega)
for m being Nat holds A |^ (m,m) = A |^ m
proof end;

theorem Th23: :: FLANG_2:23
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat st m <= k & l <= n holds
A |^ (k,l) c= A |^ (m,n)
proof end;

theorem :: FLANG_2:24
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
proof end;

theorem Th25: :: FLANG_2:25
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
proof end;

theorem Th26: :: FLANG_2:26
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
proof end;

theorem :: FLANG_2:27
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
proof end;

theorem Th28: :: FLANG_2:28
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))
proof end;

theorem Th29: :: FLANG_2:29
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B holds
A |^ (m,n) c= B |^ (m,n)
proof end;

theorem Th30: :: FLANG_2:30
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st x in A & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ (m,n) <> {(<%> E)}
proof end;

theorem Th31: :: FLANG_2:31
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {(<%> E)} iff ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) )
proof end;

theorem Th32: :: FLANG_2:32
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) c= A *
proof end;

theorem Th33: :: FLANG_2:33
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
proof end;

theorem Th34: :: FLANG_2:34
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A |^ (m,n) = A |^ n
proof end;

theorem Th35: :: FLANG_2:35
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))
proof end;

theorem Th36: :: FLANG_2:36
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))
proof end;

theorem Th37: :: FLANG_2:37
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
proof end;

theorem Th38: :: FLANG_2:38
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
proof end;

theorem Th39: :: FLANG_2:39
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
proof end;

theorem Th40: :: FLANG_2:40
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
proof end;

theorem Th41: :: FLANG_2:41
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (k + 1)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n))
proof end;

theorem Th42: :: FLANG_2:42
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
proof end;

theorem :: FLANG_2:43
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
proof end;

theorem :: FLANG_2:44
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (k + l)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n))
proof end;

theorem Th45: :: FLANG_2:45
for E being set
for A being Subset of (E ^omega) holds A |^ (0,0) = {(<%> E)}
proof end;

theorem Th46: :: FLANG_2:46
for E being set
for A being Subset of (E ^omega) holds A |^ (0,1) = {(<%> E)} \/ A
proof end;

theorem :: FLANG_2:47
for E being set
for A being Subset of (E ^omega) holds A |^ (1,1) = A
proof end;

theorem :: FLANG_2:48
for E being set
for A being Subset of (E ^omega) holds A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
proof end;

theorem :: FLANG_2:49
for E being set
for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)
proof end;

theorem :: FLANG_2:50
for E being set
for A being Subset of (E ^omega) holds A |^ (2,2) = A ^^ A
proof end;

theorem Th51: :: FLANG_2:51
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m > 0 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
proof end;

theorem Th52: :: FLANG_2:52
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ (m,n) = {x} holds
x = <%> E
proof end;

theorem Th53: :: FLANG_2:53
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( <%x%> in A |^ (m,n) iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
proof end;

theorem :: FLANG_2:54
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat holds (A /\ B) |^ (m,n) c= (A |^ (m,n)) /\ (B |^ (m,n))
proof end;

theorem :: FLANG_2:55
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) \/ (B |^ (m,n)) c= (A \/ B) |^ (m,n)
proof end;

theorem :: FLANG_2:56
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
proof end;

theorem :: FLANG_2:57
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in B holds
( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A )
proof end;

theorem :: FLANG_2:58
for E being set
for A, B, C being Subset of (E ^omega)
for k, l, m, n being Nat st m <= n & k <= l & A c= C |^ (m,n) & B c= C |^ (k,l) holds
A ^^ B c= C |^ ((m + k),(n + l))
proof end;

theorem :: FLANG_2:59
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) * c= A *
proof end;

theorem :: FLANG_2:60
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A *) |^ (m,n) c= A *
proof end;

theorem :: FLANG_2:61
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 holds
(A *) |^ (m,n) = A *
proof end;

theorem :: FLANG_2:62
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 & <%> E in A holds
(A |^ (m,n)) * = A *
proof end;

theorem :: FLANG_2:63
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in A holds
(A |^ (m,n)) * = (A *) |^ (m,n)
proof end;

theorem Th64: :: FLANG_2:64
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B * holds
A |^ (m,n) c= B *
proof end;

theorem :: FLANG_2:65
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B * holds
B * = (B \/ (A |^ (m,n))) * by Th64, FLANG_1:67;

theorem Th66: :: FLANG_2:66
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))
proof end;

theorem :: FLANG_2:67
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A * = (A *) ^^ (A |^ (m,n))
proof end;

theorem :: FLANG_2:68
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (m,n)) |^ k c= A * by Th32, FLANG_1:59;

theorem Th69: :: FLANG_2:69
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
proof end;

theorem :: FLANG_2:70
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A |^ m) * c= (A |^ (m,n)) * by Th20, FLANG_1:61;

theorem Th71: :: FLANG_2:71
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
proof end;

theorem Th72: :: FLANG_2:72
for E being set
for A being Subset of (E ^omega)
for k, l, n being Nat st <%> E in A & k <= n & l <= n holds
A |^ (k,n) = A |^ (l,n)
proof end;

:: Optional Occurrence
:: Definition of ?
definition
let E be set ;
let A be Subset of (E ^omega);
func A ? -> Subset of (E ^omega) equals :: FLANG_2:def 2
union { B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k )
}
;
coherence
union { B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k )
}
is Subset of (E ^omega)
proof end;
end;

:: deftheorem defines ? FLANG_2: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 k being Nat st
( k <= 1 & B = A |^ k )
}
;

:: Optional Occurrence
:: Properties of ?
theorem Th73: :: FLANG_2:73
for E, x being set
for A being Subset of (E ^omega) holds
( x in A ? iff ex k being Nat st
( k <= 1 & x in A |^ k ) )
proof end;

theorem :: FLANG_2:74
for E being set
for A being Subset of (E ^omega)
for n being Nat st n <= 1 holds
A |^ n c= A ? by Th73;

theorem Th75: :: FLANG_2:75
for E being set
for A being Subset of (E ^omega) holds A ? = (A |^ 0) \/ (A |^ 1)
proof end;

theorem Th76: :: FLANG_2:76
for E being set
for A being Subset of (E ^omega) holds A ? = {(<%> E)} \/ A
proof end;

theorem :: FLANG_2:77
for E being set
for A being Subset of (E ^omega) holds A c= A ?
proof end;

theorem Th78: :: FLANG_2:78
for E, x being set
for A being Subset of (E ^omega) holds
( x in A ? iff ( x = <%> E or x in A ) )
proof end;

theorem Th79: :: FLANG_2:79
for E being set
for A being Subset of (E ^omega) holds A ? = A |^ (0,1)
proof end;

theorem Th80: :: FLANG_2:80
for E being set
for A being Subset of (E ^omega) holds
( A ? = A iff <%> E in A )
proof end;

registration
let E be set ;
let A be Subset of (E ^omega);
cluster A ? -> non empty ;
coherence
not A ? is empty
proof end;
end;

theorem :: FLANG_2:81
for E being set
for A being Subset of (E ^omega) holds (A ?) ? = A ?
proof end;

theorem :: FLANG_2:82
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A ? c= B ?
proof end;

theorem :: FLANG_2:83
for E, x being set
for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A ? <> {(<%> E)}
proof end;

theorem :: FLANG_2:84
for E being set
for A being Subset of (E ^omega) holds
( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
proof end;

theorem :: FLANG_2:85
for E being set
for A being Subset of (E ^omega) holds
( (A *) ? = A * & (A ?) * = A * )
proof end;

theorem :: FLANG_2:86
for E being set
for A being Subset of (E ^omega) holds A ? c= A *
proof end;

theorem :: FLANG_2:87
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) ? = (A ?) /\ (B ?)
proof end;

theorem :: FLANG_2:88
for E being set
for A, B being Subset of (E ^omega) holds (A ?) \/ (B ?) = (A \/ B) ?
proof end;

theorem :: FLANG_2:89
for E, x being set
for A being Subset of (E ^omega) st A ? = {x} holds
x = <%> E
proof end;

theorem :: FLANG_2:90
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A ? iff <%x%> in A )
proof end;

theorem :: FLANG_2:91
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A ^^ (A ?)
proof end;

theorem :: FLANG_2:92
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A |^ (1,2)
proof end;

theorem Th93: :: FLANG_2:93
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A ?) = A |^ (0,2)
proof end;

theorem Th94: :: FLANG_2:94
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
proof end;

theorem Th95: :: FLANG_2:95
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = A |^ (0,k)
proof end;

theorem Th96: :: FLANG_2:96
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = (A ?) |^ (0,n)
proof end;

theorem Th97: :: FLANG_2:97
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A ?) |^ (0,n) = A |^ (0,n)
proof end;

theorem Th98: :: FLANG_2:98
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = A |^ (0,n)
proof end;

theorem :: FLANG_2:99
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ (1,n)) ? = A |^ (0,n)
proof end;

theorem :: FLANG_2:100
for E being set
for A, B being Subset of (E ^omega) st <%> E in A & <%> E in B holds
( A ? c= A ^^ B & A ? c= B ^^ A )
proof end;

theorem :: FLANG_2:101
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B ?) & A c= (B ?) ^^ A )
proof end;

theorem :: FLANG_2:102
for E being set
for A, B, C being Subset of (E ^omega) st A c= C ? & B c= C ? holds
A ^^ B c= C |^ (0,2)
proof end;

theorem :: FLANG_2:103
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
proof end;

theorem :: FLANG_2:104
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)
proof end;

theorem Th105: :: FLANG_2:105
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A ? c= B *
proof end;

theorem :: FLANG_2:106
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ (A ?)) * by Th105, FLANG_1:67;

theorem :: FLANG_2:107
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = (A *) ^^ (A ?)
proof end;

theorem :: FLANG_2:108
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = A *
proof end;

theorem :: FLANG_2:109
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k c= A *
proof end;

theorem :: FLANG_2:110
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ? c= A *
proof end;

theorem :: FLANG_2:111
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
proof end;

theorem :: FLANG_2:112
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
proof end;

theorem :: FLANG_2:113
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) |^ (m,n) c= A *
proof end;

theorem :: FLANG_2:114
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ? c= A *
proof end;

theorem :: FLANG_2:115
for E being set
for A being Subset of (E ^omega) holds A ? = (A \ {(<%> E)}) ?
proof end;

theorem :: FLANG_2:116
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
A ? c= B ?
proof end;

theorem :: FLANG_2:117
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
B ? = (B \/ A) ?
proof end;