:: LANG1 semantic presentation
begin
definition
attrc1 is strict ;
struct DTConstrStr -> 1-sorted ;
aggrDTConstrStr(# carrier, Rules #) -> DTConstrStr ;
sel Rules c1 -> Relation of the carrier of c1,( the carrier of c1 *);
end;
registration
cluster non empty strict for DTConstrStr ;
existence
ex b1 being DTConstrStr st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set P = the Relation of the non empty set ,( the non empty set *);
take DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) ; ::_thesis: ( not DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty & DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict )
thus not the carrier of DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict
thus DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict ; ::_thesis: verum
end;
end;
definition
attrc1 is strict ;
struct GrammarStr -> DTConstrStr ;
aggrGrammarStr(# carrier, InitialSym, Rules #) -> GrammarStr ;
sel InitialSym c1 -> Element of the carrier of c1;
end;
registration
cluster non empty for GrammarStr ;
existence
not for b1 being GrammarStr holds b1 is empty
proof
set A = the non empty set ;
set P = the Relation of the non empty set ,( the non empty set *);
set I = the Element of the non empty set ;
take GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) ; ::_thesis: not GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty
thus not the carrier of GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
let G be DTConstrStr ;
mode Symbol of G is Element of G;
mode String of G is Element of the carrier of G * ;
end;
definition
let G be non empty DTConstrStr ;
let s be Symbol of G;
let n be FinSequence;
preds ==> n means :Def1: :: LANG1:def 1
[s,n] in the Rules of G;
end;
:: deftheorem Def1 defines ==> LANG1:def_1_:_
for G being non empty DTConstrStr
for s being Symbol of G
for n being FinSequence holds
( s ==> n iff [s,n] in the Rules of G );
definition
let G be non empty DTConstrStr ;
func Terminals G -> set equals :: LANG1:def 2
{ s where s is Symbol of G : for n being FinSequence holds not s ==> n } ;
coherence
{ s where s is Symbol of G : for n being FinSequence holds not s ==> n } is set ;
func NonTerminals G -> set equals :: LANG1:def 3
{ s where s is Symbol of G : ex n being FinSequence st s ==> n } ;
coherence
{ s where s is Symbol of G : ex n being FinSequence st s ==> n } is set ;
end;
:: deftheorem defines Terminals LANG1:def_2_:_
for G being non empty DTConstrStr holds Terminals G = { s where s is Symbol of G : for n being FinSequence holds not s ==> n } ;
:: deftheorem defines NonTerminals LANG1:def_3_:_
for G being non empty DTConstrStr holds NonTerminals G = { s where s is Symbol of G : ex n being FinSequence st s ==> n } ;
theorem :: LANG1:1
for G being non empty DTConstrStr holds (Terminals G) \/ (NonTerminals G) = the carrier of G
proof
let G be non empty DTConstrStr ; ::_thesis: (Terminals G) \/ (NonTerminals G) = the carrier of G
thus (Terminals G) \/ (NonTerminals G) c= the carrier of G :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= (Terminals G) \/ (NonTerminals G)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (Terminals G) \/ (NonTerminals G) or a in the carrier of G )
assume a in (Terminals G) \/ (NonTerminals G) ; ::_thesis: a in the carrier of G
then ( a in Terminals G or a in NonTerminals G ) by XBOOLE_0:def_3;
then ( ex s being Symbol of G st
( a = s & ( for n being FinSequence holds not s ==> n ) ) or ex s being Symbol of G st
( a = s & ex n being FinSequence st s ==> n ) ) ;
hence a in the carrier of G ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of G or a in (Terminals G) \/ (NonTerminals G) )
assume a in the carrier of G ; ::_thesis: a in (Terminals G) \/ (NonTerminals G)
then reconsider s = a as Symbol of G ;
( for n being FinSequence holds not s ==> n or ex n being FinSequence st s ==> n ) ;
then ( a in Terminals G or a in NonTerminals G ) ;
hence a in (Terminals G) \/ (NonTerminals G) by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let G be non empty DTConstrStr ;
let n, m be String of G;
predn ==> m means :: LANG1:def 4
ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 & m = (n1 ^ n3) ^ n2 & s ==> n3 );
end;
:: deftheorem defines ==> LANG1:def_4_:_
for G being non empty DTConstrStr
for n, m being String of G holds
( n ==> m iff ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 & m = (n1 ^ n3) ^ n2 & s ==> n3 ) );
theorem :: LANG1:2
for G being non empty DTConstrStr
for s being Symbol of G
for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
proof
let G be non empty DTConstrStr ; ::_thesis: for s being Symbol of G
for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
let s be Symbol of G; ::_thesis: for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
let n, n1, n2 be String of G; ::_thesis: ( s ==> n implies (n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2 )
assume A1: s ==> n ; ::_thesis: (n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
take n1 ; :: according to LANG1:def_4 ::_thesis: ex n2, n3 being String of G ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n3) ^ n2 & s ==> n3 )
take n2 ; ::_thesis: ex n3 being String of G ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n3) ^ n2 & s ==> n3 )
take n ; ::_thesis: ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n )
take s ; ::_thesis: ( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n )
thus ( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n ) by A1; ::_thesis: verum
end;
theorem Th3: :: LANG1:3
for G being non empty DTConstrStr
for s being Symbol of G
for n being String of G st s ==> n holds
<*s*> ==> n
proof
let G be non empty DTConstrStr ; ::_thesis: for s being Symbol of G
for n being String of G st s ==> n holds
<*s*> ==> n
let s be Symbol of G; ::_thesis: for n being String of G st s ==> n holds
<*s*> ==> n
let n be String of G; ::_thesis: ( s ==> n implies <*s*> ==> n )
assume A1: s ==> n ; ::_thesis: <*s*> ==> n
take n1 = <*> the carrier of G; :: according to LANG1:def_4 ::_thesis: ex n2, n3 being String of G ex s being Symbol of G st
( <*s*> = (n1 ^ <*s*>) ^ n2 & n = (n1 ^ n3) ^ n2 & s ==> n3 )
take n2 = <*> the carrier of G; ::_thesis: ex n3 being String of G ex s being Symbol of G st
( <*s*> = (n1 ^ <*s*>) ^ n2 & n = (n1 ^ n3) ^ n2 & s ==> n3 )
take n3 = n; ::_thesis: ex s being Symbol of G st
( <*s*> = (n1 ^ <*s*>) ^ n2 & n = (n1 ^ n3) ^ n2 & s ==> n3 )
take s ; ::_thesis: ( <*s*> = (n1 ^ <*s*>) ^ n2 & n = (n1 ^ n3) ^ n2 & s ==> n3 )
thus <*s*> = n1 ^ <*s*> by FINSEQ_1:34
.= (n1 ^ <*s*>) ^ n2 by FINSEQ_1:34 ; ::_thesis: ( n = (n1 ^ n3) ^ n2 & s ==> n3 )
thus n = n1 ^ n3 by FINSEQ_1:34
.= (n1 ^ n3) ^ n2 by FINSEQ_1:34 ; ::_thesis: s ==> n3
thus s ==> n3 by A1; ::_thesis: verum
end;
theorem Th4: :: LANG1:4
for G being non empty DTConstrStr
for s being Symbol of G
for n being String of G st <*s*> ==> n holds
s ==> n
proof
let G be non empty DTConstrStr ; ::_thesis: for s being Symbol of G
for n being String of G st <*s*> ==> n holds
s ==> n
let s be Symbol of G; ::_thesis: for n being String of G st <*s*> ==> n holds
s ==> n
let n be String of G; ::_thesis: ( <*s*> ==> n implies s ==> n )
given n1, n2, n3 being String of G, t being Symbol of G such that A1: <*s*> = (n1 ^ <*t*>) ^ n2 and
A2: n = (n1 ^ n3) ^ n2 and
A3: t ==> n3 ; :: according to LANG1:def_4 ::_thesis: s ==> n
A4: len <*t*> = 1 by FINSEQ_1:40;
A5: len (n1 ^ <*t*>) = (len n1) + (len <*t*>) by FINSEQ_1:22;
len <*s*> = (len (n1 ^ <*t*>)) + (len n2) by A1, FINSEQ_1:22;
then A6: 1 + 0 = 1 + ((len n1) + (len n2)) by A4, A5, FINSEQ_1:40;
then A7: n2 = {} by NAT_1:7;
A8: n3 ^ {} = n3 by FINSEQ_1:34;
A9: {} ^ n3 = n3 by FINSEQ_1:34;
A10: <*s*> . 1 = s by FINSEQ_1:40;
A11: <*t*> ^ {} = <*t*> by FINSEQ_1:34;
A12: {} ^ <*t*> = <*t*> by FINSEQ_1:34;
n1 = {} by A6, NAT_1:7;
hence s ==> n by A1, A2, A3, A7, A12, A11, A9, A8, A10, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th5: :: LANG1:5
for G being non empty DTConstrStr
for n, n1, n2 being String of G st n1 ==> n2 holds
( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )
proof
let G be non empty DTConstrStr ; ::_thesis: for n, n1, n2 being String of G st n1 ==> n2 holds
( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )
let n, n1, n2 be String of G; ::_thesis: ( n1 ==> n2 implies ( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n ) )
given m1, m2, m3 being String of G, s being Symbol of G such that A1: n1 = (m1 ^ <*s*>) ^ m2 and
A2: n2 = (m1 ^ m3) ^ m2 and
A3: s ==> m3 ; :: according to LANG1:def_4 ::_thesis: ( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )
thus n ^ n1 ==> n ^ n2 ::_thesis: n1 ^ n ==> n2 ^ n
proof
take n ^ m1 ; :: according to LANG1:def_4 ::_thesis: ex n2, n3 being String of G ex s being Symbol of G st
( n ^ n1 = ((n ^ m1) ^ <*s*>) ^ n2 & n ^ n2 = ((n ^ m1) ^ n3) ^ n2 & s ==> n3 )
take m2 ; ::_thesis: ex n3 being String of G ex s being Symbol of G st
( n ^ n1 = ((n ^ m1) ^ <*s*>) ^ m2 & n ^ n2 = ((n ^ m1) ^ n3) ^ m2 & s ==> n3 )
take m3 ; ::_thesis: ex s being Symbol of G st
( n ^ n1 = ((n ^ m1) ^ <*s*>) ^ m2 & n ^ n2 = ((n ^ m1) ^ m3) ^ m2 & s ==> m3 )
take s ; ::_thesis: ( n ^ n1 = ((n ^ m1) ^ <*s*>) ^ m2 & n ^ n2 = ((n ^ m1) ^ m3) ^ m2 & s ==> m3 )
thus n ^ n1 = (n ^ (m1 ^ <*s*>)) ^ m2 by A1, FINSEQ_1:32
.= ((n ^ m1) ^ <*s*>) ^ m2 by FINSEQ_1:32 ; ::_thesis: ( n ^ n2 = ((n ^ m1) ^ m3) ^ m2 & s ==> m3 )
thus n ^ n2 = (n ^ (m1 ^ m3)) ^ m2 by A2, FINSEQ_1:32
.= ((n ^ m1) ^ m3) ^ m2 by FINSEQ_1:32 ; ::_thesis: s ==> m3
thus s ==> m3 by A3; ::_thesis: verum
end;
take m1 ; :: according to LANG1:def_4 ::_thesis: ex n2, n3 being String of G ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ n2 & n2 ^ n = (m1 ^ n3) ^ n2 & s ==> n3 )
take m2 ^ n ; ::_thesis: ex n3 being String of G ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ n3) ^ (m2 ^ n) & s ==> n3 )
take m3 ; ::_thesis: ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 )
take s ; ::_thesis: ( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 )
thus ( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 ) by A1, A2, A3, FINSEQ_1:32; ::_thesis: verum
end;
definition
let G be non empty DTConstrStr ;
let n, m be String of G;
predm is_derivable_from n means :Def5: :: LANG1:def 5
ex p being FinSequence st
( len p >= 1 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) );
end;
:: deftheorem Def5 defines is_derivable_from LANG1:def_5_:_
for G being non empty DTConstrStr
for n, m being String of G holds
( m is_derivable_from n iff ex p being FinSequence st
( len p >= 1 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) ) );
theorem Th6: :: LANG1:6
for G being non empty DTConstrStr
for n being String of G holds n is_derivable_from n
proof
let G be non empty DTConstrStr ; ::_thesis: for n being String of G holds n is_derivable_from n
let n be String of G; ::_thesis: n is_derivable_from n
take p = <*n*>; :: according to LANG1:def_5 ::_thesis: ( len p >= 1 & p . 1 = n & p . (len p) = n & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
len p = 1 by FINSEQ_1:40;
hence ( len p >= 1 & p . 1 = n & p . (len p) = n ) by FINSEQ_1:40; ::_thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; ::_thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume that
A1: i >= 1 and
A2: i < len p ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
thus ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) by A1, A2, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th7: :: LANG1:7
for G being non empty DTConstrStr
for n, m being String of G st n ==> m holds
m is_derivable_from n
proof
let G be non empty DTConstrStr ; ::_thesis: for n, m being String of G st n ==> m holds
m is_derivable_from n
let n, m be String of G; ::_thesis: ( n ==> m implies m is_derivable_from n )
assume A1: n ==> m ; ::_thesis: m is_derivable_from n
take p = <*n,m*>; :: according to LANG1:def_5 ::_thesis: ( len p >= 1 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
A2: len p = 2 by FINSEQ_1:44;
hence ( len p >= 1 & p . 1 = n & p . (len p) = m ) by FINSEQ_1:44; ::_thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; ::_thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume that
A3: i >= 1 and
A4: i < len p ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take a = n; ::_thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = m; ::_thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
2 = 1 + 1 ;
then i <= 1 by A2, A4, NAT_1:13;
then A5: i = 1 by A3, XXREAL_0:1;
hence p . i = a by FINSEQ_1:44; ::_thesis: ( p . (i + 1) = b & a ==> b )
thus p . (i + 1) = b by A5, FINSEQ_1:44; ::_thesis: a ==> b
thus a ==> b by A1; ::_thesis: verum
end;
theorem Th8: :: LANG1:8
for G being non empty DTConstrStr
for n1, n2, n3 being String of G st n1 is_derivable_from n2 & n2 is_derivable_from n3 holds
n1 is_derivable_from n3
proof
let G be non empty DTConstrStr ; ::_thesis: for n1, n2, n3 being String of G st n1 is_derivable_from n2 & n2 is_derivable_from n3 holds
n1 is_derivable_from n3
let n1, n2, n3 be String of G; ::_thesis: ( n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1 is_derivable_from n3 )
given p1 being FinSequence such that A1: len p1 >= 1 and
A2: p1 . 1 = n2 and
A3: p1 . (len p1) = n1 and
A4: for i being Element of NAT st i >= 1 & i < len p1 holds
ex a, b being String of G st
( p1 . i = a & p1 . (i + 1) = b & a ==> b ) ; :: according to LANG1:def_5 ::_thesis: ( not n2 is_derivable_from n3 or n1 is_derivable_from n3 )
given p2 being FinSequence such that A5: len p2 >= 1 and
A6: p2 . 1 = n3 and
A7: p2 . (len p2) = n2 and
A8: for i being Element of NAT st i >= 1 & i < len p2 holds
ex a, b being String of G st
( p2 . i = a & p2 . (i + 1) = b & a ==> b ) ; :: according to LANG1:def_5 ::_thesis: n1 is_derivable_from n3
p2 <> {} by A5;
then consider q being FinSequence, x being set such that
A9: p2 = q ^ <*x*> by FINSEQ_1:46;
take p = q ^ p1; :: according to LANG1:def_5 ::_thesis: ( len p >= 1 & p . 1 = n3 & p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
A10: 1 + (len q) >= 1 by NAT_1:11;
A11: len p = (len q) + (len p1) by FINSEQ_1:22;
then len p >= 1 + (len q) by A1, XREAL_1:7;
hence len p >= 1 by A10, XXREAL_0:2; ::_thesis: ( p . 1 = n3 & p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
now__::_thesis:_p_._1_=_n3
percases ( q = {} or q <> {} ) ;
supposeA12: q = {} ; ::_thesis: p . 1 = n3
then A13: p = p1 by FINSEQ_1:34;
p2 = <*x*> by A9, A12, FINSEQ_1:34;
hence p . 1 = n3 by A2, A6, A7, A13, FINSEQ_1:40; ::_thesis: verum
end;
supposeA14: q <> {} ; ::_thesis: p . 1 = n3
A15: 0 + 1 = 1 ;
len q > 0 by A14, NAT_1:2;
then len q >= 1 by A15, NAT_1:13;
then A16: 1 in dom q by FINSEQ_3:25;
then p . 1 = q . 1 by FINSEQ_1:def_7;
hence p . 1 = n3 by A6, A9, A16, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence p . 1 = n3 ; ::_thesis: ( p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
len p1 in dom p1 by A1, FINSEQ_3:25;
hence p . (len p) = n1 by A3, A11, FINSEQ_1:def_7; ::_thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; ::_thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume that
A17: i >= 1 and
A18: i < len p ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
len <*x*> = 1 by FINSEQ_1:40;
then A19: len p2 = (len q) + 1 by A9, FINSEQ_1:22;
now__::_thesis:_ex_a,_b_being_String_of_G_st_
(_p_._i_=_a_&_p_._(i_+_1)_=_b_&_a_==>_b_)
percases ( i + 1 = len p2 or i + 1 > len p2 or i + 1 < len p2 ) by XXREAL_0:1;
supposeA20: i + 1 = len p2 ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
A21: 1 in dom p1 by A1, FINSEQ_3:25;
i < len p2 by A20, NAT_1:13;
then consider a, b being String of G such that
A22: p2 . i = a and
A23: p2 . (i + 1) = b and
A24: a ==> b by A8, A17;
take a = a; ::_thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; ::_thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
A25: i in dom q by A19, A17, A20, FINSEQ_3:25;
then p2 . i = q . i by A9, FINSEQ_1:def_7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A2, A7, A19, A20, A22, A23, A24, A21, A25, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose i + 1 > len p2 ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
then i >= len p2 by NAT_1:13;
then consider j being Nat such that
A26: i = (len p2) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A27: i = (len q) + (1 + j) by A19, A26;
then A28: 1 + j < len p1 by A11, A18, XREAL_1:6;
then consider a, b being String of G such that
A29: p1 . (1 + j) = a and
A30: p1 . ((1 + j) + 1) = b and
A31: a ==> b by A4, NAT_1:11;
take a = a; ::_thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; ::_thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
A32: (1 + j) + 1 >= 1 by NAT_1:11;
1 + j >= 1 by NAT_1:11;
then A33: 1 + j in dom p1 by A28, FINSEQ_3:25;
(1 + j) + 1 <= len p1 by A28, NAT_1:13;
then A34: (1 + j) + 1 in dom p1 by A32, FINSEQ_3:25;
i + 1 = (len q) + ((1 + j) + 1) by A19, A26;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A27, A29, A30, A31, A33, A34, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA35: i + 1 < len p2 ; ::_thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
A36: 1 <= 1 + i by NAT_1:11;
i + 1 <= len q by A19, A35, NAT_1:13;
then A37: i + 1 in dom q by A36, FINSEQ_3:25;
then A38: p . (i + 1) = q . (i + 1) by FINSEQ_1:def_7;
i < len p2 by A35, NAT_1:13;
then consider a, b being String of G such that
A39: p2 . i = a and
A40: p2 . (i + 1) = b and
A41: a ==> b by A8, A17;
take a = a; ::_thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; ::_thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
i <= len q by A19, A35, XREAL_1:6;
then A42: i in dom q by A17, FINSEQ_3:25;
then p . i = q . i by FINSEQ_1:def_7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A9, A39, A40, A41, A42, A37, A38, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ; ::_thesis: verum
end;
definition
let G be non empty GrammarStr ;
func Lang G -> set equals :: LANG1:def 6
{ a where a is Element of the carrier of G * : ( rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) } ;
coherence
{ a where a is Element of the carrier of G * : ( rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) } is set ;
end;
:: deftheorem defines Lang LANG1:def_6_:_
for G being non empty GrammarStr holds Lang G = { a where a is Element of the carrier of G * : ( rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) } ;
theorem :: LANG1:9
for G being non empty GrammarStr
for n being String of G holds
( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )
proof
let G be non empty GrammarStr ; ::_thesis: for n being String of G holds
( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )
let n be String of G; ::_thesis: ( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )
now__::_thesis:_(_n_in_Lang_G_implies_(_rng_n_c=_Terminals_G_&_n_is_derivable_from_<*_the_InitialSym_of_G*>_)_)
assume n in Lang G ; ::_thesis: ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> )
then ex a being Element of the carrier of G * st
( n = a & rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) ;
hence ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) ; ::_thesis: verum
end;
hence ( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) ) ; ::_thesis: verum
end;
definition
let D, E be non empty set ;
let a be Element of [:D,E:];
:: original: {
redefine func{a} -> Relation of D,E;
coherence
{a} is Relation of D,E
proof
{a} c= [:D,E:] ;
hence {a} is Relation of D,E ; ::_thesis: verum
end;
let b be Element of [:D,E:];
:: original: {
redefine func{a,b} -> Relation of D,E;
coherence
{a,b} is Relation of D,E
proof
{a,b} c= [:D,E:] ;
hence {a,b} is Relation of D,E ; ::_thesis: verum
end;
end;
definition
let a be set ;
func EmptyGrammar a -> strict GrammarStr means :Def7: :: LANG1:def 7
( the carrier of it = {a} & the Rules of it = {[a,{}]} );
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a} & the Rules of b1 = {[a,{}]} )
proof
reconsider S = a as Element of {a} by TARSKI:def_1;
take GrammarStr(# {a},S,{[S,(<*> {a})]} #) ; ::_thesis: ( the carrier of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {a} & the Rules of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {[a,{}]} )
thus ( the carrier of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {a} & the Rules of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {[a,{}]} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a} & the Rules of b1 = {[a,{}]} & the carrier of b2 = {a} & the Rules of b2 = {[a,{}]} holds
b1 = b2
proof
let G1, G2 be strict GrammarStr ; ::_thesis: ( the carrier of G1 = {a} & the Rules of G1 = {[a,{}]} & the carrier of G2 = {a} & the Rules of G2 = {[a,{}]} implies G1 = G2 )
assume that
A1: the carrier of G1 = {a} and
A2: the Rules of G1 = {[a,{}]} and
A3: the carrier of G2 = {a} and
A4: the Rules of G2 = {[a,{}]} ; ::_thesis: G1 = G2
the InitialSym of G1 = a by A1, TARSKI:def_1;
hence G1 = G2 by A1, A2, A3, A4, TARSKI:def_1; ::_thesis: verum
end;
let b be set ;
func SingleGrammar (a,b) -> strict GrammarStr means :Def8: :: LANG1:def 8
( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]} );
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b*>]} )
proof
reconsider S = a, x = b as Element of {a,b} by TARSKI:def_2;
take GrammarStr(# {a,b},S,{[S,<*x*>]} #) ; ::_thesis: ( the carrier of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = {a,b} & the InitialSym of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = a & the Rules of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = {[a,<*b*>]} )
thus ( the carrier of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = {a,b} & the InitialSym of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = a & the Rules of GrammarStr(# {a,b},S,{[S,<*x*>]} #) = {[a,<*b*>]} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b*>]} & the carrier of b2 = {a,b} & the InitialSym of b2 = a & the Rules of b2 = {[a,<*b*>]} holds
b1 = b2 ;
func IterGrammar (a,b) -> strict GrammarStr means :Def9: :: LANG1:def 9
( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]} );
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b,a*>],[a,{}]} )
proof
reconsider S = a, x = b as Element of {a,b} by TARSKI:def_2;
take GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) ; ::_thesis: ( the carrier of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = {a,b} & the InitialSym of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = a & the Rules of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = {[a,<*b,a*>],[a,{}]} )
thus ( the carrier of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = {a,b} & the InitialSym of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = a & the Rules of GrammarStr(# {a,b},S,{[S,<*x,S*>],[S,(<*> {a,b})]} #) = {[a,<*b,a*>],[a,{}]} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b,a*>],[a,{}]} & the carrier of b2 = {a,b} & the InitialSym of b2 = a & the Rules of b2 = {[a,<*b,a*>],[a,{}]} holds
b1 = b2 ;
end;
:: deftheorem Def7 defines EmptyGrammar LANG1:def_7_:_
for a being set
for b2 being strict GrammarStr holds
( b2 = EmptyGrammar a iff ( the carrier of b2 = {a} & the Rules of b2 = {[a,{}]} ) );
:: deftheorem Def8 defines SingleGrammar LANG1:def_8_:_
for a, b being set
for b3 being strict GrammarStr holds
( b3 = SingleGrammar (a,b) iff ( the carrier of b3 = {a,b} & the InitialSym of b3 = a & the Rules of b3 = {[a,<*b*>]} ) );
:: deftheorem Def9 defines IterGrammar LANG1:def_9_:_
for a, b being set
for b3 being strict GrammarStr holds
( b3 = IterGrammar (a,b) iff ( the carrier of b3 = {a,b} & the InitialSym of b3 = a & the Rules of b3 = {[a,<*b,a*>],[a,{}]} ) );
registration
let a be set ;
cluster EmptyGrammar a -> non empty strict ;
coherence
not EmptyGrammar a is empty
proof
the carrier of (EmptyGrammar a) = {a} by Def7;
hence not the carrier of (EmptyGrammar a) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
let b be set ;
cluster SingleGrammar (a,b) -> non empty strict ;
coherence
not SingleGrammar (a,b) is empty
proof
the carrier of (SingleGrammar (a,b)) = {a,b} by Def8;
hence not the carrier of (SingleGrammar (a,b)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
cluster IterGrammar (a,b) -> non empty strict ;
coherence
not IterGrammar (a,b) is empty
proof
the carrier of (IterGrammar (a,b)) = {a,b} by Def9;
hence not the carrier of (IterGrammar (a,b)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
let D be non empty set ;
func TotalGrammar D -> strict GrammarStr means :Def10: :: LANG1:def 10
( the carrier of it = succ D & the InitialSym of it = D & the Rules of it = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} );
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = succ D & the InitialSym of b1 = D & the Rules of b1 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )
proof
reconsider E = succ D as non empty set ;
D in {D} by TARSKI:def_1;
then reconsider S = D as Element of E by XBOOLE_0:def_3;
set R = { [S,<*d,S*>] where d is Element of D : d = d } ;
{ [S,<*d,S*>] where d is Element of D : d = d } c= [:E,(E *):]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [S,<*d,S*>] where d is Element of D : d = d } or a in [:E,(E *):] )
assume a in { [S,<*d,S*>] where d is Element of D : d = d } ; ::_thesis: a in [:E,(E *):]
then consider d being Element of D such that
A1: a = [S,<*d,S*>] and
d = d ;
reconsider d = d as Element of E by XBOOLE_0:def_3;
a = [S,<*d,S*>] by A1;
hence a in [:E,(E *):] ; ::_thesis: verum
end;
then reconsider R = { [S,<*d,S*>] where d is Element of D : d = d } as Relation of E,(E *) ;
take GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) ; ::_thesis: ( the carrier of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = succ D & the InitialSym of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = D & the Rules of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )
thus ( the carrier of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = succ D & the InitialSym of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = D & the Rules of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = succ D & the InitialSym of b1 = D & the Rules of b1 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} & the carrier of b2 = succ D & the InitialSym of b2 = D & the Rules of b2 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} holds
b1 = b2 ;
end;
:: deftheorem Def10 defines TotalGrammar LANG1:def_10_:_
for D being non empty set
for b2 being strict GrammarStr holds
( b2 = TotalGrammar D iff ( the carrier of b2 = succ D & the InitialSym of b2 = D & the Rules of b2 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} ) );
registration
let D be non empty set ;
cluster TotalGrammar D -> non empty strict ;
coherence
not TotalGrammar D is empty
proof
the carrier of (TotalGrammar D) = succ D by Def10;
hence not the carrier of (TotalGrammar D) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem Th10: :: LANG1:10
for a being set holds Terminals (EmptyGrammar a) = {}
proof
let a be set ; ::_thesis: Terminals (EmptyGrammar a) = {}
set E = EmptyGrammar a;
set b = the Element of Terminals (EmptyGrammar a);
the Rules of (EmptyGrammar a) = {[a,{}]} by Def7;
then A1: [a,{}] in the Rules of (EmptyGrammar a) by TARSKI:def_1;
assume not Terminals (EmptyGrammar a) = {} ; ::_thesis: contradiction
then the Element of Terminals (EmptyGrammar a) in Terminals (EmptyGrammar a) ;
then consider s being Symbol of (EmptyGrammar a) such that
the Element of Terminals (EmptyGrammar a) = s and
A2: for n being FinSequence holds not s ==> n ;
the carrier of (EmptyGrammar a) = {a} by Def7;
then s = a by TARSKI:def_1;
then s ==> <*> the carrier of (EmptyGrammar a) by A1, Def1;
hence contradiction by A2; ::_thesis: verum
end;
theorem Th11: :: LANG1:11
for a being set holds Lang (EmptyGrammar a) = {{}}
proof
let a be set ; ::_thesis: Lang (EmptyGrammar a) = {{}}
set E = EmptyGrammar a;
A1: Terminals (EmptyGrammar a) = {} by Th10;
thus Lang (EmptyGrammar a) c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= Lang (EmptyGrammar a)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Lang (EmptyGrammar a) or b in {{}} )
assume b in Lang (EmptyGrammar a) ; ::_thesis: b in {{}}
then ex p being String of (EmptyGrammar a) st
( b = p & rng p c= Terminals (EmptyGrammar a) & p is_derivable_from <* the InitialSym of (EmptyGrammar a)*> ) ;
then b = {} by A1;
hence b in {{}} by TARSKI:def_1; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in {{}} or b in Lang (EmptyGrammar a) )
assume b in {{}} ; ::_thesis: b in Lang (EmptyGrammar a)
then A2: b = {} by TARSKI:def_1;
the Rules of (EmptyGrammar a) = {[a,{}]} by Def7;
then A3: [a,{}] in the Rules of (EmptyGrammar a) by TARSKI:def_1;
the carrier of (EmptyGrammar a) = {a} by Def7;
then a = the InitialSym of (EmptyGrammar a) by TARSKI:def_1;
then the InitialSym of (EmptyGrammar a) ==> <*> the carrier of (EmptyGrammar a) by A3, Def1;
then A4: <*> the carrier of (EmptyGrammar a) is_derivable_from <* the InitialSym of (EmptyGrammar a)*> by Th3, Th7;
rng {} = {} ;
hence b in Lang (EmptyGrammar a) by A1, A2, A4; ::_thesis: verum
end;
theorem Th12: :: LANG1:12
for a, b being set st a <> b holds
Terminals (SingleGrammar (a,b)) = {b}
proof
let a, b be set ; ::_thesis: ( a <> b implies Terminals (SingleGrammar (a,b)) = {b} )
set E = SingleGrammar (a,b);
A1: the Rules of (SingleGrammar (a,b)) = {[a,<*b*>]} by Def8;
A2: the carrier of (SingleGrammar (a,b)) = {a,b} by Def8;
then reconsider x = a, y = b as Symbol of (SingleGrammar (a,b)) by TARSKI:def_2;
assume A3: a <> b ; ::_thesis: Terminals (SingleGrammar (a,b)) = {b}
A4: now__::_thesis:_for_n_being_FinSequence_holds_not_y_==>_n
let n be FinSequence; ::_thesis: not y ==> n
assume y ==> n ; ::_thesis: contradiction
then [y,n] in {[a,<*b*>]} by A1, Def1;
then [y,n] = [a,<*b*>] by TARSKI:def_1;
hence contradiction by A3, XTUPLE_0:1; ::_thesis: verum
end;
[x,<*y*>] in the Rules of (SingleGrammar (a,b)) by A1, TARSKI:def_1;
then A5: x ==> <*y*> by Def1;
thus Terminals (SingleGrammar (a,b)) c= {b} :: according to XBOOLE_0:def_10 ::_thesis: {b} c= Terminals (SingleGrammar (a,b))
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Terminals (SingleGrammar (a,b)) or c in {b} )
assume c in Terminals (SingleGrammar (a,b)) ; ::_thesis: c in {b}
then consider s being Symbol of (SingleGrammar (a,b)) such that
A6: c = s and
A7: for n being FinSequence holds not s ==> n ;
s <> x by A5, A7;
then c = b by A2, A6, TARSKI:def_2;
hence c in {b} by TARSKI:def_1; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in {b} or c in Terminals (SingleGrammar (a,b)) )
assume c in {b} ; ::_thesis: c in Terminals (SingleGrammar (a,b))
then c = b by TARSKI:def_1;
hence c in Terminals (SingleGrammar (a,b)) by A4; ::_thesis: verum
end;
theorem :: LANG1:13
for a, b being set st a <> b holds
Lang (SingleGrammar (a,b)) = {<*b*>}
proof
let a, b be set ; ::_thesis: ( a <> b implies Lang (SingleGrammar (a,b)) = {<*b*>} )
set E = SingleGrammar (a,b);
A1: the InitialSym of (SingleGrammar (a,b)) = a by Def8;
the carrier of (SingleGrammar (a,b)) = {a,b} by Def8;
then reconsider x = a, y = b as Symbol of (SingleGrammar (a,b)) by TARSKI:def_2;
A2: the Rules of (SingleGrammar (a,b)) = {[a,<*b*>]} by Def8;
then [a,<*b*>] in the Rules of (SingleGrammar (a,b)) by TARSKI:def_1;
then the InitialSym of (SingleGrammar (a,b)) ==> <*y*> by A1, Def1;
then A3: <*y*> is_derivable_from <* the InitialSym of (SingleGrammar (a,b))*> by Th3, Th7;
assume A4: a <> b ; ::_thesis: Lang (SingleGrammar (a,b)) = {<*b*>}
then A5: Terminals (SingleGrammar (a,b)) = {b} by Th12;
thus Lang (SingleGrammar (a,b)) c= {<*b*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*b*>} c= Lang (SingleGrammar (a,b))
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Lang (SingleGrammar (a,b)) or c in {<*b*>} )
assume c in Lang (SingleGrammar (a,b)) ; ::_thesis: c in {<*b*>}
then consider p being String of (SingleGrammar (a,b)) such that
A6: c = p and
A7: rng p c= Terminals (SingleGrammar (a,b)) and
A8: p is_derivable_from <* the InitialSym of (SingleGrammar (a,b))*> ;
consider q being FinSequence such that
A9: len q >= 1 and
A10: q . 1 = <* the InitialSym of (SingleGrammar (a,b))*> and
A11: q . (len q) = p and
A12: for i being Element of NAT st i >= 1 & i < len q holds
ex a, b being String of (SingleGrammar (a,b)) st
( q . i = a & q . (i + 1) = b & a ==> b ) by A8, Def5;
now__::_thesis:_not_p_=_<*x*>
assume p = <*x*> ; ::_thesis: contradiction
then rng p = {x} by FINSEQ_1:38;
then x in rng p by TARSKI:def_1;
hence contradiction by A4, A5, A7, TARSKI:def_1; ::_thesis: verum
end;
then A13: len q > 1 by A1, A9, A10, A11, XXREAL_0:1;
then consider n, m being String of (SingleGrammar (a,b)) such that
A14: q . 1 = n and
A15: q . (1 + 1) = m and
A16: n ==> m by A12;
x ==> m by A1, A10, A14, A16, Th4;
then [x,m] in {[a,<*b*>]} by A2, Def1;
then [x,m] = [a,<*b*>] by TARSKI:def_1;
then A17: m = <*b*> by XTUPLE_0:1;
A18: now__::_thesis:_not_2_<_len_q
assume 2 < len q ; ::_thesis: contradiction
then consider k, l being String of (SingleGrammar (a,b)) such that
A19: q . 2 = k and
q . (2 + 1) = l and
A20: k ==> l by A12;
y ==> l by A15, A17, A19, A20, Th4;
then [y,l] in {[a,<*b*>]} by A2, Def1;
then [y,l] = [a,<*b*>] by TARSKI:def_1;
hence contradiction by A4, XTUPLE_0:1; ::_thesis: verum
end;
len q >= 1 + 1 by A13, NAT_1:13;
then c = <*b*> by A6, A11, A15, A17, A18, XXREAL_0:1;
hence c in {<*b*>} by TARSKI:def_1; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in {<*b*>} or c in Lang (SingleGrammar (a,b)) )
assume c in {<*b*>} ; ::_thesis: c in Lang (SingleGrammar (a,b))
then A21: c = <*b*> by TARSKI:def_1;
rng <*b*> = {b} by FINSEQ_1:38;
hence c in Lang (SingleGrammar (a,b)) by A5, A21, A3; ::_thesis: verum
end;
theorem Th14: :: LANG1:14
for a, b being set st a <> b holds
Terminals (IterGrammar (a,b)) = {b}
proof
let a, b be set ; ::_thesis: ( a <> b implies Terminals (IterGrammar (a,b)) = {b} )
set T = IterGrammar (a,b);
assume A1: a <> b ; ::_thesis: Terminals (IterGrammar (a,b)) = {b}
A2: the carrier of (IterGrammar (a,b)) = {a,b} by Def9;
then reconsider x = a, y = b as Symbol of (IterGrammar (a,b)) by TARSKI:def_2;
A3: the Rules of (IterGrammar (a,b)) = {[a,<*b,a*>],[a,{}]} by Def9;
thus Terminals (IterGrammar (a,b)) c= {b} :: according to XBOOLE_0:def_10 ::_thesis: {b} c= Terminals (IterGrammar (a,b))
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Terminals (IterGrammar (a,b)) or c in {b} )
assume c in Terminals (IterGrammar (a,b)) ; ::_thesis: c in {b}
then consider s being Symbol of (IterGrammar (a,b)) such that
A4: c = s and
A5: for n being FinSequence holds not s ==> n ;
[a,<*b,a*>] in the Rules of (IterGrammar (a,b)) by A3, TARSKI:def_2;
then x ==> <*y,x*> by Def1;
then s <> x by A5;
then c = b by A2, A4, TARSKI:def_2;
hence c in {b} by TARSKI:def_1; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in {b} or c in Terminals (IterGrammar (a,b)) )
assume c in {b} ; ::_thesis: c in Terminals (IterGrammar (a,b))
then A6: b = c by TARSKI:def_1;
assume not c in Terminals (IterGrammar (a,b)) ; ::_thesis: contradiction
then consider n being FinSequence such that
A7: y ==> n by A6;
A8: [a,{}] <> [b,n] by A1, XTUPLE_0:1;
[a,<*b,a*>] <> [b,n] by A1, XTUPLE_0:1;
then not [b,n] in {[a,<*b,a*>],[a,{}]} by A8, TARSKI:def_2;
hence contradiction by A3, A7, Def1; ::_thesis: verum
end;
theorem :: LANG1:15
for a, b being set st a <> b holds
Lang (IterGrammar (a,b)) = {b} *
proof
let a, b be set ; ::_thesis: ( a <> b implies Lang (IterGrammar (a,b)) = {b} * )
set T = IterGrammar (a,b);
set I = <* the InitialSym of (IterGrammar (a,b))*>;
defpred S1[ Element of NAT ] means for p being String of (IterGrammar (a,b)) st len p = $1 & p in {b} * holds
p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*>;
A1: the carrier of (IterGrammar (a,b)) = {a,b} by Def9;
assume a <> b ; ::_thesis: Lang (IterGrammar (a,b)) = {b} *
then A2: Terminals (IterGrammar (a,b)) = {b} by Th14;
thus Lang (IterGrammar (a,b)) c= {b} * :: according to XBOOLE_0:def_10 ::_thesis: {b} * c= Lang (IterGrammar (a,b))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Lang (IterGrammar (a,b)) or a in {b} * )
assume a in Lang (IterGrammar (a,b)) ; ::_thesis: a in {b} *
then consider p being String of (IterGrammar (a,b)) such that
A3: a = p and
A4: rng p c= Terminals (IterGrammar (a,b)) and
p is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> ;
p is FinSequence of {b} by A2, A4, FINSEQ_1:def_4;
hence a in {b} * by A3, FINSEQ_1:def_11; ::_thesis: verum
end;
A5: the InitialSym of (IterGrammar (a,b)) = a by Def9;
A6: the Rules of (IterGrammar (a,b)) = {[a,<*b,a*>],[a,{}]} by Def9;
then [a,{}] in the Rules of (IterGrammar (a,b)) by TARSKI:def_2;
then the InitialSym of (IterGrammar (a,b)) ==> <*> the carrier of (IterGrammar (a,b)) by A5, Def1;
then A7: <* the InitialSym of (IterGrammar (a,b))*> ==> <*> the carrier of (IterGrammar (a,b)) by Th3;
A8: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: for p being String of (IterGrammar (a,b)) st len p = k & p in {b} * holds
p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> ; ::_thesis: S1[k + 1]
let p be String of (IterGrammar (a,b)); ::_thesis: ( len p = k + 1 & p in {b} * implies p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> )
assume that
A10: len p = k + 1 and
A11: p in {b} * ; ::_thesis: p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*>
consider q being FinSequence, c being set such that
A12: p = q ^ <*c*> and
A13: len q = k by A10, TREES_2:3;
A14: rng <*c*> = {c} by FINSEQ_1:38;
A15: p is FinSequence of {b} by A11, FINSEQ_1:def_11;
then A16: q is FinSequence of {b} by A12, FINSEQ_1:36;
<*c*> is FinSequence of the carrier of (IterGrammar (a,b)) by A12, FINSEQ_1:36;
then A17: {c} c= the carrier of (IterGrammar (a,b)) by A14, FINSEQ_1:def_4;
<*c*> is FinSequence of {b} by A12, A15, FINSEQ_1:36;
then {c} c= {b} by A14, FINSEQ_1:def_4;
then reconsider c = c as Element of {b} by ZFMISC_1:31;
reconsider x = c as Symbol of (IterGrammar (a,b)) by A17, ZFMISC_1:31;
A18: q is FinSequence of the carrier of (IterGrammar (a,b)) by A12, FINSEQ_1:36;
A19: [a,<*b,a*>] in the Rules of (IterGrammar (a,b)) by A6, TARSKI:def_2;
reconsider q = q as String of (IterGrammar (a,b)) by A18, FINSEQ_1:def_11;
c = b by TARSKI:def_1;
then the InitialSym of (IterGrammar (a,b)) ==> <*x, the InitialSym of (IterGrammar (a,b))*> by A5, A19, Def1;
then <* the InitialSym of (IterGrammar (a,b))*> ==> <*x, the InitialSym of (IterGrammar (a,b))*> by Th3;
then A20: q ^ <* the InitialSym of (IterGrammar (a,b))*> ==> q ^ <*x, the InitialSym of (IterGrammar (a,b))*> by Th5;
<*x, the InitialSym of (IterGrammar (a,b))*> = <*x*> ^ <* the InitialSym of (IterGrammar (a,b))*> by FINSEQ_1:def_9;
then q ^ <* the InitialSym of (IterGrammar (a,b))*> ==> p ^ <* the InitialSym of (IterGrammar (a,b))*> by A12, A20, FINSEQ_1:32;
then A21: p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from q ^ <* the InitialSym of (IterGrammar (a,b))*> by Th7;
q in {b} * by A16, FINSEQ_1:def_11;
then q ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> by A9, A13;
hence p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> by A21, Th8; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in {b} * or c in Lang (IterGrammar (a,b)) )
assume A22: c in {b} * ; ::_thesis: c in Lang (IterGrammar (a,b))
then reconsider c = c as FinSequence of {b} by FINSEQ_1:def_11;
{b} c= {a,b} by ZFMISC_1:7;
then rng c c= {a,b} by XBOOLE_1:1;
then c is FinSequence of the carrier of (IterGrammar (a,b)) by A1, FINSEQ_1:def_4;
then reconsider n = c as String of (IterGrammar (a,b)) by FINSEQ_1:def_11;
n ^ {} = n by FINSEQ_1:34;
then n ^ <* the InitialSym of (IterGrammar (a,b))*> ==> n by A7, Th5;
then A23: n is_derivable_from n ^ <* the InitialSym of (IterGrammar (a,b))*> by Th7;
A24: S1[ 0 ]
proof
let p be String of (IterGrammar (a,b)); ::_thesis: ( len p = 0 & p in {b} * implies p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> )
assume len p = 0 ; ::_thesis: ( not p in {b} * or p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> )
then p = {} ;
then p ^ <* the InitialSym of (IterGrammar (a,b))*> = <* the InitialSym of (IterGrammar (a,b))*> by FINSEQ_1:34;
hence ( not p in {b} * or p ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> ) by Th6; ::_thesis: verum
end;
A25: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A8);
len n = len n ;
then n ^ <* the InitialSym of (IterGrammar (a,b))*> is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> by A25, A22;
then A26: n is_derivable_from <* the InitialSym of (IterGrammar (a,b))*> by A23, Th8;
rng c c= {b} ;
hence c in Lang (IterGrammar (a,b)) by A2, A26; ::_thesis: verum
end;
theorem Th16: :: LANG1:16
for D being non empty set holds Terminals (TotalGrammar D) = D
proof
let D be non empty set ; ::_thesis: Terminals (TotalGrammar D) = D
set T = TotalGrammar D;
A1: the Rules of (TotalGrammar D) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} by Def10;
A2: the carrier of (TotalGrammar D) = succ D by Def10;
thus Terminals (TotalGrammar D) c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= Terminals (TotalGrammar D)
proof
reconsider b = D as Symbol of (TotalGrammar D) by Def10;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Terminals (TotalGrammar D) or a in D )
assume a in Terminals (TotalGrammar D) ; ::_thesis: a in D
then consider s being Symbol of (TotalGrammar D) such that
A3: a = s and
A4: for n being FinSequence holds not s ==> n ;
[D,{}] in {[D,{}]} by TARSKI:def_1;
then [D,{}] in the Rules of (TotalGrammar D) by A1, XBOOLE_0:def_3;
then b ==> <*> the carrier of (TotalGrammar D) by Def1;
then s <> D by A4;
then not s in {D} by TARSKI:def_1;
hence a in D by A2, A3, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in Terminals (TotalGrammar D) )
assume a in D ; ::_thesis: a in Terminals (TotalGrammar D)
then reconsider a = a as Element of D ;
reconsider x = a as Symbol of (TotalGrammar D) by A2, XBOOLE_0:def_3;
assume not a in Terminals (TotalGrammar D) ; ::_thesis: contradiction
then consider n being FinSequence such that
A5: x ==> n ;
A6: not a in a ;
then a <> D ;
then [a,n] <> [D,{}] by XTUPLE_0:1;
then A7: not [a,n] in {[D,{}]} by TARSKI:def_1;
[a,n] in the Rules of (TotalGrammar D) by A5, Def1;
then [a,n] in { [D,<*d,D*>] where d is Element of D : d = d } by A1, A7, XBOOLE_0:def_3;
then ex d being Element of D st
( [a,n] = [D,<*d,D*>] & d = d ) ;
then a = D by XTUPLE_0:1;
hence contradiction by A6; ::_thesis: verum
end;
theorem :: LANG1:17
for D being non empty set holds Lang (TotalGrammar D) = D *
proof
let D be non empty set ; ::_thesis: Lang (TotalGrammar D) = D *
set T = TotalGrammar D;
set I = <* the InitialSym of (TotalGrammar D)*>;
defpred S1[ Element of NAT ] means for p being String of (TotalGrammar D) st len p = $1 & p in D * holds
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>;
A1: D c= succ D by XBOOLE_1:7;
A2: the Rules of (TotalGrammar D) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} by Def10;
A3: the InitialSym of (TotalGrammar D) = D by Def10;
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: for p being String of (TotalGrammar D) st len p = k & p in D * holds
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> ; ::_thesis: S1[k + 1]
let p be String of (TotalGrammar D); ::_thesis: ( len p = k + 1 & p in D * implies p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> )
assume that
A6: len p = k + 1 and
A7: p in D * ; ::_thesis: p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
consider q being FinSequence, a being set such that
A8: p = q ^ <*a*> and
A9: len q = k by A6, TREES_2:3;
A10: rng <*a*> = {a} by FINSEQ_1:38;
<*a*> is FinSequence of the carrier of (TotalGrammar D) by A8, FINSEQ_1:36;
then A11: {a} c= the carrier of (TotalGrammar D) by A10, FINSEQ_1:def_4;
A12: q is FinSequence of the carrier of (TotalGrammar D) by A8, FINSEQ_1:36;
A13: p is FinSequence of D by A7, FINSEQ_1:def_11;
then A14: q is FinSequence of D by A8, FINSEQ_1:36;
<*a*> is FinSequence of D by A8, A13, FINSEQ_1:36;
then A15: {a} c= D by A10, FINSEQ_1:def_4;
reconsider q = q as String of (TotalGrammar D) by A12, FINSEQ_1:def_11;
reconsider a = a as Element of D by A15, ZFMISC_1:31;
reconsider x = a as Symbol of (TotalGrammar D) by A11, ZFMISC_1:31;
[D,<*a,D*>] in { [D,<*d,D*>] where d is Element of D : d = d } ;
then [D,<*a,D*>] in the Rules of (TotalGrammar D) by A2, XBOOLE_0:def_3;
then the InitialSym of (TotalGrammar D) ==> <*x, the InitialSym of (TotalGrammar D)*> by A3, Def1;
then <* the InitialSym of (TotalGrammar D)*> ==> <*x, the InitialSym of (TotalGrammar D)*> by Th3;
then A16: q ^ <* the InitialSym of (TotalGrammar D)*> ==> q ^ <*x, the InitialSym of (TotalGrammar D)*> by Th5;
<*x, the InitialSym of (TotalGrammar D)*> = <*x*> ^ <* the InitialSym of (TotalGrammar D)*> by FINSEQ_1:def_9;
then q ^ <* the InitialSym of (TotalGrammar D)*> ==> p ^ <* the InitialSym of (TotalGrammar D)*> by A8, A16, FINSEQ_1:32;
then A17: p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from q ^ <* the InitialSym of (TotalGrammar D)*> by Th7;
q in D * by A14, FINSEQ_1:def_11;
then q ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> by A5, A9;
hence p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> by A17, Th8; ::_thesis: verum
end;
[D,{}] in {[D,{}]} by TARSKI:def_1;
then [D,{}] in the Rules of (TotalGrammar D) by A2, XBOOLE_0:def_3;
then the InitialSym of (TotalGrammar D) ==> <*> the carrier of (TotalGrammar D) by A3, Def1;
then A18: <* the InitialSym of (TotalGrammar D)*> ==> <*> the carrier of (TotalGrammar D) by Th3;
A19: Terminals (TotalGrammar D) = D by Th16;
thus Lang (TotalGrammar D) c= D * :: according to XBOOLE_0:def_10 ::_thesis: D * c= Lang (TotalGrammar D)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Lang (TotalGrammar D) or a in D * )
assume a in Lang (TotalGrammar D) ; ::_thesis: a in D *
then consider p being String of (TotalGrammar D) such that
A20: a = p and
A21: rng p c= Terminals (TotalGrammar D) and
p is_derivable_from <* the InitialSym of (TotalGrammar D)*> ;
p is FinSequence of D by A19, A21, FINSEQ_1:def_4;
hence a in D * by A20, FINSEQ_1:def_11; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D * or a in Lang (TotalGrammar D) )
assume A22: a in D * ; ::_thesis: a in Lang (TotalGrammar D)
then reconsider a = a as FinSequence of D by FINSEQ_1:def_11;
the carrier of (TotalGrammar D) = succ D by Def10;
then rng a c= the carrier of (TotalGrammar D) by A1, XBOOLE_1:1;
then a is FinSequence of the carrier of (TotalGrammar D) by FINSEQ_1:def_4;
then reconsider n = a as String of (TotalGrammar D) by FINSEQ_1:def_11;
n ^ {} = n by FINSEQ_1:34;
then n ^ <* the InitialSym of (TotalGrammar D)*> ==> n by A18, Th5;
then A23: n is_derivable_from n ^ <* the InitialSym of (TotalGrammar D)*> by Th7;
A24: S1[ 0 ]
proof
let p be String of (TotalGrammar D); ::_thesis: ( len p = 0 & p in D * implies p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> )
assume len p = 0 ; ::_thesis: ( not p in D * or p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> )
then p = {} ;
then p ^ <* the InitialSym of (TotalGrammar D)*> = <* the InitialSym of (TotalGrammar D)*> by FINSEQ_1:34;
hence ( not p in D * or p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> ) by Th6; ::_thesis: verum
end;
A25: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A4);
len n = len n ;
then n ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> by A25, A22;
then A26: n is_derivable_from <* the InitialSym of (TotalGrammar D)*> by A23, Th8;
rng a c= D ;
hence a in Lang (TotalGrammar D) by A19, A26; ::_thesis: verum
end;
definition
let IT be non empty GrammarStr ;
attrIT is efective means :Def11: :: LANG1:def 11
( not Lang IT is empty & the InitialSym of IT in NonTerminals IT & ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT & s in rng p ) ) );
end;
:: deftheorem Def11 defines efective LANG1:def_11_:_
for IT being non empty GrammarStr holds
( IT is efective iff ( not Lang IT is empty & the InitialSym of IT in NonTerminals IT & ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT & s in rng p ) ) ) );
definition
let IT be GrammarStr ;
attrIT is finite means :: LANG1:def 12
the Rules of IT is finite ;
end;
:: deftheorem defines finite LANG1:def_12_:_
for IT being GrammarStr holds
( IT is finite iff the Rules of IT is finite );
registration
cluster non empty efective finite for GrammarStr ;
existence
ex b1 being non empty GrammarStr st
( b1 is efective & b1 is finite )
proof
take G = EmptyGrammar 0; ::_thesis: ( G is efective & G is finite )
A1: the Rules of G = {[0,{}]} by Def7;
the carrier of G = {0} by Def7;
then A2: the InitialSym of G = 0 by TARSKI:def_1;
[0,{}] in {[0,{}]} by TARSKI:def_1;
then the InitialSym of G ==> <*> the carrier of G by A1, A2, Def1;
then A3: the InitialSym of G in NonTerminals G ;
A4: for s being Symbol of G st s in Terminals G holds
ex p being String of G st
( p in Lang G & s in rng p ) by Th10;
not Lang G is empty by Th11;
hence G is efective by A3, A4, Def11; ::_thesis: G is finite
thus the Rules of G is finite by A1; :: according to LANG1:def_12 ::_thesis: verum
end;
end;
definition
let G be non empty efective GrammarStr ;
:: original: NonTerminals
redefine func NonTerminals G -> non empty Subset of G;
coherence
NonTerminals G is non empty Subset of G
proof
NonTerminals G c= the carrier of G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NonTerminals G or a in the carrier of G )
assume a in NonTerminals G ; ::_thesis: a in the carrier of G
then ex s being Symbol of G st
( a = s & ex n being FinSequence st s ==> n ) ;
hence a in the carrier of G ; ::_thesis: verum
end;
hence NonTerminals G is non empty Subset of G by Def11; ::_thesis: verum
end;
end;
definition
let X, Y be non empty set ;
let p be FinSequence of X;
let f be Function of X,Y;
:: original: *
redefine funcf * p -> Element of Y * ;
coherence
p * f is Element of Y *
proof
rng p c= X ;
then reconsider g = p as Function of (dom p),X by FUNCT_2:def_1, RELSET_1:4;
A1: rng (f * g) c= Y ;
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
dom (f * g) = dom p by FUNCT_2:def_1;
then f * g is FinSequence by A2, FINSEQ_1:def_2;
then f * g is FinSequence of Y by A1, FINSEQ_1:def_4;
hence p * f is Element of Y * by FINSEQ_1:def_11; ::_thesis: verum
end;
end;
definition
let X, Y be non empty set ;
let f be Function of X,Y;
funcf * -> Function of (X *),(Y *) means :: LANG1:def 13
for p being Element of X * holds it . p = f * p;
existence
ex b1 being Function of (X *),(Y *) st
for p being Element of X * holds b1 . p = f * p
proof
deffunc H1( Element of X * ) -> Element of Y * = f * $1;
consider g being Function of (X *),(Y *) such that
A1: for x being Element of X * holds g . x = H1(x) from FUNCT_2:sch_4();
take g ; ::_thesis: for p being Element of X * holds g . p = f * p
thus for p being Element of X * holds g . p = f * p by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (X *),(Y *) st ( for p being Element of X * holds b1 . p = f * p ) & ( for p being Element of X * holds b2 . p = f * p ) holds
b1 = b2
proof
let f1, f2 be Function of (X *),(Y *); ::_thesis: ( ( for p being Element of X * holds f1 . p = f * p ) & ( for p being Element of X * holds f2 . p = f * p ) implies f1 = f2 )
assume that
A2: for p being Element of X * holds f1 . p = f * p and
A3: for p being Element of X * holds f2 . p = f * p ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_X_*_holds_f1_._x_=_f2_._x
let x be Element of X * ; ::_thesis: f1 . x = f2 . x
thus f1 . x = f * x by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines * LANG1:def_13_:_
for X, Y being non empty set
for f being Function of X,Y
for b4 being Function of (X *),(Y *) holds
( b4 = f * iff for p being Element of X * holds b4 . p = f * p );
theorem :: LANG1:18
for R being Relation holds R c= R [*]
proof
let R be Relation; ::_thesis: R c= R [*]
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in R [*] )
let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in R [*] )
A1: len <*x,y*> = 2 by FINSEQ_1:44;
A2: <*x,y*> . 2 = y by FINSEQ_1:44;
assume A3: [x,y] in R ; ::_thesis: [x,y] in R [*]
then A4: y in field R by RELAT_1:15;
A5: <*x,y*> . 1 = x by FINSEQ_1:44;
A6: now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<_2_holds_
[(<*x,y*>_._i),(<*x,y*>_._(i_+_1))]_in_R
let i be Nat; ::_thesis: ( i >= 1 & i < 2 implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R )
assume that
A7: i >= 1 and
A8: i < 2 ; ::_thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R
1 + 1 = 2 ;
then i <= 1 by A8, NAT_1:13;
then i = 1 by A7, XXREAL_0:1;
hence [(<*x,y*> . i),(<*x,y*> . (i + 1))] in R by A3, A5, FINSEQ_1:44; ::_thesis: verum
end;
x in field R by A3, RELAT_1:15;
hence [x,y] in R [*] by A4, A1, A5, A2, A6, FINSEQ_1:def_16; ::_thesis: verum
end;
definition
let X be non empty set ;
let R be Relation of X;
:: original: [*]
redefine funcR [*] -> Relation of X;
coherence
R [*] is Relation of X
proof
[:X,X:] c= [:X,X:] ;
then reconsider P = [:X,X:] as Relation of X ;
R [*] c= P
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R [*] or [x,b1] in P )
let y be set ; ::_thesis: ( not [x,y] in R [*] or [x,y] in P )
A1: field R c= X \/ X by RELSET_1:8;
assume A2: [x,y] in R [*] ; ::_thesis: [x,y] in P
then A3: y in field R by FINSEQ_1:def_16;
x in field R by A2, FINSEQ_1:def_16;
hence [x,y] in P by A3, A1, ZFMISC_1:87; ::_thesis: verum
end;
hence R [*] is Relation of X ; ::_thesis: verum
end;
end;
definition
let G be non empty GrammarStr ;
let X be non empty set ;
let f be Function of the carrier of G,X;
funcG . f -> strict GrammarStr equals :: LANG1:def 14
GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #);
correctness
coherence
GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #) is strict GrammarStr ;
;
end;
:: deftheorem defines . LANG1:def_14_:_
for G being non empty GrammarStr
for X being non empty set
for f being Function of the carrier of G,X holds G . f = GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #);