:: 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;