:: Context-Free Grammar - Part 1
::  by Patricia L. Carlson and Grzegorz Bancerek
::
:: Received February 21, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, STRUCT_0, RELAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1,
      TDGROUP, TARSKI, ORDINAL4, ARYTM_3, CARD_1, FUNCT_1, XXREAL_0, NAT_1,
      ZFMISC_1, ORDINAL1, FINSET_1, LANG1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
      DOMAIN_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, FINSET_1, RELSET_1,
      PARTFUN1, FUNCT_2, FINSEQ_2, XXREAL_0, PRE_POLY;
 constructors PARTFUN1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0,
      RELSET_1, PRE_POLY;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
      XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, ORDINAL1, CARD_1, RELSET_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions XBOOLE_0, TARSKI, RELAT_1, STRUCT_0, ORDINAL1;
 theorems TARSKI, ZFMISC_1, RELAT_1, FINSEQ_1, NAT_1, RELSET_1, TREES_2,
      FUNCT_2, FINSEQ_3, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1,
      XTUPLE_0;
 schemes NAT_1, FUNCT_2;

begin

:: Grammar structure is introduced as triple (S, I, R) where S is
:: a set of non-terminal and terminal symbols, I is an initial symbol,
:: and R is a set of rules (ordered pairs).

definition
  struct(1-sorted) DTConstrStr (# carrier -> set, Rules -> Relation of the
    carrier, (the carrier)* #);
end;

registration
  cluster non empty strict for DTConstrStr;
  existence
  proof
    set A = the non empty set,P = the Relation of A,A*;
    take DTConstrStr(#A,P#);
    thus the carrier of DTConstrStr(#A,P#) is non empty;
    thus thesis;
  end;
end;

definition
  struct(DTConstrStr) GrammarStr (# carrier -> set, InitialSym -> Element of
    the carrier, Rules -> Relation of the carrier, (the carrier)* #);
end;

registration
  cluster non empty for GrammarStr;
  existence
  proof
    set A = the non empty set,P = the Relation of A,A*,I = the Element of A;
    take GrammarStr(#A,I,P#);
    thus the carrier of GrammarStr(#A,I,P#) is non empty;
  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;

reserve G for non empty DTConstrStr,
  s for Symbol of G,
  n,m for String of G;

definition
  let G,s;
  let n be FinSequence;
  pred s ==> n means
  :Def1:
  [s,n] in the Rules of G;
end;

definition
  let G;
  func Terminals G equals
  { s : not ex n being FinSequence st s ==> n};
  coherence;
  func NonTerminals G equals
  { s : ex n being FinSequence st s ==> n};
  coherence;
end;

theorem
  Terminals(G) \/ NonTerminals(G) = the carrier of G
proof
  thus Terminals G \/ NonTerminals G c= the carrier of G
  proof
    let a be set;
    assume a in Terminals G \/ NonTerminals G;
    then a in Terminals G or a in NonTerminals G by XBOOLE_0:def 3;
    then
    (ex s st a = s & not ex n being FinSequence st s ==> n) or ex s st a =
    s & ex n being FinSequence st s ==> n;
    hence thesis;
  end;
  let a be set;
  assume a in the carrier of G;
  then reconsider s = a as Symbol of G;
  not (ex n being FinSequence st s ==> n) or ex n being FinSequence st s ==> n;
  then a in Terminals G or a in NonTerminals G;
  hence thesis by XBOOLE_0:def 3;
end;

definition
  let G,n,m;
  pred n ==> m means
  ex n1,n2,n3 being String of G, s st n = n1^<*s*>^n2 & m =
  n1^n3^n2 & s ==> n3;
end;

reserve n1,n2,n3 for String of G;

theorem
  s ==> n implies n1^<*s*>^n2 ==> n1^n^n2
proof
  assume
A1: s ==> n;
  take n1,n2,n,s;
  thus thesis by A1;
end;

theorem Th3:
  s ==> n implies <*s*> ==> n
proof
  assume
A1: s ==> n;
  take n1 = <*>(the carrier of G), n2 = <*>(the carrier of G), n3 = n, s;
  thus <*s*> = n1^<*s*> by FINSEQ_1:34
    .= n1^<*s*>^n2 by FINSEQ_1:34;
  thus n = n1^n3 by FINSEQ_1:34
    .= n1^n3^n2 by FINSEQ_1:34;
  thus thesis by A1;
end;

theorem Th4:
  <*s*> ==> n implies s ==> n
proof
  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;
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 thesis by A1,A2,A3,A7,A12,A11,A9,A8,A10,FINSEQ_1:40;
end;

theorem Th5:
  n1 ==> n2 implies n^n1 ==> n^n2 & n1^n ==> n2^n
proof
  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;
  thus n^n1 ==> n^n2
  proof
    take n^m1, m2, m3, s;
    thus n^n1 = n^(m1^<*s*>)^m2 by A1,FINSEQ_1:32
      .= n^m1^<*s*>^m2 by FINSEQ_1:32;
    thus n^n2 = n^(m1^m3)^m2 by A2,FINSEQ_1:32
      .= n^m1^m3^m2 by FINSEQ_1:32;
    thus thesis by A3;
  end;
  take m1, m2^n, m3, s;
  thus thesis by A1,A2,A3,FINSEQ_1:32;
end;

definition
  let G, n, m;
  pred m is_derivable_from n means
  :Def5:
  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 ex a
  ,b being String of G st p.i = a & p.(i+1) = b & a ==> b;
end;

theorem Th6:
  n is_derivable_from n
proof
  take p = <*n*>;
  len p = 1 by FINSEQ_1:40;
  hence len p >= 1 & p.1 = n & p.len p = n by FINSEQ_1:40;
  let i be Element of NAT;
  assume that
A1: i >= 1 and
A2: i < len p;
  thus thesis by A1,A2,FINSEQ_1:40;
end;

theorem Th7:
  n ==> m implies m is_derivable_from n
proof
  assume
A1: n ==> m;
  take p = <*n,m*>;
A2: len p = 2 by FINSEQ_1:44;
  hence len p >= 1 & p.1 = n & p.(len p) = m by FINSEQ_1:44;
  let i be Element of NAT;
  assume that
A3: i >= 1 and
A4: i < len p;
  take a = n, b = m;
  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;
  thus p.(i+1) = b by A5,FINSEQ_1:44;
  thus thesis by A1;
end;

theorem Th8:
  n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1
  is_derivable_from n3
proof
  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 ex a,b being
  String of G st p1.i = a & p1.(i+1) = b & a ==> b;
  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 ex a,b being
  String of G st p2.i = a & p2.(i+1) = b & a ==> b;
  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;
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;
  now
    per cases;
    suppose
A12:  q = {};
      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;
    end;
    suppose
A14:  q <> {};
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;
    end;
  end;
  hence p.1 = n3;
  len p1 in dom p1 by A1,FINSEQ_3:25;
  hence p.(len p) = n1 by A3,A11,FINSEQ_1:def 7;
  let i be Element of NAT such that
A17: i >= 1 and
A18: i < len p;
  len <*x*> = 1 by FINSEQ_1:40;
  then
A19: len p2 = len q + 1 by A9,FINSEQ_1:22;
  now
    per cases by XXREAL_0:1;
    suppose
A20:  i+1 = len p2;
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, 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;
    end;
    suppose
      i+1 > len p2;
      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 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, 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;
    end;
    suppose
A35:  i+1 < len p2;
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, 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;
    end;
  end;
  hence thesis;
end;

:: Define language

definition
  let G be non empty GrammarStr;
  func Lang(G) equals
  {a where a is Element of (the carrier of G)*: rng a c=
  Terminals(G) & a is_derivable_from <*the InitialSym of G*>};
  coherence;
end;

theorem
  for G being non empty GrammarStr, 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, n be String of G;
  now
    assume n in Lang 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*>;
  end;
  hence thesis;
end;

:: GrammarStr(#{a},a,{[a,{}{a}]}#)             -> Lang = {{}}
:: GrammarStr(#{a,b},a,{[a,<*b*>]}#)            -> Lang = {b}
:: GrammarStr(#{a,b},a,{[a,{}{a}],[a,<*a,b*>]}#) -> Lang = {{}, b, bb, ...}
:: GrammarStr(#{a,b,c},a,{[a,<*b*>}],[a,<*c*>]}#) -> Lang = {b, c}

definition
  let D,E be non empty set, a be Element of [:D,E:];
  redefine func {a} -> Relation of D,E;
  coherence
  proof
    {a} c= [:D,E:];
    hence thesis;
  end;
  let b be Element of [:D,E:];
  redefine func {a,b} -> Relation of D,E;
  coherence
  proof
    {a,b} c= [:D,E:];
    hence thesis;
  end;
end;

definition
  let a be set;
  func EmptyGrammar a -> strict GrammarStr means
  :Def7:
  the carrier of it = {a } & the Rules of it = {[a,{}]};
  existence
  proof
    reconsider S = a as Element of {a} by TARSKI:def 1;
    take GrammarStr(#{a}, S, {[S,<*>{a}]}#);
    thus thesis;
  end;
  uniqueness
  proof
    let G1, G2 be strict GrammarStr such 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,{}]};
    the InitialSym of G1 = a by A1,TARSKI:def 1;
    hence thesis by A1,A2,A3,A4,TARSKI:def 1;
  end;
  let b be set;
  func SingleGrammar(a,b) -> strict GrammarStr means
  :Def8:
  the carrier of it
  = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]};
  existence
  proof
    reconsider S = a, x = b as Element of {a,b} by TARSKI:def 2;
    take GrammarStr(#{a,b}, S, {[S,<*x*>]}#);
    thus thesis;
  end;
  uniqueness;
  func IterGrammar(a,b) -> strict GrammarStr means
  :Def9:
  the carrier of it =
  {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]};
  existence
  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}]}#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let a be set;
  cluster EmptyGrammar a -> non empty;
  coherence
  proof
    the carrier of EmptyGrammar a = {a} by Def7;
    hence the carrier of EmptyGrammar a is non empty;
  end;
  let b be set;
  cluster SingleGrammar(a,b) -> non empty;
  coherence
  proof
    the carrier of SingleGrammar(a,b) = {a,b} by Def8;
    hence the carrier of SingleGrammar(a,b) is non empty;
  end;
  cluster IterGrammar(a,b) -> non empty;
  coherence
  proof
    the carrier of IterGrammar(a,b) = {a,b} by Def9;
    hence the carrier of IterGrammar(a,b) is non empty;
  end;
end;

definition
  let D be non empty set;
  func TotalGrammar D -> strict GrammarStr means
  : Def10:
  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
  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};
    R c= [:E,E*:]
    proof
      let a be set;
      assume a in R;
      then consider d being Element of D such that
A1:   a = [S,<*d,S*>] and
      d = d;
      reconsider d as Element of E by XBOOLE_0:def 3;
      a = [S,<*d,S*>] by A1;
      hence thesis;
    end;
    then reconsider R as Relation of E, E*;
    take GrammarStr(#E, S, R \/ {[S,<*>E]}#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let D be non empty set;
  cluster TotalGrammar D -> non empty;
  coherence
  proof
    the carrier of TotalGrammar D = succ D by Def10;
    hence the carrier of TotalGrammar D is non empty;
  end;
end;

reserve a,b,c for set,
  D for non empty set,
  d for Element of D;

theorem Th10:
  Terminals EmptyGrammar a = {}
proof
  set E = EmptyGrammar a;
  set b = the Element of Terminals E;
  the Rules of E = {[a,{}]} by Def7;
  then
A1: [a,{}] in the Rules of E by TARSKI:def 1;
  assume not thesis;
  then b in Terminals E;
  then consider s being Symbol of E such that
  b = s and
A2: not ex n being FinSequence st s ==> n;
  the carrier of E = {a} by Def7;
  then s = a by TARSKI:def 1;
  then s ==> <*>the carrier of E by A1,Def1;
  hence contradiction by A2;
end;

theorem Th11:
  Lang EmptyGrammar a = {{}}
proof
  set E = EmptyGrammar a;
A1: Terminals E = {} by Th10;
  thus Lang E c= {{}}
  proof
    let b;
    assume b in Lang E;
    then ex p being String of E st b = p & rng p c= Terminals E & p
    is_derivable_from <*the InitialSym of E*>;
    then b = {} by A1;
    hence thesis by TARSKI:def 1;
  end;
  let b;
  assume b in {{}};
  then
A2: b = {} by TARSKI:def 1;
  the Rules of E = {[a,{}]} by Def7;
  then
A3: [a,{}] in the Rules of E by TARSKI:def 1;
  the carrier of E = {a} by Def7;
  then a = the InitialSym of E by TARSKI:def 1;
  then the InitialSym of E ==> <*> the carrier of E by A3,Def1;
  then
A4: <*> the carrier of E is_derivable_from <*the InitialSym of E*> by Th3,Th7;
  rng {} = {};
  hence thesis by A1,A2,A4;
end;

theorem Th12:
  a <> b implies Terminals SingleGrammar(a,b) = {b}
proof
  set E = SingleGrammar(a,b);
A1: the Rules of E = {[a,<*b*>]} by Def8;
A2: the carrier of E = {a,b} by Def8;
  then reconsider x = a, y = b as Symbol of E by TARSKI:def 2;
  assume
A3: a <> b;
A4: now
    let n be FinSequence;
    assume y ==> n;
    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;
  end;
  [x,<*y*>] in the Rules of E by A1,TARSKI:def 1;
  then
A5: x ==> <*y*> by Def1;
  thus Terminals E c= {b}
  proof
    let c;
    assume c in Terminals E;
    then consider s being Symbol of E such that
A6: c = s and
A7: not ex n being FinSequence st s ==> n;
    s <> x by A5,A7;
    then c = b by A2,A6,TARSKI:def 2;
    hence thesis by TARSKI:def 1;
  end;
  let c;
  assume c in {b};
  then c = b by TARSKI:def 1;
  hence thesis by A4;
end;

theorem
  a <> b implies Lang SingleGrammar(a,b) = {<*b*>}
proof
  set E = SingleGrammar(a,b);
A1: the InitialSym of E = a by Def8;
  the carrier of E = {a,b} by Def8;
  then reconsider x = a, y = b as Symbol of E by TARSKI:def 2;
A2: the Rules of E = {[a,<*b*>]} by Def8;
  then [a,<*b*>] in the Rules of E by TARSKI:def 1;
  then the InitialSym of E ==> <*y*> by A1,Def1;
  then
A3: <*y*> is_derivable_from <*the InitialSym of E*> by Th3,Th7;
  assume
A4: a <> b;
  then
A5: Terminals E = {b} by Th12;
  thus Lang E c= {<*b*>}
  proof
    let c;
    assume c in Lang E;
    then consider p being String of E such that
A6: c = p and
A7: rng p c= Terminals E and
A8: p is_derivable_from <*the InitialSym of E*>;
    consider q being FinSequence such that
A9: len q >= 1 and
A10: q.1 = <*the InitialSym of E*> and
A11: q.(len q) = p and
A12: for i being Element of NAT st i >= 1 & i < len q ex a,b being
    String of E st q.i = a & q.(i+1) = b & a ==> b by A8,Def5;
    now
      assume p = <*x*>;
      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;
    end;
    then
A13: len q > 1 by A1,A9,A10,A11,XXREAL_0:1;
    then consider n, m being String of E 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
      assume 2 < len q;
      then consider k, l being String of E 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;
    end;
    len q >= 1+1 by A13,NAT_1:13;
    then c = <*b*> by A6,A11,A15,A17,A18,XXREAL_0:1;
    hence thesis by TARSKI:def 1;
  end;
  let c;
  assume c in {<*b*>};
  then
A21: c = <*b*> by TARSKI:def 1;
  rng <*b*> = {b} by FINSEQ_1:38;
  hence thesis by A5,A21,A3;
end;

theorem Th14:
  a <> b implies Terminals IterGrammar(a,b) = {b}
proof
  set T = IterGrammar(a,b);
  assume
A1: a <> b;
A2: the carrier of T = {a,b} by Def9;
  then reconsider x = a, y = b as Symbol of T by TARSKI:def 2;
A3: the Rules of T = {[a,<*b,a*>],[a,{}]} by Def9;
  thus Terminals T c= {b}
  proof
    let c;
    assume c in Terminals T;
    then consider s being Symbol of T such that
A4: c = s and
A5: not ex n being FinSequence st s ==> n;
    [a,<*b,a*>] in the Rules of T 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 thesis by TARSKI:def 1;
  end;
  let c;
  assume c in {b};
  then
A6: b = c by TARSKI:def 1;
  assume not thesis;
  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 thesis by A3,A7,Def1;
end;

theorem
  a <> b implies Lang IterGrammar(a,b) = {b}*
proof
  set T = IterGrammar(a,b);
  set I = <*the InitialSym of T*>;
  defpred X[Element of NAT] means for p being String of T st len p = $1 & p in
  {b}* holds p^I is_derivable_from I;
A1: the carrier of T = {a,b} by Def9;
  assume a <> b;
  then
A2: Terminals T = {b} by Th14;
  thus Lang T c= {b}*
  proof
    let a;
    assume a in Lang T;
    then consider p being String of T such that
A3: a = p and
A4: rng p c= Terminals T and
    p is_derivable_from <*the InitialSym of T*>;
    p is FinSequence of {b} by A2,A4,FINSEQ_1:def 4;
    hence thesis by A3,FINSEQ_1:def 11;
  end;
A5: the InitialSym of T = a by Def9;
A6: the Rules of T = {[a,<*b,a*>],[a,{}]} by Def9;
  then [a,{}] in the Rules of T by TARSKI:def 2;
  then the InitialSym of T ==> <*> the carrier of T by A5,Def1;
  then
A7: I ==> <*> the carrier of T by Th3;
A8: for k being Element of NAT st X[k] holds X[k+1]
  proof
    let k be Element of NAT such that
A9: for p being String of T st len p = k & p in {b}* holds p^I
    is_derivable_from I;
    let p be String of T;
    assume that
A10: len p = k+1 and
A11: p in {b}*;
    consider q being FinSequence, c 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 T by A12,FINSEQ_1:36;
    then
A17: {c} c= the carrier of T 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 as Element of {b} by ZFMISC_1:31;
    reconsider x = c as Symbol of T by A17,ZFMISC_1:31;
A18: q is FinSequence of the carrier of T by A12,FINSEQ_1:36;
A19: [a,<*b,a*>] in the Rules of T by A6,TARSKI:def 2;
    reconsider q as String of T by A18,FINSEQ_1:def 11;
    c = b by TARSKI:def 1;
    then the InitialSym of T ==> <*x,the InitialSym of T*> by A5,A19,Def1;
    then I ==> <*x,the InitialSym of T*> by Th3;
    then
A20: q^I ==> q^<*x,the InitialSym of T*> by Th5;
    <*x,the InitialSym of T*> = <*x*>^I by FINSEQ_1:def 9;
    then q^I ==> p^I by A12,A20,FINSEQ_1:32;
    then
A21: p^I is_derivable_from q^I by Th7;
    q in {b}* by A16,FINSEQ_1:def 11;
    then q^I is_derivable_from I by A9,A13;
    hence thesis by A21,Th8;
  end;
  let c;
  assume
A22: c in {b}*;
  then reconsider 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 T by A1,FINSEQ_1:def 4;
  then reconsider n = c as String of T by FINSEQ_1:def 11;
  n^{} = n by FINSEQ_1:34;
  then n^I ==> n by A7,Th5;
  then
A23: n is_derivable_from n^I by Th7;
A24: X[0]
  proof
    let p be String of T;
    assume len p = 0;
    then p = {};
    then p^I = I by FINSEQ_1:34;
    hence thesis by Th6;
  end;
A25: for k being Element of NAT holds X[k] from NAT_1:sch 1(A24,A8);
  len n = len n;
  then n^I is_derivable_from I by A25,A22;
  then
A26: n is_derivable_from I by A23,Th8;
  rng c c= {b};
  hence thesis by A2,A26;
end;

theorem Th16:
  Terminals TotalGrammar D = D
proof
  set T = TotalGrammar D;
A1: the Rules of T = {[D,<*d,D*>] where d is Element of D: d = d} \/ {[D,{}]
  } by Def10;
A2: the carrier of T = succ D by Def10;
  thus Terminals T c= D
  proof
    reconsider b = D as Symbol of T by Def10;
    let a;
    assume a in Terminals T;
    then consider s being Symbol of T such that
A3: a = s and
A4: not ex n being FinSequence st s ==> n;
    [D,{}] in {[D,{}]} by TARSKI:def 1;
    then [D,{}] in the Rules of T by A1,XBOOLE_0:def 3;
    then b ==> <*> the carrier of T by Def1;
    then s <> D by A4;
    then not s in {D} by TARSKI:def 1;
    hence thesis by A2,A3,XBOOLE_0:def 3;
  end;
  let a;
  assume a in D;
  then reconsider a as Element of D;
  reconsider x = a as Symbol of T by A2,XBOOLE_0:def 3;
  assume not thesis;
  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 T by A5,Def1;
  then [a,n] in {[D,<*d,D*>]: d = d} by A1,A7,XBOOLE_0:def 3;
  then ex d st [a,n] = [D,<*d,D*>] & d = d;
  then a = D by XTUPLE_0:1;
  hence thesis by A6;
end;

theorem
  Lang TotalGrammar D = D*
proof
  set T = TotalGrammar D;
  set I = <*the InitialSym of T*>;
  defpred X[Element of NAT] means for p being String of T st len p = $1 & p in
  D* holds p^I is_derivable_from I;
A1: D c= succ D by XBOOLE_1:7;
A2: the Rules of T = {[D,<*d,D*>] where d is Element of D: d = d} \/ {[D,{}]
  } by Def10;
A3: the InitialSym of T = D by Def10;
A4: for k being Element of NAT st X[k] holds X[k+1]
  proof
    let k be Element of NAT such that
A5: for p being String of T st len p = k & p in D* holds p^I
    is_derivable_from I;
    let p be String of T;
    assume that
A6: len p = k+1 and
A7: p in D*;
    consider q being FinSequence, a 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 T by A8,FINSEQ_1:36;
    then
A11: {a} c= the carrier of T by A10,FINSEQ_1:def 4;
A12: q is FinSequence of the carrier of T 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 as String of T by A12,FINSEQ_1:def 11;
    reconsider a as Element of D by A15,ZFMISC_1:31;
    reconsider x = a as Symbol of T by A11,ZFMISC_1:31;
    [D,<*a,D*>] in {[D,<*d,D*>]: d = d};
    then [D,<*a,D*>] in the Rules of T by A2,XBOOLE_0:def 3;
    then the InitialSym of T ==> <*x,the InitialSym of T*> by A3,Def1;
    then I ==> <*x,the InitialSym of T*> by Th3;
    then
A16: q^I ==> q^<*x,the InitialSym of T*> by Th5;
    <*x,the InitialSym of T*> = <*x*>^I by FINSEQ_1:def 9;
    then q^I ==> p^I by A8,A16,FINSEQ_1:32;
    then
A17: p^I is_derivable_from q^I by Th7;
    q in D* by A14,FINSEQ_1:def 11;
    then q^I is_derivable_from I by A5,A9;
    hence thesis by A17,Th8;
  end;
  [D,{}] in {[D,{}]} by TARSKI:def 1;
  then [D,{}] in the Rules of T by A2,XBOOLE_0:def 3;
  then the InitialSym of T ==> <*> the carrier of T by A3,Def1;
  then
A18: I ==> <*> the carrier of T by Th3;
A19: Terminals T = D by Th16;
  thus Lang T c= D*
  proof
    let a;
    assume a in Lang T;
    then consider p being String of T such that
A20: a = p and
A21: rng p c= Terminals T and
    p is_derivable_from <*the InitialSym of T*>;
    p is FinSequence of D by A19,A21,FINSEQ_1:def 4;
    hence thesis by A20,FINSEQ_1:def 11;
  end;
  let a;
  assume
A22: a in D*;
  then reconsider a as FinSequence of D by FINSEQ_1:def 11;
  the carrier of T = succ D by Def10;
  then rng a c= the carrier of T by A1,XBOOLE_1:1;
  then a is FinSequence of the carrier of T by FINSEQ_1:def 4;
  then reconsider n = a as String of T by FINSEQ_1:def 11;
  n^{} = n by FINSEQ_1:34;
  then n^I ==> n by A18,Th5;
  then
A23: n is_derivable_from n^I by Th7;
A24: X[0]
  proof
    let p be String of T;
    assume len p = 0;
    then p = {};
    then p^I = I by FINSEQ_1:34;
    hence thesis by Th6;
  end;
A25: for k being Element of NAT holds X[k] from NAT_1:sch 1(A24,A4);
  len n = len n;
  then n^I is_derivable_from I by A25,A22;
  then
A26: n is_derivable_from I by A23,Th8;
  rng a c= D;
  hence thesis by A19,A26;
end;

definition
  let IT be non empty GrammarStr;
  attr IT is efective means
  :Def11:
  Lang IT is non empty & the InitialSym of
  IT in NonTerminals IT & for s being Symbol of IT st s in Terminals IT ex p
  being String of IT st p in Lang(IT) & s in rng p;
end;

definition
  let IT be GrammarStr;
  attr IT is finite means
  the Rules of IT is finite;
end;

registration
  cluster efective finite for non empty GrammarStr;
  existence
  proof
    take G = EmptyGrammar 0;
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 ex p being String of G st p
    in Lang(G) & s in rng p by Th10;
    Lang(G) is non empty by Th11;
    hence G is efective by A3,A4,Def11;
    thus the Rules of G is finite by A1;
  end;
end;

definition
  let G be efective non empty GrammarStr;
  redefine func NonTerminals G -> non empty Subset of G;
  coherence
  proof
    NonTerminals G c= the carrier of G
    proof
      let a be set;
      assume a in NonTerminals G;
      then
      ex s being Symbol of G st a = s & ex n being FinSequence st s ==> n;
      hence thesis;
    end;
    hence thesis by Def11;
  end;
end;

definition
  let X,Y be non empty set, p be FinSequence of X, f be Function of X,Y;
  redefine func f*p -> Element of Y*;
  coherence
  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 thesis by FINSEQ_1:def 11;
  end;
end;

definition
  let X,Y be non empty set;
  let f be Function of X,Y;

  func f* -> Function of X*,Y* means
  for p being Element of X* holds it.p = f* p;
  existence
  proof
    deffunc U(Element of X*) = f*$1;
    consider g being Function of X*,Y* such that
A1: for x being Element of X* holds g.x = U(x) from FUNCT_2:sch 4;
    take g;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f1,f2 be Function of X*,Y* such 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;
    now
      let x be Element of X*;
      thus f1.x = f*x by A2
        .= f2.x by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

reserve R for Relation,
  x,y for set;

theorem
  R c= R[*]
proof
  let x,y;
A1: len <*x,y*> = 2 by FINSEQ_1:44;
A2: <*x,y*>.2 = y by FINSEQ_1:44;
  assume
A3: [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
    let i be Nat such that
A7: i >= 1 and
A8: i < 2;
    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;
  end;
  x in field R by A3,RELAT_1:15;
  hence thesis by A4,A1,A5,A2,A6,FINSEQ_1:def 16;
end;

definition
  let X be non empty set, R be Relation of X;
  redefine func R[*] -> Relation of X;
  coherence
  proof
    [:X,X:] c= [:X,X:];
    then reconsider P = [:X,X:] as Relation of X;
    R[*] c= P
    proof
      let x,y;
A1:   field R c= X \/ X by RELSET_1:8;
      assume
A2:   [x,y] in R[*];
      then
A3:   y in field R by FINSEQ_1:def 16;
      x in field R by A2,FINSEQ_1:def 16;
      hence thesis by A3,A1,ZFMISC_1:87;
    end;
    hence thesis;
  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;
  func G.f -> strict GrammarStr equals
  GrammarStr (#X, f.the InitialSym of G,
    (f)~*(the Rules of G)*(f*) #);
  correctness;
end;
 
:: The goal is to show:
::   f is_one-to-one implies f*.:Lang(G) = Lang(G.f)