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

theorem :: FLANG_3:1

for E being set
for A, B being Subset of (E ^omega) st B c= A * holds
( (A *) ^^ B c= A * & B ^^ (A *) c= A * )

proof end;

:: At least n Occurences
:: Definition of |^.. n

definition

let E be set ;
let A be Subset of (E ^omega);
let n be Nat;

func A |^.. 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 & B = A |^ m ) } ;

coherence
union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } is Subset of (E ^omega)

proof end;

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 & 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 & x in A |^ m ) )

proof end;

theorem Th3: :: FLANG_3:3

for E being set
for A being Subset of (E ^omega)
for m, n being Nat st n <= m holds
A |^ m c= A |^.. n by Th2;

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 & A = {} ) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 *

proof end;

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 ) )

proof end;

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 ) )

proof end;

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))

proof end;

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

proof end;

theorem Th14: :: FLANG_3:14

for E, x being set
for A being Subset of (E ^omega)
for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}

proof end;

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 & A = {} ) ) )

proof end;

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

proof end;

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

proof end;

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)

proof end;

theorem Th19: :: FLANG_3:19

for E being set
for A being Subset of (E ^omega)
for m, n being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)

proof end;

theorem :: FLANG_3:20

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^.. n) * = (A |^.. n) ?

proof end;

theorem Th21: :: FLANG_3:21

for E being set
for A, B, C being Subset of (E ^omega)
for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)

proof end;

theorem Th22: :: FLANG_3:22

for E being set
for A being Subset of (E ^omega)
for k, n being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)

proof end;

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

proof end;

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)

proof end;

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))

proof end;

theorem :: FLANG_3:26

for E being set
for A, B being Subset of (E ^omega)
for n being Nat st <%> E in B holds
( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )

proof end;

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)

proof end;

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 & n > 0 holds
A |^ n c= B |^.. k

proof end;

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 & n > 0 holds
A |^.. n c= B |^.. k

proof end;

theorem Th30: :: FLANG_3:30

for E being set
for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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 & b in C |^.. n holds
a ^ b in C |^.. (m + n)

proof end;

theorem Th38: :: FLANG_3:38

for E, x being set
for A being Subset of (E ^omega)
for k being Nat st A |^.. k = {x} holds
x = <%> E

proof end;

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 *

proof end;

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 ) )

proof end;

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

proof end;

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)

proof end;

theorem :: FLANG_3:43

for E being set
for A, B being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )

proof end;

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)

proof end;

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

proof end;

theorem Th46: :: FLANG_3:46

for E, x being set
for A being Subset of (E ^omega)
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

proof end;

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

proof end;

:: Positive Closure
:: Definition of +

definition

let E be set ;
let A be Subset of (E ^omega);

func A + -> 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 & B = A |^ n ) } ;

coherence
union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } is Subset of (E ^omega)

proof end;

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 & 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 & x in A |^ n ) )

proof end;

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 + by Th48;

theorem Th50: :: FLANG_3:50

for E being set
for A being Subset of (E ^omega) holds A + = A |^.. 1

proof end;

theorem :: FLANG_3:51

for E being set
for A being Subset of (E ^omega) holds
( A + = {} iff A = {} )

proof end;

theorem Th52: :: FLANG_3:52

for E being set
for A being Subset of (E ^omega) holds A + = (A *) ^^ A

proof end;

theorem Th53: :: FLANG_3:53

for E being set
for A being Subset of (E ^omega) holds A * = {(<%> E)} \/ (A +)

proof end;

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))

proof end;

theorem Th55: :: FLANG_3:55

for E being set
for A being Subset of (E ^omega) holds A + c= A *

proof end;

theorem Th56: :: FLANG_3:56

for E being set
for A being Subset of (E ^omega) holds
( <%> E in A + iff <%> E in A )

proof end;

theorem Th57: :: FLANG_3:57

for E being set
for A being Subset of (E ^omega) holds
( A + = A * iff <%> E in A )

proof end;

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 +

proof end;

theorem Th59: :: FLANG_3:59

for E being set
for A being Subset of (E ^omega) holds A c= A +

proof end;

theorem Th60: :: FLANG_3:60

for E being set
for A being Subset of (E ^omega) holds
( (A *) + = A * & (A +) * = A * )

proof end;

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 *

proof end;

theorem :: FLANG_3:62

for E being set
for A being Subset of (E ^omega) holds (A +) + = A +

proof end;

theorem :: FLANG_3:63

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_3:64

for E being set
for A being Subset of (E ^omega) holds
( A + = {(<%> E)} iff A = {(<%> E)} )

proof end;

theorem :: FLANG_3:65

for E being set
for A being Subset of (E ^omega) holds
( (A +) ? = A * & (A ?) + = A * )

proof end;

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 + & b in C + holds
a ^ b in C +

proof end;

theorem :: FLANG_3:67

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 +

proof end;

theorem :: FLANG_3:68

for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A +

proof end;

theorem :: FLANG_3:69

for E, x being set
for A being Subset of (E ^omega) st A + = {x} holds
x = <%> E

proof end;

theorem :: FLANG_3:70

for E being set
for A being Subset of (E ^omega) holds A ^^ (A +) = (A +) ^^ A

proof end;

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)

proof end;

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))

proof end;

theorem :: FLANG_3:73

for E being set
for A, B being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) & A c= (B +) ^^ A )

proof end;

theorem :: FLANG_3:74

for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2

proof end;

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)

proof end;

theorem :: FLANG_3:76

for E being set
for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2

proof end;

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)

proof end;

theorem :: FLANG_3:78

for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^ n c= B +

proof end;

theorem :: FLANG_3:79

for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = (A ?) ^^ (A +)

proof end;

theorem :: FLANG_3:80

for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = A +

proof end;

theorem :: FLANG_3:81

for E being set
for A being Subset of (E ^omega) holds
( A ? c= A + iff <%> E in A )

proof end;

theorem :: FLANG_3: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_3:83

for E being set
for A, B being Subset of (E ^omega) st A c= B + holds
B + = (B \/ A) +

proof end;

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 +

proof end;

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 +

proof end;

theorem Th86: :: FLANG_3:86

for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A +) = (A +) ^^ (A *)

proof end;

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

proof end;

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

proof end;

theorem :: FLANG_3:89

for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^.. n c= B +

proof end;

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)

proof end;

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 +)

proof end;

theorem Th92: :: FLANG_3:92

for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A *) = A +

proof end;

theorem :: FLANG_3:93

for E being set
for A, B being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + & B ^^ (A +) c= A + )

proof end;

theorem :: FLANG_3:94

for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +)

proof end;

theorem :: FLANG_3:95

for E being set
for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) +

proof end;

theorem :: FLANG_3:96

for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A + iff <%x%> in A )

proof end;