:: by Micha{\l} Trybulec

::

:: Received March 9, 2007

:: Copyright (c) 2007-2016 Association of Mizar Users

:: Preliminaries - Redefinitions

definition

let E be set ;

let a, b be Element of E ^omega ;

:: original: ^

redefine func a ^ b -> Element of E ^omega ;

coherence

a ^ b is Element of E ^omega by AFINSQ_1:def 7;

end;
let a, b be Element of E ^omega ;

:: original: ^

redefine func a ^ b -> Element of E ^omega ;

coherence

a ^ b is Element of E ^omega by AFINSQ_1:def 7;

definition

let E be set ;

:: original: <%>

redefine func <%> E -> Element of E ^omega ;

coherence

<%> E is Element of E ^omega by AFINSQ_1:def 7;

end;
:: original: <%>

redefine func <%> E -> Element of E ^omega ;

coherence

<%> E is Element of E ^omega by AFINSQ_1:def 7;

definition

let E be non empty set ;

let e be Element of E;

:: original: <%

redefine func <%e%> -> Element of E ^omega ;

coherence

<%e%> is Element of E ^omega by AFINSQ_1:def 7;

end;
let e be Element of E;

:: original: <%

redefine func <%e%> -> Element of E ^omega ;

coherence

<%e%> is Element of E ^omega by AFINSQ_1:def 7;

definition

let E be set ;

let a be Element of E ^omega ;

:: original: {

redefine func {a} -> Subset of (E ^omega);

coherence

{a} is Subset of (E ^omega) by SUBSET_1:33;

end;
let a be Element of E ^omega ;

:: original: {

redefine func {a} -> Subset of (E ^omega);

coherence

{a} is Subset of (E ^omega) by SUBSET_1:33;

definition

let E be set ;

let f be sequence of (bool E);

let n be Nat;

:: original: .

redefine func f . n -> Subset of E;

coherence

f . n is Subset of E

end;
let f be sequence of (bool E);

let n be Nat;

:: original: .

redefine func f . n -> Subset of E;

coherence

f . n is Subset of E

proof end;

:: Preliminaries - Numbers:

:: Preliminaries - Sequences:

theorem Th4: :: FLANG_1:4

for E, x being set

for a, b being Element of E ^omega holds

( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )

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 )

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

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 object st p = <%x%> ^ q

ex q being XFinSequence ex x being object 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 )

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;

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

theorem :: FLANG_1:10

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 )

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;

:: Concatenation of Languages

:: Definition of ^^

:: Definition of ^^

definition

let E be set ;

let A, B be Subset of (E ^omega);

ex b_{1} being Subset of (E ^omega) st

for x being set holds

( x in b_{1} iff ex a, b being Element of E ^omega st

( a in A & b in B & x = a ^ b ) )

