lang1.miz



    begin

    definition

      struct ( 1-sorted) DTConstrStr (# the carrier -> set,

the Rules -> Relation of the carrier, ( the carrier * ) #)

       attr strict strict;

    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 (# the carrier -> set,

the InitialSym -> Element of the carrier,

the Rules -> Relation of the carrier, ( the carrier * ) #)

       attr strict strict;

    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;

      :: LANG1:def1

      pred s ==> n means [s, n] in the Rules of G;

    end

    definition

      let G;

      :: LANG1:def2

      func Terminals G -> set equals { s : not ex n be FinSequence st s ==> n };

      coherence ;

      :: LANG1:def3

      func NonTerminals G -> set equals { s : ex n be FinSequence st s ==> n };

      coherence ;

    end

    theorem :: LANG1:1

    (( Terminals G) \/ ( NonTerminals G)) = the carrier of G

    proof

      thus (( Terminals G) \/ ( NonTerminals G)) c= the carrier of G

      proof

        let a be object;

        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 be FinSequence st s ==> n) or ex s st a = s & ex n be FinSequence st s ==> n;

        hence thesis;

      end;

      let a be object;

      assume a in the carrier of G;

      then

      reconsider s = a as Symbol of G;

       not (ex n be FinSequence st s ==> n) or ex n be 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;

      :: LANG1:def4

      pred n ==> m means ex n1,n2,n3 be 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 :: LANG1:2

    s ==> n implies ((n1 ^ <*s*>) ^ n2) ==> ((n1 ^ n) ^ n2);

    theorem :: LANG1:3

    

     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 :: LANG1:4

    

     Th4: <*s*> ==> n implies s ==> n

    proof

      given n1,n2,n3 be String of G, t be 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 :: LANG1:5

    

     Th5: n1 ==> n2 implies (n ^ n1) ==> (n ^ n2) & (n1 ^ n) ==> (n2 ^ n)

    proof

      given m1,m2,m3 be String of G, s be 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;

      :: LANG1:def5

      pred m is_derivable_from n means ex p be FinSequence st ( len p) >= 1 & (p . 1) = n & (p . ( len p)) = m & for i be Element of NAT st i >= 1 & i < ( len p) holds ex a,b be String of G st (p . i) = a & (p . (i + 1)) = b & a ==> b;

    end

    theorem :: LANG1:6

    

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

    

     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 :: LANG1:8

    

     Th8: n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1 is_derivable_from n3

    proof

      given p1 be FinSequence such that

       A1: ( len p1) >= 1 and

       A2: (p1 . 1) = n2 and

       A3: (p1 . ( len p1)) = n1 and

       A4: for i be Element of NAT st i >= 1 & i < ( len p1) holds ex a,b be String of G st (p1 . i) = a & (p1 . (i + 1)) = b & a ==> b;

      given p2 be FinSequence such that

       A5: ( len p2) >= 1 and

       A6: (p2 . 1) = n3 and

       A7: (p2 . ( len p2)) = n2 and

       A8: for i be Element of NAT st i >= 1 & i < ( len p2) holds ex a,b be String of G st (p2 . i) = a & (p2 . (i + 1)) = b & a ==> b;

      p2 <> {} by A5;

      then

      consider q be FinSequence, x be object 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 be 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 be 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 be 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 be 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;

    definition

      let G be non empty GrammarStr;

      :: LANG1:def6

      func Lang (G) -> set equals { a where a be Element of (the carrier of G * ) : ( rng a) c= ( Terminals G) & a is_derivable_from <*the InitialSym of G*> };

      coherence ;

    end

    theorem :: LANG1:9

    for G be non empty GrammarStr, n be 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 be 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;

    definition

      let D,E be non empty set, a be Element of [:D, E:];

      :: original: {

      redefine

      func {a} -> Relation of D, E ;

      coherence

      proof

         {a} c= [:D, E:];

        hence thesis;

      end;

      let b be Element of [:D, E:];

      :: original: {

      redefine

      func {a,b} -> Relation of D, E ;

      coherence

      proof

         {a, b} c= [:D, E:];

        hence thesis;

      end;

    end

    definition

      let a be set;

      :: LANG1:def7

      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;

      :: LANG1:def8

      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 ;

      :: LANG1:def9

      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;

      :: LANG1:def10

      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 be 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 be Element of D : d = d };

        R c= [:E, (E * ):]

        proof

          let a be object;

          assume a in R;

          then

          consider d be 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 :: LANG1:10

    

     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 be Symbol of E such that b = s and

       A2: not ex n be 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;

      hence contradiction by A2;

    end;

    theorem :: LANG1:11

    

     Th11: ( Lang ( EmptyGrammar a)) = { {} }

    proof

      set E = ( EmptyGrammar a);

      

       A1: ( Terminals E) = {} by Th10;

      thus ( Lang E) c= { {} }

      proof

        let b be object;

        assume b in ( Lang E);

        then ex p be 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 be object;

      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;

      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 :: LANG1:12

    

     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;

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

      thus ( Terminals E) c= {b}

      proof

        let c be object;

        assume c in ( Terminals E);

        then

        consider s be Symbol of E such that

         A6: c = s and

         A7: not ex n be 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 be object;

      assume c in {b};

      then c = b by TARSKI:def 1;

      hence thesis by A4;

    end;

    theorem :: LANG1:13

    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;

      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 be object;

        assume c in ( Lang E);

        then

        consider p be 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 be 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 be Element of NAT st i >= 1 & i < ( len q) holds ex a,b be String of E st (q . i) = a & (q . (i + 1)) = b & a ==> b by A8;

        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 be 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;

        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 be 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;

          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 be object;

      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 :: LANG1:14

    

     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 be object;

        assume c in ( Terminals T);

        then

        consider s be Symbol of T such that

         A4: c = s and

         A5: not ex n be FinSequence st s ==> n;

         [a, <*b, a*>] in the Rules of T by A3, TARSKI:def 2;

        then x ==> <*y, x*>;

        then s <> x by A5;

        then c = b by A2, A4, TARSKI:def 2;

        hence thesis by TARSKI:def 1;

      end;

      let c be object;

      assume c in {b};

      then

       A6: b = c by TARSKI:def 1;

      assume not thesis;

      then

      consider n be 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;

    end;

    theorem :: LANG1:15

    a <> b implies ( Lang ( IterGrammar (a,b))) = ( {b} * )

    proof

      set T = ( IterGrammar (a,b));

      set I = <*the InitialSym of T*>;

      defpred X[ Nat] means for p be 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 be object;

        assume a in ( Lang T);

        then

        consider p be 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;

      then

       A7: I ==> ( <*> the carrier of T) by Th3;

      

       A8: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A9: for p be 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 be 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;

        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 be object;

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

      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 be Nat holds X[k] from NAT_1:sch 2( 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 :: LANG1:16

    

     Th16: ( Terminals ( TotalGrammar D)) = D

    proof

      set T = ( TotalGrammar D);

      

       A1: the Rules of T = ({ [D, <*d, D*>] where d be 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 be object;

        assume a in ( Terminals T);

        then

        consider s be Symbol of T such that

         A3: a = s and

         A4: not ex n be 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);

        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 be object;

      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 be 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;

      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 :: LANG1:17

    ( Lang ( TotalGrammar D)) = (D * )

    proof

      set T = ( TotalGrammar D);

      set I = <*the InitialSym of T*>;

      defpred X[ Nat] means for p be 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 be Element of D : d = d } \/ { [D, {} ]}) by Def10;

      

       A3: the InitialSym of T = D by Def10;

      

       A4: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A5: for p be 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 be 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;

        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;

      then

       A18: I ==> ( <*> the carrier of T) by Th3;

      

       A19: ( Terminals T) = D by Th16;

      thus ( Lang T) c= (D * )

      proof

        let a be object;

        assume a in ( Lang T);

        then

        consider p be 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 be object;

      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;

      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 be Nat holds X[k] from NAT_1:sch 2( 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;

      :: LANG1:def11

      attr IT is effective means

      : Def11: ( Lang IT) is non empty & the InitialSym of IT in ( NonTerminals IT) & for s be Symbol of IT st s in ( Terminals IT) holds ex p be String of IT st p in ( Lang IT) & s in ( rng p);

    end

    definition

      let IT be GrammarStr;

      :: LANG1:def12

      attr IT is finite means the Rules of IT is finite;

    end

    registration

      cluster effective 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;

        then

         A3: the InitialSym of G in ( NonTerminals G);

        

         A4: for s be Symbol of G st s in ( Terminals G) holds ex p be String of G st p in ( Lang G) & s in ( rng p) by Th10;

        ( Lang G) is non empty by Th11;

        hence G is effective by A3, A4;

        thus the Rules of G is finite by A1;

      end;

    end

    definition

      let G be effective non empty GrammarStr;

      :: original: NonTerminals

      redefine

      func NonTerminals G -> non empty Subset of G ;

      coherence

      proof

        ( NonTerminals G) c= the carrier of G

        proof

          let a be object;

          assume a in ( NonTerminals G);

          then ex s be Symbol of G st a = s & ex n be 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;

      :: original: *

      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;

      :: LANG1:def13

      func f * -> Function of (X * ), (Y * ) means for p be Element of (X * ) holds (it . p) = (f * p);

      existence

      proof

        deffunc U( Element of (X * )) = (f * $1);

        consider g be Function of (X * ), (Y * ) such that

         A1: for x be 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 be Element of (X * ) holds (f1 . p) = (f * p) and

         A3: for p be 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 :: LANG1:18

    R c= (R [*] )

    proof

      let x,y be object;

      

       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;

      :: original: [*]

      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 be object;

          

           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;

      :: LANG1:def14

      func G . f -> strict GrammarStr equals GrammarStr (# X, (f . the InitialSym of G), (((f ~ ) * the Rules of G) * (f * )) #);

      correctness ;

    end