FLANG_1: Formal Languages -- Concatenation and Closure

:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

definition

let E be set ;
let a, b be Element of E ^omega ;
:: original: ^
redefine func a ^ b -> Element of E ^omega ;
coherence by AFINSQ_1:def 8;

end;

definition

let E be set ;
:: original: <%>
redefine func <%> E -> Element of E ^omega ;
coherence by AFINSQ_1:def 8;

end;

definition

let E be non empty set ;
let e be Element of E;
:: original: <%
redefine func <%e%> -> Element of E ^omega ;
coherence by AFINSQ_1:def 8;

end;

definition

let E be set ;
let a be Element of E ^omega ;
:: original: {
redefine func {a} -> Subset of (E ^omega);
coherence by SUBSET_1:55;

end;

definition

let E be set ;
let f be Function of NAT,(bool E);
let n be Nat;
:: original: .
redefine func f . n -> Subset of E;
coherence

proof end;

end;

theorem Th1: :: FLANG_1:1

for n1, n, n2 being Nat st ( n1 > n or n2 > n ) holds
n1 + n2 > n

proof end;

theorem Th2: :: FLANG_1:2

for n1, n, n2 being Nat st n1 + n <= n2 + 1 & n > 0 holds
n1 <= n2

proof end;

theorem Th3: :: FLANG_1:3

for n1, n2 being Nat holds
( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )

proof end;

theorem Th4: :: FLANG_1:4

for x, E being set
for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )

proof end;

theorem Th5: :: FLANG_1:5

for E being set
for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )

proof end;

theorem Th6: :: FLANG_1:6

for x, E being set st <%x%> is Element of E ^omega holds
x in E

proof end;

theorem Th7: :: FLANG_1:7

for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )

proof end;

theorem Th8: :: FLANG_1:8

for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = <%x%> ^ q

proof end;

theorem :: FLANG_1:9

for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )

proof end;

theorem :: FLANG_1:10

canceled;

Lm1: for i, j being Nat
for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
by AFINSQ_1:65;

theorem :: FLANG_1:11

for E being set
for b being Element of E ^omega
for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )

proof end;

theorem Th12: :: FLANG_1:12

for E being set
for a being Element of E ^omega st a ^ a = a holds
a = {}

proof end;

begin

definition

let E be set ;
let A, B be Subset of (E ^omega);
func A ^^ B -> Subset of (E ^omega) means :Def1: :: FLANG_1:def 1
for x being set holds
( x in it iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ^^ FLANG_1:def 1 :

theorem Th13: :: FLANG_1:13

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

proof end;

theorem Th14: :: FLANG_1:14

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

proof end;

theorem Th15: :: FLANG_1:15

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

proof end;

theorem Th16: :: FLANG_1:16

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

proof end;

theorem Th17: :: FLANG_1:17

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

proof end;

theorem Th18: :: FLANG_1:18

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

proof end;

theorem Th19: :: FLANG_1:19

for E being set
for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C)

proof end;

theorem Th20: :: FLANG_1:20

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

proof end;

theorem Th21: :: FLANG_1:21

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

proof end;

theorem Th22: :: FLANG_1:22

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

proof end;

theorem :: FLANG_1:23

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

proof end;

begin

definition

let E be set ;
let A be Subset of (E ^omega);
let n be Nat;
func A |^ n -> Subset of (E ^omega) means :Def2: :: FLANG_1:def 2
ex concat being Function of NAT,(bool (E ^omega)) st
( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines |^ FLANG_1:def 2 :

theorem Th24: :: FLANG_1:24

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 Th25: :: FLANG_1:25

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

proof end;

theorem Th26: :: FLANG_1:26

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

proof end;

theorem Th27: :: FLANG_1:27

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

proof end;

theorem Th28: :: FLANG_1:28

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 Th29: :: FLANG_1:29

for E being set
for n being Nat holds {(<%> E)} |^ n = {(<%> E)}

proof end;

theorem :: FLANG_1:30

for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )

proof end;

theorem Th31: :: FLANG_1:31

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
<%> E in A |^ n

proof end;

theorem :: FLANG_1:32

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A |^ n & n > 0 holds
<%> E in A

proof end;

theorem Th33: :: FLANG_1:33

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

proof end;

theorem Th34: :: FLANG_1:34

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

proof end;

theorem :: FLANG_1:35

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

proof end;

theorem Th36: :: FLANG_1:36

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_1:37

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

proof end;

theorem Th38: :: FLANG_1:38

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 :: FLANG_1:39

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

proof end;

theorem :: FLANG_1:40

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

proof end;

theorem Th41: :: FLANG_1:41

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;

begin

definition

let E be set ;
let A be Subset of (E ^omega);
func A * -> Subset of (E ^omega) equals :: FLANG_1:def 3
union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;
coherence

proof end;

end;

:: deftheorem defines * FLANG_1:def 3 :

theorem Th42: :: FLANG_1:42

for E, x being set
for A being Subset of (E ^omega) holds
( x in A * iff ex n being Nat st x in A |^ n )

proof end;

theorem Th43: :: FLANG_1:43

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

proof end;

theorem Th44: :: FLANG_1:44

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

proof end;

theorem :: FLANG_1:45

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

proof end;

theorem Th46: :: FLANG_1:46

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 Th47: :: FLANG_1:47

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

proof end;

theorem :: FLANG_1:48

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

proof end;

theorem Th49: :: FLANG_1:49

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

proof end;

theorem :: FLANG_1:50

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

proof end;

theorem Th51: :: FLANG_1:51

for E, x being set
for A being Subset of (E ^omega)
for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )

proof end;

theorem :: FLANG_1:52

for E being set
for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )

proof end;

theorem Th53: :: FLANG_1:53

for E, x being set
for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds
x in A *

proof end;

theorem :: FLANG_1:54

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

proof end;

theorem Th55: :: FLANG_1:55

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

proof end;

theorem :: FLANG_1:56

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

proof end;

theorem Th57: :: FLANG_1:57

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

proof end;

theorem Th58: :: FLANG_1:58

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

proof end;

theorem :: FLANG_1:59

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

proof end;

theorem Th60: :: FLANG_1:60

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 Th61: :: FLANG_1:61

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

proof end;

theorem Th62: :: FLANG_1:62

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

proof end;

theorem Th63: :: FLANG_1:63

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

proof end;

theorem :: FLANG_1:64

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

proof end;

theorem :: FLANG_1:65

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) * c= A * by Th43, Th61;

theorem Th66: :: FLANG_1:66

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

proof end;

theorem :: FLANG_1:67

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

proof end;

theorem Th68: :: FLANG_1:68

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

proof end;

theorem Th69: :: FLANG_1:69

for E being set
for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *

proof end;

theorem :: FLANG_1:70

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

proof end;

theorem :: FLANG_1:71

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

proof end;

theorem :: FLANG_1:72

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

proof end;

theorem Th73: :: FLANG_1:73

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

proof end;

begin

definition

let E be set ;
func Lex E -> Subset of (E ^omega) means :Def4: :: FLANG_1:def 4
for x being set holds
( x in it iff ex e being Element of E st
( e in E & x = <%e%> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Lex FLANG_1:def 4 :

theorem Th74: :: FLANG_1:74

for E being set
for a being Element of E ^omega holds a in (Lex E) |^ (len a)

proof end;

theorem :: FLANG_1:75

for E being set holds (Lex E) * = E ^omega

proof end;

theorem :: FLANG_1:76

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

proof end;