for b_{1}, b_{2} being Subset of (E ^omega) st ( for x being set holds

( x in b_{1} iff ex a, b being Element of E ^omega st

( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds

( x in b_{2} iff ex a, b being Element of E ^omega st

( a in A & b in B & x = a ^ b ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being set holds

( x in b

( a in A & b in B & x = a ^ b ) )

proof end;

uniqueness for b

( x in b

( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds

( x in b

( a in A & b in B & x = a ^ b ) ) ) holds

b

proof end;

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

for E being set

for A, B, b_{4} being Subset of (E ^omega) holds

( b_{4} = A ^^ B iff for x being set holds

( x in b_{4} iff ex a, b being Element of E ^omega st

( a in A & b in B & x = a ^ b ) ) );

for E being set

for A, B, b

( b

( x in b

( a in A & b in B & x = a ^ b ) ) );

:: Concatenation of Languages

:: Properties of ^^

:: Properties of ^^

theorem Th14: :: FLANG_1:14

for E being set

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

( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )

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

( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )

proof end;

theorem Th15: :: FLANG_1:15

for E being set

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

( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )

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

( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )

proof end;

theorem Th16: :: FLANG_1:16

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 )

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

( A c= A ^^ B & A c= B ^^ A )

proof end;

theorem Th19: :: FLANG_1:19

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

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 Th20: :: FLANG_1:20

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 )

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 Th21: :: FLANG_1:21

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 )

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

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;

:: Concatenation of a Language with Itself

:: Definition of |^

:: Definition of |^

definition

let E be set ;

let A be Subset of (E ^omega);

let n be Nat;

ex b_{1} being Subset of (E ^omega) ex concat being sequence of (bool (E ^omega)) st

( b_{1} = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )

for b_{1}, b_{2} being Subset of (E ^omega) st ex concat being sequence of (bool (E ^omega)) st

( b_{1} = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being sequence of (bool (E ^omega)) st

( b_{2} = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds

b_{1} = b_{2}

end;
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 sequence of (bool (E ^omega)) st

( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );

existence ex concat being sequence of (bool (E ^omega)) st

( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

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

for E being set

for A being Subset of (E ^omega)

for n being Nat

for b_{4} being Subset of (E ^omega) holds

( b_{4} = A |^ n iff ex concat being sequence of (bool (E ^omega)) st

( b_{4} = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) );

for E being set

for A being Subset of (E ^omega)

for n being Nat

for b

( b

( b

:: Concatenation of a Language with Itself

:: Properties of |^

:: Properties of |^

theorem Th27: :: FLANG_1:27

for E being set

for A being Subset of (E ^omega)

for n being Nat holds

( A |^ n = {} iff ( n > 0 & A = {} ) )

for A being Subset of (E ^omega)

for n being Nat holds

( A |^ n = {} iff ( n > 0 & A = {} ) )

proof end;

theorem :: FLANG_1:29

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

for A being Subset of (E ^omega)

for n being Nat holds

( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )

proof end;

theorem Th30: :: FLANG_1:30

for E being set

for A being Subset of (E ^omega)

for n being Nat st <%> E in A holds

<%> E in A |^ n

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

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

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 Th32: :: FLANG_1:32

for E being set

for A being Subset of (E ^omega)

for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)

for A being Subset of (E ^omega)

for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)

proof end;

theorem Th33: :: FLANG_1:33

for E being set

for A being Subset of (E ^omega)

for n, m being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)

for A being Subset of (E ^omega)

for n, m being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)

proof end;

theorem :: FLANG_1:34

for E being set

for A being Subset of (E ^omega)

for n, m being Nat holds (A |^ m) |^ n = A |^ (m * n)

for A being Subset of (E ^omega)

for n, m being Nat holds (A |^ m) |^ n = A |^ (m * n)

proof end;

theorem Th35: :: FLANG_1:35

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

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

for E being set

for A being Subset of (E ^omega)

for n, m being Nat st <%> E in A & m > n holds

A |^ n c= A |^ m

for A being Subset of (E ^omega)

for n, m being Nat st <%> E in A & m > n holds

A |^ n c= A |^ m

proof end;

theorem Th37: :: FLANG_1:37

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

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

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

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

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)

for A, B being Subset of (E ^omega)

for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)

proof end;

theorem Th40: :: FLANG_1:40

for E being set

for C being Subset of (E ^omega)

for a, b being Element of E ^omega

for n, m being Nat st a in C |^ m & b in C |^ n holds

a ^ b in C |^ (m + n)

for C being Subset of (E ^omega)

for a, b being Element of E ^omega

for n, m being Nat st a in C |^ m & b in C |^ n holds

a ^ b in C |^ (m + n)

proof end;

:: Kleene Closure

:: Definition of *

:: Definition of *

definition

let E be set ;

let A be Subset of (E ^omega);

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

end;
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 union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;

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

proof end;

:: deftheorem defines * FLANG_1:def 3 :

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 B = A |^ n } ;

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 B = A |^ n } ;

:: Kleene Closure

:: Properties of *

:: Properties of *

theorem Th41: :: FLANG_1:41

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 )

for A being Subset of (E ^omega) holds

( x in A * iff ex n being Nat st x in A |^ n )

proof end;

theorem Th45: :: FLANG_1:45

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 *

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

for E being set

for A being Subset of (E ^omega) holds

( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )

for A being Subset of (E ^omega) holds

( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )

proof end;

theorem Th50: :: FLANG_1:50

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

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

theorem Th52: :: FLANG_1:52

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 *

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

theorem Th54: :: FLANG_1:54

for E being set

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

( A * = (A *) ^^ A & A * = A ^^ (A *) )

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

( A * = (A *) ^^ A & A * = A ^^ (A *) )

proof end;

theorem :: FLANG_1:55

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

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 Th56: :: FLANG_1:56

for E being set

for A being Subset of (E ^omega) holds

( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )

for A being Subset of (E ^omega) holds

( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )

proof end;

theorem :: FLANG_1:58

for E being set

for A being Subset of (E ^omega)

for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)

for A being Subset of (E ^omega)

for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)

proof end;

theorem :: FLANG_1:64

:: Lexemes as a Subset of E^omega

:: Definition of Lex

:: Definition of Lex

definition

let E be set ;

ex b_{1} being Subset of (E ^omega) st

for x being set holds

( x in b_{1} iff ex e being Element of E st

( e in E & x = <%e%> ) )

for b_{1}, b_{2} being Subset of (E ^omega) st ( for x being set holds

( x in b_{1} iff ex e being Element of E st

( e in E & x = <%e%> ) ) ) & ( for x being set holds

( x in b_{2} iff ex e being Element of E st

( e in E & x = <%e%> ) ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff ex e being Element of E st

( e in E & x = <%e%> ) );

ex b

for x being set holds

( x in b

( e in E & x = <%e%> ) )

proof end;

uniqueness for b

( x in b

( e in E & x = <%e%> ) ) ) & ( for x being set holds

( x in b

( e in E & x = <%e%> ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Lex FLANG_1:def 4 :

for E being set

for b_{2} being Subset of (E ^omega) holds

( b_{2} = Lex E iff for x being set holds

( x in b_{2} iff ex e being Element of E st

( e in E & x = <%e%> ) ) );

for E being set

for b

( b

( x in b

( e in E & x = <%e%> ) ) );

:: Lexemes as a Subset of E^omega

:: Properties of Lex

:: Properties of Lex