:: 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 *)) #);