dtconstr.miz



    begin

    deffunc T( set) = 0 ;

    deffunc A( set, set, set) = 0 ;

    theorem :: DTCONSTR:1

    

     Th1: for D be non empty set, p be FinSequence of ( FinTrees D) holds p is FinSequence of ( Trees D)

    proof

      let D be non empty set;

      ( FinTrees D) is non empty Subset of ( Trees D) by TREES_3: 21;

      hence thesis by FINSEQ_2: 24;

    end;

    theorem :: DTCONSTR:2

    

     Th2: for x,y be set, p be FinSequence of x st y in ( dom p) holds (p . y) in x

    proof

      let x,y be set;

      let p be FinSequence of x;

      assume y in ( dom p);

      then

       A1: (p . y) in ( rng p) by FUNCT_1:def 3;

      ( rng p) c= x by FINSEQ_1:def 4;

      hence thesis by A1;

    end;

    registration

      let D be non empty set, T be DTree-set of D;

      cluster -> DTree-yielding for FinSequence of T;

      coherence ;

    end

    definition

      let D be non empty set;

      let F be non empty DTree-set of D;

      let Tset be non empty Subset of F;

      :: original: Element

      redefine

      mode Element of Tset -> Element of F ;

      coherence

      proof

        let x be Element of Tset;

        thus thesis;

      end;

    end

    definition

      let D be non empty set, T be DTree-set of D;

      let p be FinSequence of T;

      :: original: roots

      redefine

      func roots p -> FinSequence of D ;

      coherence

      proof

        let x be object;

        assume x in ( rng ( roots p));

        then

        consider k be object such that

         A1: k in ( dom ( roots p)) and

         A2: x = (( roots p) . k) by FUNCT_1:def 3;

        reconsider k as Element of NAT by A1;

        

         A3: ( dom ( roots p)) = ( dom p) by TREES_3:def 18;

        then

        consider t be DecoratedTree such that

         A4: t = (p . k) and

         A5: (( roots p) . k) = (t . {} ) by A1, TREES_3:def 18;

        reconsider t as DecoratedTree of D by A1, A3, A4, Th2, TREES_3:def 6;

        reconsider r = {} as Node of t by TREES_1: 22;

        (t . r) in D;

        hence thesis by A2, A5;

      end;

    end

    

     Lm1: ( dom ( roots {} )) = ( dom {} ) by TREES_3:def 18

    .= {} ;

    theorem :: DTCONSTR:3

    

     Th3: ( roots {} ) = {} by Lm1;

    theorem :: DTCONSTR:4

    

     Th4: for T be DecoratedTree holds ( roots <*T*>) = <*(T . {} )*>

    proof

      let T be DecoratedTree;

      

       A1: ( dom <*T*>) = ( Seg 1) by FINSEQ_1:def 8;

      

       A2: ( dom <*(T . {} )*>) = ( Seg 1) by FINSEQ_1:def 8;

      

       A3: ( <*T*> . 1) = T by FINSEQ_1:def 8;

      

       A4: ( <*(T . {} )*> . 1) = (T . {} ) by FINSEQ_1:def 8;

      now

        let i be Element of NAT ;

        assume

         A5: i in ( dom <*T*>);

        take t = T;

        thus t = ( <*T*> . i) & ( <*(T . {} )*> . i) = (t . {} ) by A1, A3, A4, A5, FINSEQ_1: 2, TARSKI:def 1;

      end;

      hence thesis by A1, A2, TREES_3:def 18;

    end;

    theorem :: DTCONSTR:5

    

     Th5: for D be non empty set, F be Subset of ( FinTrees D), p be FinSequence of F st ( len ( roots p)) = 1 holds ex x be Element of ( FinTrees D) st p = <*x*> & x in F

    proof

      let D be non empty set, F be Subset of ( FinTrees D), p be FinSequence of F;

      assume ( len ( roots p)) = 1;

      then

       A1: ( dom ( roots p)) = ( Seg 1) by FINSEQ_1:def 3;

      

       A2: ( dom p) = ( dom ( roots p)) by TREES_3:def 18;

      then

       A3: 1 in ( dom p) by A1;

      then

      reconsider x = (p . 1) as Element of ( FinTrees D) by Th2;

      take x;

      thus thesis by A1, A2, A3, Th2, FINSEQ_1:def 8;

    end;

    theorem :: DTCONSTR:6

    for T1,T2 be DecoratedTree holds ( roots <*T1, T2*>) = <*(T1 . {} ), (T2 . {} )*>

    proof

      let T1,T2 be DecoratedTree;

      

       A1: ( len <*T1, T2*>) = 2 by FINSEQ_1: 44;

      

       A2: ( len <*(T1 . {} ), (T2 . {} )*>) = 2 by FINSEQ_1: 44;

      

       A3: ( <*T1, T2*> . 1) = T1 by FINSEQ_1: 44;

      

       A4: ( <*(T1 . {} ), (T2 . {} )*> . 1) = (T1 . {} ) by FINSEQ_1: 44;

      

       A5: ( <*T1, T2*> . 2) = T2 by FINSEQ_1: 44;

      

       A6: ( <*(T1 . {} ), (T2 . {} )*> . 2) = (T2 . {} ) by FINSEQ_1: 44;

      

       A7: ( dom <*T1, T2*>) = ( Seg 2) by A1, FINSEQ_1:def 3;

      

       A8: ( dom <*(T1 . {} ), (T2 . {} )*>) = ( Seg 2) by A2, FINSEQ_1:def 3;

      now

        let i be Element of NAT ;

        assume i in ( dom <*T1, T2*>);

        then i in ( Seg 2) by A1, FINSEQ_1:def 3;

        then i = 1 or i = 2 by FINSEQ_1: 2, TARSKI:def 2;

        hence ex t be DecoratedTree st t = ( <*T1, T2*> . i) & ( <*(T1 . {} ), (T2 . {} )*> . i) = (t . {} ) by A3, A4, A5, A6;

      end;

      hence thesis by A7, A8, TREES_3:def 18;

    end;

    definition

      let X,Y be set, f be FinSequence of [:X, Y:];

      :: original: pr1

      redefine

      func pr1 f -> FinSequence of X ;

      coherence

      proof

        

         A1: ( dom ( pr1 f)) = ( dom f) by MCART_1:def 12;

        ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        then

        reconsider p = ( pr1 f) as FinSequence by A1, FINSEQ_1:def 2;

        ( rng p) c= X

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider i be object such that

           A2: i in ( dom p) and

           A3: x = (p . i) by FUNCT_1:def 3;

          

           A4: (f . i) in [:X, Y:] by A1, A2, Th2;

          x = ((f . i) `1 ) by A1, A2, A3, MCART_1:def 12;

          hence thesis by A4, MCART_1: 10;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

      :: original: pr2

      redefine

      func pr2 f -> FinSequence of Y ;

      coherence

      proof

        

         A5: ( dom ( pr2 f)) = ( dom f) by MCART_1:def 13;

        ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        then

        reconsider p = ( pr2 f) as FinSequence by A5, FINSEQ_1:def 2;

        ( rng p) c= Y

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider i be object such that

           A6: i in ( dom p) and

           A7: x = (p . i) by FUNCT_1:def 3;

          

           A8: (f . i) in [:X, Y:] by A5, A6, Th2;

          x = ((f . i) `2 ) by A5, A6, A7, MCART_1:def 13;

          hence thesis by A8, MCART_1: 10;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: DTCONSTR:7

    

     Th7: ( pr1 {} ) = {} & ( pr2 {} ) = {}

    proof

      set r = ( <*> [: {} , {} :]);

      ( dom ( pr1 r)) = ( dom {} )

      .= {} ;

      hence ( pr1 {} ) = {} ;

      ( dom ( pr2 r)) = ( dom {} )

      .= {} ;

      hence thesis;

    end;

    begin

    registration

      let A be non empty set, R be Relation of A, (A * );

      cluster DTConstrStr (# A, R #) -> non empty;

      coherence ;

    end

    scheme :: DTCONSTR:sch1

    DTConstrStrEx { S() -> non empty set , P[ object, object] } :

ex G be strict non empty DTConstrStr st the carrier of G = S() & for x be Symbol of G, p be FinSequence of the carrier of G holds x ==> p iff P[x, p];

      consider PR be Relation of S(), (S() * ) such that

       A1: for x,y be object holds [x, y] in PR iff x in S() & y in (S() * ) & P[x, y] from RELSET_1:sch 1;

      take DT = DTConstrStr (# S(), PR #);

      thus the carrier of DT = S();

      let x be Symbol of DT, p be FinSequence of the carrier of DT;

      hereby

        assume x ==> p;

        then [x, p] in the Rules of DT by LANG1:def 1;

        hence P[x, p] by A1;

      end;

      assume

       A2: P[x, p];

      p in (the carrier of DT * ) by FINSEQ_1:def 11;

      then [x, p] in PR by A1, A2;

      hence thesis by LANG1:def 1;

    end;

    scheme :: DTCONSTR:sch2

    DTConstrStrUniq { S() -> non empty set , P[ set, set] } :

for G1,G2 be strict non empty DTConstrStr st (the carrier of G1 = S() & for x be Symbol of G1, p be FinSequence of the carrier of G1 holds x ==> p iff P[x, p]) & (the carrier of G2 = S() & for x be Symbol of G2, p be FinSequence of the carrier of G2 holds x ==> p iff P[x, p]) holds G1 = G2;

      let G1,G2 be strict non empty DTConstrStr such that

       A1: the carrier of G1 = S() and

       A2: for x be Symbol of G1, p be FinSequence of the carrier of G1 holds x ==> p iff P[x, p] and

       A3: the carrier of G2 = S() and

       A4: for x be Symbol of G2, p be FinSequence of the carrier of G2 holds x ==> p iff P[x, p];

      now

        let x,y be object;

        hereby

          assume

           A5: [x, y] in the Rules of G1;

          then

           A6: y in (the carrier of G1 * ) by ZFMISC_1: 87;

          reconsider x1 = x as Symbol of G1 by A5, ZFMISC_1: 87;

          reconsider y1 = y as FinSequence of the carrier of G1 by A6, FINSEQ_2:def 3;

          

           A7: x1 ==> y1 iff P[x1, y1] by A2;

          reconsider x2 = x as Symbol of G2 by A1, A3, A5, ZFMISC_1: 87;

          reconsider y2 = y as FinSequence of the carrier of G2 by A1, A3, A6, FINSEQ_2:def 3;

          x2 ==> y2 by A4, A5, A7, LANG1:def 1;

          hence [x, y] in the Rules of G2 by LANG1:def 1;

        end;

        assume

         A8: [x, y] in the Rules of G2;

        then

         A9: y in (the carrier of G2 * ) by ZFMISC_1: 87;

        reconsider x2 = x as Symbol of G2 by A8, ZFMISC_1: 87;

        reconsider y2 = y as FinSequence of the carrier of G2 by A9, FINSEQ_2:def 3;

        

         A10: x2 ==> y2 iff P[x2, y2] by A4;

        reconsider x1 = x as Symbol of G1 by A1, A3, A8, ZFMISC_1: 87;

        reconsider y1 = y as FinSequence of the carrier of G1 by A1, A3, A9, FINSEQ_2:def 3;

        x1 ==> y1 by A2, A8, A10, LANG1:def 1;

        hence [x, y] in the Rules of G1 by LANG1:def 1;

      end;

      hence thesis by A1, A3, RELAT_1:def 2;

    end;

    theorem :: DTCONSTR:8

    for G be non empty DTConstrStr holds ( Terminals G) misses ( NonTerminals G)

    proof

      let G be non empty DTConstrStr;

      

       A1: ( Terminals G) = { t where t be Symbol of G : not ex tnt be FinSequence st t ==> tnt } by LANG1:def 2;

      

       A2: ( NonTerminals G) = { t where t be Symbol of G : ex tnt be FinSequence st t ==> tnt } by LANG1:def 3;

      assume not thesis;

      then

      consider x be object such that

       A3: x in ( Terminals G) and

       A4: x in ( NonTerminals G) by XBOOLE_0: 3;

      

       A5: ex t be Symbol of G st x = t & not ex tnt be FinSequence st t ==> tnt by A1, A3;

      ex t be Symbol of G st x = t & ex tnt be FinSequence st t ==> tnt by A2, A4;

      hence contradiction by A5;

    end;

    scheme :: DTCONSTR:sch3

    DTCMin { f() -> Function , G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() } :

ex X be Subset of ( FinTrees [:the carrier of G(), D():]) st X = ( Union f()) & (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, TermVal(d)]) in X) & (for o be Symbol of G(), p be FinSequence of X st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in X) & for F be Subset of ( FinTrees [:the carrier of G(), D():]) st (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, TermVal(d)]) in F) & (for o be Symbol of G(), p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in F) holds X c= F

      provided

       A1: ( dom f()) = NAT

       and

       A2: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) }

       and

       A3: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) });

      set f = f();

      set G = G();

      set D = D();

      deffunc NTV( Symbol of G, FinSequence) = NTermVal($1,pr1,pr2);

      ( Union f) c= ( FinTrees [:the carrier of G, D:])

      proof

        let u be object;

        assume u in ( Union f);

        then

         A4: ex k be object st (k in NAT ) & (u in (f . k)) by A1, CARD_5: 2;

        defpred P[ Nat] means for u be set st u in (f . $1) holds u in ( FinTrees [:the carrier of G, D:]);

        

         A5: P[ 0 ]

        proof

          let u be set;

          assume u in (f . 0 );

          then ex t be Symbol of G, d be Element of D st u = ( root-tree [t, d]) & (t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{})) by A2;

          hence thesis;

        end;

         A6:

        now

          let n be Nat such that

           A7: P[n];

          thus P[(n + 1)]

          proof

            let u be set;

            assume u in (f . (n + 1));

            then u in ((f . n) \/ { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

            then

             A8: u in (f . n) or u in { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st p = q & o ==> ( pr1 ( roots q)) } by XBOOLE_0:def 3;

            assume

             A9: not u in ( FinTrees [:the carrier of G, D:]);

            then

            consider o be Symbol of G, p be Element of ((f . n) * ) such that

             A10: u = ( [o, NTV(o,p)] -tree p) and

             A11: ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st p = q & o ==> ( pr1 ( roots q)) by A7, A8;

            reconsider p as FinSequence of ( FinTrees [:the carrier of G, D:]) by A11;

            u = ( [o, NTV(o,p)] -tree p) by A10;

            hence contradiction by A9;

          end;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A5, A6);

        hence thesis by A4;

      end;

      then

      reconsider X = ( Union f) as Subset of ( FinTrees [:the carrier of G, D:]);

      take X;

      thus X = ( Union f);

      hereby

        let d be Symbol of G;

        assume d in ( Terminals G);

        then ( root-tree [d, TermVal(d)]) in (f . 0 ) by A2;

        hence ( root-tree [d, TermVal(d)]) in X by A1, CARD_5: 2;

      end;

      hereby

        let o be Symbol of G, p be FinSequence of X such that

         A12: o ==> ( pr1 ( roots p));

        set s = ( pr1 ( roots p)), v = ( pr2 ( roots p));

        

         A13: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        defpred P[ set, set] means (p . $1) in (f . $2);

        

         A14: for x be Nat st x in ( Seg ( len p)) holds ex n be Element of NAT st P[x, n]

        proof

          let x be Nat;

          assume x in ( Seg ( len p));

          then

           A15: (p . x) in ( rng p) by A13, FUNCT_1:def 3;

          ( rng p) c= X by FINSEQ_1:def 4;

          then ex n be object st n in NAT & (p . x) in (f . n) by A1, A15, CARD_5: 2;

          hence thesis;

        end;

        consider pn be FinSequence of NAT such that

         A16: ( dom pn) = ( Seg ( len p)) & for k be Nat st k in ( Seg ( len p)) holds P[k, (pn . k)] from FINSEQ_1:sch 5( A14);

         A17:

        now

          defpred P[ Element of NAT , Element of NAT ] means $1 >= $2;

          assume ( rng pn) <> {} ;

          then

           A18: ( rng pn) is finite & ( rng pn) <> {} & ( rng pn) c= NAT by FINSEQ_1:def 4;

          

           A19: for x,y be Element of NAT holds P[x, y] or P[y, x];

          

           A20: for x,y,z be Element of NAT st P[x, y] & P[y, z] holds P[x, z] by XXREAL_0: 2;

          consider n be Element of NAT such that

           A21: n in ( rng pn) & for y be Element of NAT st y in ( rng pn) holds P[n, y] from CQC_SIM1:sch 4( A18, A19, A20);

          take n;

          thus ( rng p) c= (f . n)

          proof

            let t be object;

            assume t in ( rng p);

            then

            consider k be object such that

             A22: k in ( dom p) and

             A23: t = (p . k) by FUNCT_1:def 3;

            reconsider k as Element of NAT by A22;

            

             A24: (pn . k) in ( rng pn) by A13, A16, A22, FUNCT_1:def 3;

            then

            reconsider pnk = (pn . k) as Element of NAT by A18;

            consider s be Nat such that

             A25: n = (pnk + s) by A21, A24, NAT_1: 10;

            deffunc H( set, set) = { ( [o1, NTermVal(o1,pr1,pr2)] -tree p1) where o1 be Symbol of G(), p1 be Element of ((f . $1) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p1 = q & o1 ==> ( pr1 ( roots q)) };

            for n be Nat holds (f . n) c= (f . (n + 1))

            proof

              let n be Nat;

              (f . (n + 1)) = ((f . n) \/ H(n,.)) by A3;

              hence thesis by XBOOLE_1: 7;

            end;

            then

             A26: (f . pnk) c= (f . n) by A25, MEASURE2: 18, NAT_1: 11;

            t in (f . (pn . k)) by A13, A16, A22, A23;

            hence thesis by A26;

          end;

        end;

        now

          assume ( rng pn) = {} ;

          then pn = {} ;

          then p = {} by A16;

          then ( rng p) = {} ;

          hence ( rng p) c= (f . 0 );

        end;

        then

        consider n be Element of NAT such that

         A27: ( rng p) c= (f . n) by A17;

        

         A28: X = ( union ( rng f)) by CARD_3:def 4;

        (f . n) in ( rng f) by A1, FUNCT_1:def 3;

        then (f . n) c= X by A28, ZFMISC_1: 74;

        then

        reconsider fn = (f . n) as Subset of ( FinTrees [:the carrier of G, D:]) by XBOOLE_1: 1;

        reconsider q = p as FinSequence of fn by A27, FINSEQ_1:def 4;

        reconsider q9 = q as Element of (fn * ) by FINSEQ_1:def 11;

        ( [o, NTermVal(o,s,v)] -tree q9) in { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of (fn * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st pp = q & oo ==> ( pr1 ( roots q)) } by A12;

        then ( [o, NTermVal(o,s,v)] -tree q9) in ((f . n) \/ { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of (fn * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st pp = q & oo ==> ( pr1 ( roots q)) }) by XBOOLE_0:def 3;

        then ( [o, NTermVal(o,s,v)] -tree q9) in (f . (n + 1)) by A3;

        hence ( [o, NTermVal(o,s,v)] -tree p) in X by A1, CARD_5: 2;

      end;

      let F be Subset of ( FinTrees [:the carrier of G, D:]) such that

       A29: for d be Symbol of G st d in ( Terminals G) holds ( root-tree [d, TermVal(d)]) in F and

       A30: for o be Symbol of G, p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, NTV(o,p)] -tree p) in F;

      defpred P[ Nat] means (f . $1) c= F;

      

       A31: P[ 0 ]

      proof

        let x be object;

        reconsider p = ( <*> F) as FinSequence of F;

        assume x in (f . 0 );

        then

        consider t be Symbol of G, d be Element of D such that

         A32: x = ( root-tree [t, d]) and

         A33: t in ( Terminals G()) & d = TermVal(t) or t ==> ( pr1 ( roots p)) & d = NTV(t,p) by A2, Th3, Th7;

        ( [t, d] -tree p) = ( root-tree [t, d]) by TREES_4: 20;

        hence thesis by A29, A30, A32, A33;

      end;

       A34:

      now

        let n be Nat such that

         A35: P[n];

        thus P[(n + 1)]

        proof

          let x be object;

          assume that

           A36: x in (f . (n + 1)) and

           A37: not x in F;

          x in ((f . n) \/ { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st pp = q & oo ==> ( pr1 ( roots q)) }) by A3, A36;

          then x in (f . n) or x in { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st pp = q & oo ==> ( pr1 ( roots q)) } by XBOOLE_0:def 3;

          then

          consider o be Symbol of G, p be Element of ((f . n) * ) such that

           A38: x = ( [o, NTV(o,p)] -tree p) and

           A39: ex q be FinSequence of ( FinTrees [:the carrier of G, D:]) st p = q & o ==> ( pr1 ( roots q)) by A35, A37;

          ( rng p) c= (f . n) by FINSEQ_1:def 4;

          then ( rng p) c= F by A35, XBOOLE_1: 1;

          then

          reconsider p as FinSequence of F by FINSEQ_1:def 4;

          o ==> ( pr1 ( roots p)) by A39;

          hence contradiction by A30, A37, A38;

        end;

      end;

      

       A40: for n be Nat holds P[n] from NAT_1:sch 2( A31, A34);

      thus X c= F

      proof

        let x be object;

        assume x in X;

        then

        consider n be object such that

         A41: n in NAT and

         A42: x in (f . n) by A1, CARD_5: 2;

        (f . n) c= F by A40, A41;

        hence thesis by A42;

      end;

    end;

    scheme :: DTCONSTR:sch4

    DTCSymbols { f() -> Function , G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() } :

ex X1 be Subset of ( FinTrees the carrier of G()) st X1 = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G(), D():]) : t in ( Union f()) } & (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree d) in X1) & (for o be Symbol of G(), p be FinSequence of X1 st o ==> ( roots p) holds (o -tree p) in X1) & for F be Subset of ( FinTrees the carrier of G()) st (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree d) in F) & (for o be Symbol of G(), p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F) holds X1 c= F

      provided

       A1: ( dom f()) = NAT

       and

       A2: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) }

       and

       A3: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) });

      set f = f();

      set G = G();

      set D = D();

      set S = the carrier of G;

      set SxD = [:S, D:];

      deffunc NTV( Symbol of G, FinSequence) = NTermVal($1,pr1,pr2);

      

       A4: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) } by A2;

      

       A5: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

      consider X be Subset of ( FinTrees [:the carrier of G, D:]) such that

       A6: X = ( Union f) & (for d be Symbol of G st d in ( Terminals G) holds ( root-tree [d, TermVal(d)]) in X) & (for o be Symbol of G, p be FinSequence of X st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in X) & for F be Subset of ( FinTrees [:the carrier of G, D:]) st (for d be Symbol of G st d in ( Terminals G) holds ( root-tree [d, TermVal(d)]) in F) & (for o be Symbol of G, p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in F) holds X c= F from DTCMin( A1, A4, A5);

      set X9 = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G, D:]) : t in ( Union f) };

      X9 c= ( FinTrees the carrier of G)

      proof

        let x be object;

        assume x in X9;

        then

        consider tt be Element of ( FinTrees [:the carrier of G, D:]) such that

         A7: x = (tt `1 ) and tt in ( Union f);

        

         A8: (tt `1 ) = (( pr1 (the carrier of G,D)) * tt) by TREES_3:def 12;

        

         A9: ( rng tt) c= [:the carrier of G, D:] by RELAT_1:def 19;

        ( dom ( pr1 (the carrier of G,D))) = [:the carrier of G, D:] by FUNCT_2:def 1;

        then ( dom (tt `1 )) = ( dom tt) by A8, A9, RELAT_1: 27;

        hence thesis by A7, TREES_3:def 8;

      end;

      then

      reconsider X9 as Subset of ( FinTrees the carrier of G());

      take X1 = X9;

      thus X1 = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G, D:]) : t in ( Union f) };

      hereby

        let t be Symbol of G();

        assume

         A10: t in ( Terminals G());

        

         A11: (( root-tree [t, TermVal(t)]) `1 ) = ( root-tree t) by TREES_4: 25;

        ( root-tree [t, TermVal(t)]) in ( Union f) by A6, A10;

        hence ( root-tree t) in X1 by A11;

      end;

      hereby

        let nt be Symbol of G(), ts be FinSequence of X1;

        assume

         A12: nt ==> ( roots ts);

        

         A13: ( dom ts) = ( Seg ( len ts)) by FINSEQ_1:def 3;

        defpred P[ set, set] means ex dt be DecoratedTree of [:the carrier of G(), D():] st dt = $2 & (dt `1 ) = (ts . $1) & dt in ( Union f);

        

         A14: for k be Nat st k in ( Seg ( len ts)) holds ex x be Element of ( FinTrees [:the carrier of G, D:]) st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len ts));

          then

           A15: (ts . k) in ( rng ts) by A13, FUNCT_1:def 3;

          ( rng ts) c= X1 by FINSEQ_1:def 4;

          then (ts . k) in X1 by A15;

          then ex x be Element of ( FinTrees [:the carrier of G, D:]) st (ts . k) = (x `1 ) & x in ( Union f);

          hence thesis;

        end;

        consider dts be FinSequence of ( FinTrees [:the carrier of G, D:]) such that

         A16: ( dom dts) = ( Seg ( len ts)) and

         A17: for k be Nat st k in ( Seg ( len ts)) holds P[k, (dts . k)] from FINSEQ_1:sch 5( A14);

        ( rng dts) c= ( Union f)

        proof

          let x be object;

          assume x in ( rng dts);

          then

          consider k be object such that

           A18: k in ( dom ts) and

           A19: x = (dts . k) by A13, A16, FUNCT_1:def 3;

          reconsider k as Element of NAT by A18;

          ex dt be DecoratedTree of [:the carrier of G(), D():] st dt = x & (dt `1 ) = (ts . k) & dt in ( Union f) by A13, A17, A18, A19;

          hence thesis;

        end;

        then

        reconsider dts as FinSequence of X by A6, FINSEQ_1:def 4;

        

         A20: ( dom ( roots ts)) = ( dom ts) by TREES_3:def 18;

        

         A21: ( dom ( pr1 ( roots dts))) = ( dom ( roots dts)) by MCART_1:def 12;

        then

         A22: ( dom ( pr1 ( roots dts))) = ( dom ts) by A13, A16, TREES_3:def 18;

        now

          let k be Nat;

          assume

           A23: k in ( dom ts);

          then

          consider dt be DecoratedTree of [:the carrier of G(), D():] such that

           A24: dt = (dts . k) and

           A25: (dt `1 ) = (ts . k) and dt in ( Union f) by A13, A17;

          reconsider r = {} as Node of dt by TREES_1: 22;

          ex T be DecoratedTree st T = (ts . k) & (( roots ts) . k) = (T . {} ) by A23, TREES_3:def 18;

          then

           A26: (( roots ts) . k) = ((dt . r) `1 ) by A25, TREES_3: 39;

          ex T be DecoratedTree st T = (dts . k) & (( roots dts) . k) = (T . {} ) by A13, A16, A23, TREES_3:def 18;

          hence (( roots ts) . k) = (( pr1 ( roots dts)) . k) by A21, A22, A23, A24, A26, MCART_1:def 12;

        end;

        then ( roots ts) = ( pr1 ( roots dts)) by A20, A22, FINSEQ_1: 13;

        then

         A27: ( [nt, NTV(nt,dts)] -tree dts) in X by A6, A12;

        

         A28: ( rng dts) c= ( FinTrees [:the carrier of G(), D():]) by FINSEQ_1:def 4;

        ( FinTrees [:the carrier of G(), D():]) c= ( Trees [:the carrier of G(), D():]) by TREES_3: 21;

        then ( rng dts) c= ( Trees [:the carrier of G(), D():]) by A28;

        then

        reconsider dts9 = dts as FinSequence of ( Trees [:the carrier of G(), D():]) by FINSEQ_1:def 4;

        

         A29: ( rng ts) c= ( FinTrees the carrier of G()) by FINSEQ_1:def 4;

        ( FinTrees the carrier of G()) c= ( Trees the carrier of G()) by TREES_3: 21;

        then ( rng ts) c= ( Trees the carrier of G()) by A29;

        then

        reconsider ts9 = ts as FinSequence of ( Trees the carrier of G()) by FINSEQ_1:def 4;

        now

          let i be Nat;

          assume i in ( dom dts);

          then

           A30: ex dt be DecoratedTree of [:the carrier of G, D:] st (dt = (dts . i)) & ((dt `1 ) = (ts . i)) & (dt in ( Union f)) by A16, A17;

          let T be DecoratedTree of [:the carrier of G(), D():];

          assume T = (dts . i);

          hence (ts . i) = (T `1 ) by A30;

        end;

        then (( [nt, NTV(nt,dts)] -tree dts9) `1 ) = (nt -tree ts9) by A13, A16, TREES_4: 27;

        hence (nt -tree ts) in X1 by A6, A27;

      end;

      let F be Subset of ( FinTrees the carrier of G);

      assume that

       A31: for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in F and

       A32: for o be Symbol of G, p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F;

      thus X1 c= F

      proof

        let x be object;

        assume x in X1;

        then

        consider tt be Element of ( FinTrees [:the carrier of G, D:]) such that

         A33: x = (tt `1 ) and

         A34: tt in ( Union f);

        set FF = { dt where dt be Element of ( FinTrees SxD) : (dt `1 ) in F };

        FF c= ( FinTrees SxD)

        proof

          let x be object;

          assume x in FF;

          then ex dt be Element of ( FinTrees SxD) st x = dt & (dt `1 ) in F;

          hence thesis;

        end;

        then

        reconsider FF as Subset of ( FinTrees SxD);

         A35:

        now

          let d be Symbol of G;

          assume d in ( Terminals G);

          then

           A36: ( root-tree d) in F by A31;

          (( root-tree [d, TermVal(d)]) `1 ) = ( root-tree d) by TREES_4: 25;

          hence ( root-tree [d, TermVal(d)]) in FF by A36;

        end;

        now

          let o be Symbol of G, p be FinSequence of FF;

          assume

           A37: o ==> ( pr1 ( roots p));

          consider p1 be FinSequence of ( FinTrees S) such that

           A38: ( dom p1) = ( dom p) and

           A39: for i be Nat st i in ( dom p) holds ex T be Element of ( FinTrees SxD) st T = (p . i) & (p1 . i) = (T `1 ) and

           A40: (( [o, NTermVal(o,pr1,pr2)] -tree p) `1 ) = (o -tree p1) by TREES_4: 31;

          ( rng p1) c= F

          proof

            let x be object;

            assume x in ( rng p1);

            then

            consider k be object such that

             A41: k in ( dom p1) and

             A42: x = (p1 . k) by FUNCT_1:def 3;

            reconsider k as Element of NAT by A41;

            

             A43: (p . k) in ( rng p) by A38, A41, FUNCT_1:def 3;

            

             A44: ex dt be Element of ( FinTrees SxD) st (dt = (p . k)) & (x = (dt `1 )) by A38, A39, A41, A42;

            ( rng p) c= FF by FINSEQ_1:def 4;

            then (p . k) in FF by A43;

            then ex dt be Element of ( FinTrees SxD) st (p . k) = dt & (dt `1 ) in F;

            hence thesis by A44;

          end;

          then

          reconsider p1 as FinSequence of F by FINSEQ_1:def 4;

          

           A45: ( dom ( roots p1)) = ( dom p1) by TREES_3:def 18;

          

           A46: ( dom ( pr1 ( roots p))) = ( dom ( roots p)) by MCART_1:def 12;

          then

           A47: ( dom ( pr1 ( roots p))) = ( dom p1) by A38, TREES_3:def 18;

          now

            let k be Nat;

            assume

             A48: k in ( dom p1);

            then

             A49: (p . k) in ( rng p) by A38, FUNCT_1:def 3;

            

             A50: ex dt be Element of ( FinTrees SxD) st (dt = (p . k)) & ((p1 . k) = (dt `1 )) by A38, A39, A48;

            ( rng p) c= FF by FINSEQ_1:def 4;

            then (p . k) in FF by A49;

            then

            consider dt be Element of ( FinTrees SxD) such that

             A51: (p . k) = dt and (dt `1 ) in F;

            reconsider r = {} as Node of dt by TREES_1: 22;

            ex T be DecoratedTree st T = (p1 . k) & (( roots p1) . k) = (T . {} ) by A48, TREES_3:def 18;

            then

             A52: (( roots p1) . k) = ((dt . r) `1 ) by A50, A51, TREES_3: 39;

            ex T be DecoratedTree st T = (p . k) & (( roots p) . k) = (T . {} ) by A38, A48, TREES_3:def 18;

            hence (( roots p1) . k) = (( pr1 ( roots p)) . k) by A46, A47, A48, A51, A52, MCART_1:def 12;

          end;

          then ( pr1 ( roots p)) = ( roots p1) by A45, A47, FINSEQ_1: 13;

          then (( [o, NTermVal(o,pr1,pr2)] -tree p) `1 ) in F by A32, A37, A40;

          hence ( [o, NTV(o,p)] -tree p) in FF;

        end;

        then X c= FF by A6, A35;

        then tt in FF by A6, A34;

        then ex dt be Element of ( FinTrees SxD) st tt = dt & (dt `1 ) in F;

        hence thesis by A33;

      end;

    end;

    scheme :: DTCONSTR:sch5

    DTCHeight { f() -> Function , G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() } :

for n be Nat, dt be Element of ( FinTrees [:the carrier of G(), D():]) st dt in ( Union f()) holds dt in (f() . n) iff ( height ( dom dt)) <= n

      provided

       A1: ( dom f()) = NAT

       and

       A2: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) }

       and

       A3: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) });

      set f = f();

      set G = G();

      set D = D();

      set SxD = [:the carrier of G, D:];

      deffunc NTV( Symbol of G, FinSequence) = NTermVal($1,pr1,pr2);

      defpred R[ Nat] means for dt be Element of ( FinTrees SxD) st dt in ( Union f) holds dt in (f . $1) iff ( height ( dom dt)) <= $1;

      

       A4: R[ 0 ]

      proof

        let dt be Element of ( FinTrees SxD);

        assume

         A5: dt in ( Union f);

        hereby

          assume dt in (f . 0 );

          then ex t be Symbol of G, d be Element of D st dt = ( root-tree [t, d]) & (t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{})) by A2;

          hence ( height ( dom dt)) <= 0 by TREES_1: 42, TREES_4: 3;

        end;

        assume ( height ( dom dt)) <= 0 ;

        then

         A6: ( height ( dom dt)) = 0 ;

        defpred P[ Nat] means not dt in (f . $1);

        assume

         A7: P[ 0 ];

         A8:

        now

          let n be Nat;

          assume

           A9: P[n];

          thus P[(n + 1)]

          proof

            assume dt in (f . (n + 1));

            then dt in ((f . n) \/ { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

            then dt in (f . n) or dt in { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) } by XBOOLE_0:def 3;

            then

            consider o be Symbol of G, p be Element of ((f . n) * ) such that

             A10: dt = ( [o, NTV(o,p)] -tree p) and

             A11: ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) by A9;

            

             A12: dt = ( root-tree (dt . {} )) by A6, TREES_1: 43, TREES_4: 5;

            then

             A13: p = {} by A10, A11, TREES_4: 17;

            then dt = ( root-tree [o, NTermVal(o,{},{})]) by A10, A12, Th3, Th7, TREES_4:def 4;

            hence contradiction by A2, A7, A11, A13, Th3, Th7;

          end;

        end;

        

         A14: for n be Nat holds P[n] from NAT_1:sch 2( A7, A8);

        ex n be object st n in NAT & dt in (f . n) by A1, A5, CARD_5: 2;

        hence contradiction by A14;

      end;

       A15:

      now

        let n be Nat;

        assume

         A16: R[n];

        thus R[(n + 1)]

        proof

          let dt be Element of ( FinTrees SxD);

          assume

           A17: dt in ( Union f);

          hereby

            assume dt in (f . (n + 1));

            then dt in ((f . n) \/ { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

            then

             A18: dt in (f . n) or dt in { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) } by XBOOLE_0:def 3;

            per cases ;

              suppose dt in (f . n);

              then

               A19: ( height ( dom dt)) <= n by A16, A17;

              n <= (n + 1) by NAT_1: 11;

              hence ( height ( dom dt)) <= (n + 1) by A19, XXREAL_0: 2;

            end;

              suppose not dt in (f . n);

              then

              consider o be Symbol of G, p be Element of ((f . n) * ) such that

               A20: dt = ( [o, NTV(o,p)] -tree p) and

               A21: ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) by A18;

              reconsider p as FinSequence of ( FinTrees SxD) by A21;

              

               A22: ( dom dt) = ( tree ( doms p)) by A20, TREES_4: 10;

              now

                let t be finite Tree;

                assume t in ( rng ( doms p));

                then

                consider k be object such that

                 A23: k in ( dom ( doms p)) and

                 A24: t = (( doms p) . k) by FUNCT_1:def 3;

                

                 A25: k in ( dom p) by A23, TREES_3: 37;

                then

                 A26: (p . k) in ( rng p) by FUNCT_1:def 3;

                ( rng p) c= ( FinTrees SxD) by FINSEQ_1:def 4;

                then

                reconsider pk = (p . k) as Element of ( FinTrees SxD) by A26;

                

                 A27: n in NAT by ORDINAL1:def 12;

                

                 A28: ( rng p) c= (f . n) by FINSEQ_1:def 4;

                

                 A29: t = ( dom pk) by A24, A25, FUNCT_6: 22;

                pk in ( Union f) by A1, A26, A28, CARD_5: 2, A27;

                hence ( height t) <= n by A16, A26, A28, A29;

              end;

              hence ( height ( dom dt)) <= (n + 1) by A22, TREES_3: 77;

            end;

          end;

          assume

           A30: ( height ( dom dt)) <= (n + 1);

          defpred P[ Nat] means dt in (f . $1);

          ex k be object st k in NAT & dt in (f . k) by A1, A17, CARD_5: 2;

          then

           A31: ex k be Nat st P[k];

          consider mk be Nat such that

           A32: P[mk] & for kk be Nat st P[kk] holds mk <= kk from NAT_1:sch 5( A31);

          deffunc F( set, set) = { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f . $1) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) };

          

           A33: for n be Nat holds (f . n) c= (f . (n + 1))

          proof

            let n be Nat;

            (f . (n + 1)) = ((f . n) \/ F(n,.)) by A3;

            hence thesis by XBOOLE_1: 7;

          end;

          per cases by NAT_1: 6;

            suppose mk = 0 ;

            then (f . mk) c= (f . ( 0 + (n + 1))) by A33, MEASURE2: 18;

            hence thesis by A32;

          end;

            suppose ex k be Nat st mk = (k + 1);

            then

            consider k be Nat such that

             A34: mk = (k + 1);

            reconsider k as Element of NAT by ORDINAL1:def 12;

            

             A35: k < (k + 1) by NAT_1: 13;

            (f . mk) = ((f . k) \/ { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . k) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) }) by A3, A34;

            then dt in (f . k) or dt in { ( [o, NTV(o,p)] -tree p) where o be Symbol of G, p be Element of ((f . k) * ) : ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) } by A32, XBOOLE_0:def 3;

            then

            consider o be Symbol of G, p be Element of ((f . k) * ) such that

             A36: dt = ( [o, NTV(o,p)] -tree p) and

             A37: ex q be FinSequence of ( FinTrees SxD) st p = q & o ==> ( pr1 ( roots q)) by A32, A34, A35;

            reconsider p as FinSequence of ( FinTrees SxD) by A37;

            

             A38: ( dom dt) = ( tree ( doms p)) by A36, TREES_4: 10;

            ( rng p) c= (f . n)

            proof

              let x be object;

              assume x in ( rng p);

              then

              consider k9 be object such that

               A39: k9 in ( dom p) and

               A40: x = (p . k9) by FUNCT_1:def 3;

              

               A41: x in ( rng p) by A39, A40, FUNCT_1:def 3;

              ( rng p) c= ( FinTrees SxD) by FINSEQ_1:def 4;

              then

              reconsider t = x as Element of ( FinTrees SxD) by A41;

              

               A42: k9 in ( dom ( doms p)) by A39, A40, FUNCT_6: 22;

              ( dom t) = (( doms p) . k9) by A39, A40, FUNCT_6: 22;

              then ( dom t) in ( rng ( doms p)) by A42, FUNCT_1:def 3;

              then ( height ( dom t)) < (n + 1) by A30, A38, TREES_3: 78, XXREAL_0: 2;

              then

               A43: ( height ( dom t)) <= n by NAT_1: 13;

              

               A44: ( rng p) c= (f . k) by FINSEQ_1:def 4;

              t in ( rng p) by A39, A40, FUNCT_1:def 3;

              then t in ( Union f) by A1, A44, CARD_5: 2;

              hence thesis by A16, A43;

            end;

            then p is FinSequence of (f . n) by FINSEQ_1:def 4;

            then

            reconsider p as Element of ((f . n) * ) by FINSEQ_1:def 11;

            ( [o, NTV(o,p)] -tree p) in { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st pp = q & oo ==> ( pr1 ( roots q)) } by A37;

            then dt in ((f . n) \/ { ( [oo, NTV(oo,pp)] -tree pp) where oo be Symbol of G, pp be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st pp = q & oo ==> ( pr1 ( roots q)) }) by A36, XBOOLE_0:def 3;

            hence thesis by A3;

          end;

        end;

      end;

      thus for n be Nat holds R[n] from NAT_1:sch 2( A4, A15);

    end;

    scheme :: DTCONSTR:sch6

    DTCUniq { f() -> Function , G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() } :

for dt1,dt2 be DecoratedTree of [:the carrier of G(), D():] st dt1 in ( Union f()) & dt2 in ( Union f()) & (dt1 `1 ) = (dt2 `1 ) holds dt1 = dt2

      provided

       A1: ( dom f()) = NAT

       and

       A2: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) }

       and

       A3: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) });

      set f = f();

      set G = G();

      set D = D();

      set S = the carrier of G;

      set SxD = [:S, D:];

      deffunc NTV( Symbol of G, FinSequence) = NTermVal($1,pr1,pr2);

      

       A4: (f() . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of D() : t in ( Terminals G()) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) } by A2;

      

       A5: for n be Nat holds (f() . (n + 1)) = ((f() . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f() . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

      defpred R[ Nat] means for dt1,dt2 be DecoratedTree of SxD st dt1 in (f . $1) & dt2 in (f . $1) & (dt1 `1 ) = (dt2 `1 ) holds dt1 = dt2;

      

       A6: R[ 0 ]

      proof

        let dt1,dt2 be DecoratedTree of SxD;

        assume that

         A7: dt1 in (f . 0 ) and

         A8: dt2 in (f . 0 ) and

         A9: (dt1 `1 ) = (dt2 `1 );

        consider t1 be Symbol of G, d1 be Element of D such that

         A10: dt1 = ( root-tree [t1, d1]) and

         A11: t1 in ( Terminals G) & d1 = TermVal(t1) or t1 ==> {} & d1 = NTermVal(t1,{},{}) by A2, A7;

        consider t2 be Symbol of G, d2 be Element of D such that

         A12: dt2 = ( root-tree [t2, d2]) and

         A13: t2 in ( Terminals G) & d2 = TermVal(t2) or t2 ==> {} & d2 = NTermVal(t2,{},{}) by A2, A8;

        

         A14: ( root-tree t1) = (dt1 `1 ) by A10, TREES_4: 25;

        ( root-tree t2) = (dt2 `1 ) by A12, TREES_4: 25;

        then

         A15: t1 = t2 by A9, A14, TREES_4: 4;

        now

          let t be Symbol of G;

          assume t ==> {} ;

          then not ex t9 be Symbol of G st t = t9 & not ex tnt be FinSequence st t9 ==> tnt;

          then not t in { t9 where t9 be Symbol of G : not ex tnt be FinSequence st t9 ==> tnt };

          hence not t in ( Terminals G) by LANG1:def 2;

        end;

        hence thesis by A10, A11, A12, A13, A15;

      end;

       A16:

      now

        let n be Nat such that

         A17: R[n];

        thus R[(n + 1)]

        proof

          let dt1,dt2 be DecoratedTree of SxD;

          assume that

           A18: dt1 in (f . (n + 1)) and

           A19: dt2 in (f . (n + 1)) and

           A20: (dt1 `1 ) = (dt2 `1 );

          

           A21: ( dom dt1) = ( dom (dt1 `1 )) by TREES_4: 24;

          

           A22: ( dom dt2) = ( dom (dt1 `1 )) by A20, TREES_4: 24;

          

           A23: dt1 in ( Union f) by A1, A18, CARD_5: 2;

          

           A24: dt2 in ( Union f) by A1, A19, CARD_5: 2;

          ex X be Subset of ( FinTrees [:the carrier of G(), D():]) st X = ( Union f()) & (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, TermVal(d)]) in X) & (for o be Symbol of G(), p be FinSequence of X st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in X) & for F be Subset of ( FinTrees [:the carrier of G(), D():]) st (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, TermVal(d)]) in F) & (for o be Symbol of G(), p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in F) holds X c= F from DTCMin( A1, A4, A5);

          then

          reconsider dt19 = dt1, dt29 = dt2 as Element of ( FinTrees SxD) by A23, A24;

          

           A25: for n be Nat, dt be Element of ( FinTrees [:the carrier of G(), D():]) st dt in ( Union f()) holds dt in (f() . n) iff ( height ( dom dt)) <= n from DTCHeight( A1, A4, A5);

          per cases ;

            suppose

             A26: dt1 in (f . n);

            then ( height ( dom dt19)) <= n by A23, A25;

            then dt29 in (f . n) by A21, A22, A24, A25;

            hence thesis by A17, A20, A26;

          end;

            suppose

             A27: not dt1 in (f . n);

            

             A28: (f . (n + 1)) = ((f . n) \/ { ( [o1, NTV(o1,p1)] -tree p1) where o1 be Symbol of G, p1 be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p1 = q & o1 ==> ( pr1 ( roots q)) }) by A3;

            then dt1 in (f . n) or dt1 in { ( [o1, NTV(o1,p1)] -tree p1) where o1 be Symbol of G, p1 be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p1 = q & o1 ==> ( pr1 ( roots q)) } by A18, XBOOLE_0:def 3;

            then

            consider o1 be Symbol of G, p1 be Element of ((f . n) * ) such that

             A29: dt1 = ( [o1, NTV(o1,p1)] -tree p1) and

             A30: ex q be FinSequence of ( FinTrees SxD) st p1 = q & o1 ==> ( pr1 ( roots q)) by A27;

            ( height ( dom dt19)) > n by A23, A25, A27;

            then

             A31: not dt29 in (f . n) by A21, A22, A24, A25;

            dt2 in (f . n) or dt2 in { ( [o2, NTV(o2,p2)] -tree p2) where o2 be Symbol of G, p2 be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees SxD) st p2 = q & o2 ==> ( pr1 ( roots q)) } by A19, A28, XBOOLE_0:def 3;

            then

            consider o2 be Symbol of G, p2 be Element of ((f . n) * ) such that

             A32: dt2 = ( [o2, NTV(o2,p2)] -tree p2) and

             A33: ex q be FinSequence of ( FinTrees SxD) st p2 = q & o2 ==> ( pr1 ( roots q)) by A31;

            reconsider p1 as FinSequence of ( FinTrees SxD) by A30;

            consider p11 be FinSequence of ( FinTrees S) such that

             A34: ( dom p11) = ( dom p1) and

             A35: for i be Nat st i in ( dom p1) holds ex T be Element of ( FinTrees SxD) st T = (p1 . i) & (p11 . i) = (T `1 ) and

             A36: (( [o1, NTV(o1,p1)] -tree p1) `1 ) = (o1 -tree p11) by TREES_4: 31;

            reconsider p2 as FinSequence of ( FinTrees SxD) by A33;

            consider p21 be FinSequence of ( FinTrees S) such that

             A37: ( dom p21) = ( dom p2) and

             A38: for i be Nat st i in ( dom p2) holds ex T be Element of ( FinTrees SxD) st T = (p2 . i) & (p21 . i) = (T `1 ) and

             A39: (( [o2, NTV(o2,p2)] -tree p2) `1 ) = (o2 -tree p21) by TREES_4: 31;

            

             A40: o1 = o2 by A20, A29, A32, A36, A39, TREES_4: 15;

            

             A41: p11 = p21 by A20, A29, A32, A36, A39, TREES_4: 15;

            now

              let k be Nat;

              assume

               A42: k in ( dom p11);

              then

              consider p1k be Element of ( FinTrees SxD) such that

               A43: p1k = (p1 . k) and

               A44: (p11 . k) = (p1k `1 ) by A34, A35;

              consider p2k be Element of ( FinTrees SxD) such that

               A45: p2k = (p2 . k) and

               A46: (p21 . k) = (p2k `1 ) by A37, A38, A41, A42;

              

               A47: p1k in (f . n) by A34, A42, A43, Th2;

              p2k in (f . n) by A37, A41, A42, A45, Th2;

              hence (p1 . k) = (p2 . k) by A17, A41, A43, A44, A45, A46, A47;

            end;

            then p1 = p2 by A34, A37, A41, FINSEQ_1: 13;

            hence thesis by A29, A32, A40;

          end;

        end;

      end;

      

       A48: for n be Nat holds R[n] from NAT_1:sch 2( A6, A16);

      let dt1,dt2 be DecoratedTree of SxD;

      assume that

       A49: dt1 in ( Union f) and

       A50: dt2 in ( Union f) and

       A51: (dt1 `1 ) = (dt2 `1 );

      consider n1 be object such that

       A52: n1 in NAT and

       A53: dt1 in (f . n1) by A1, A49, CARD_5: 2;

      consider n2 be object such that

       A54: n2 in NAT and

       A55: dt2 in (f . n2) by A1, A50, CARD_5: 2;

      reconsider n1, n2 as Element of NAT by A52, A54;

      deffunc F( set, set) = { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f . $1) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), D():]) st p = q & o ==> ( pr1 ( roots q)) };

      

       A56: for n be Nat holds (f . n) c= (f . (n + 1))

      proof

        let n be Nat;

        (f . (n + 1)) = ((f . n) \/ F(n,.)) by A3;

        hence thesis by XBOOLE_1: 7;

      end;

      

       A57: for k,s be Nat holds (f . k) c= (f . (k + s)) by NAT_1: 11, A56, MEASURE2: 18;

      n1 <= n2 or n1 >= n2;

      then (ex s be Nat st n2 = (n1 + s)) or ex s be Nat st n1 = (n2 + s) by NAT_1: 10;

      then (f . n1) c= (f . n2) or (f . n2) c= (f . n1) by A57;

      hence thesis by A48, A51, A53, A55;

    end;

    definition

      let G be non empty DTConstrStr;

      :: DTCONSTR:def1

      func TS (G) -> Subset of ( FinTrees the carrier of G) means

      : Def1: (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in it ) & (for o be Symbol of G, p be FinSequence of it st o ==> ( roots p) holds (o -tree p) in it ) & for F be Subset of ( FinTrees the carrier of G) st (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in F) & (for o be Symbol of G, p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F) holds it c= F;

      existence

      proof

        deffunc F( set, set) = ($2 \/ { ( [o, A(o,pr1,pr2)] -tree p) where o be Symbol of G, p be Element of ($2 * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, NAT :]) st p = q & o ==> ( pr1 ( roots q)) });

        consider f be Function such that

         A1: ( dom f) = NAT and

         A2: (f . 0 ) = { ( root-tree [t, d]) where t be Symbol of G, d be Element of NAT : t in ( Terminals G) & d = T(t) or t ==> {} & d = A(t,{},{}) } and

         A3: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

        

         A4: for n be Nat holds (f . (n + 1)) = ((f . n) \/ { ( [o, A(o,pr1,pr2)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, NAT :]) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

        ex X1 be Subset of ( FinTrees the carrier of G) st X1 = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G, NAT :]) : t in ( Union f) } & (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in X1) & (for o be Symbol of G, p be FinSequence of X1 st o ==> ( roots p) holds (o -tree p) in X1) & for F be Subset of ( FinTrees the carrier of G) st (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in F) & (for o be Symbol of G, p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F) holds X1 c= F from DTCSymbols( A1, A2, A4);

        hence thesis;

      end;

      uniqueness ;

    end

    scheme :: DTCONSTR:sch7

    DTConstrInd { G() -> non empty DTConstrStr , P[ set] } :

for t be DecoratedTree of the carrier of G() st t in ( TS G()) holds P[t]

      provided

       A1: for s be Symbol of G() st s in ( Terminals G()) holds P[( root-tree s)]

       and

       A2: for nt be Symbol of G(), ts be FinSequence of ( TS G()) st nt ==> ( roots ts) & for t be DecoratedTree of the carrier of G() st t in ( rng ts) holds P[t] holds P[(nt -tree ts)];

      deffunc F( set, set) = ($2 \/ { ( [o, 0 ] -tree p) where o be Symbol of G(), p be Element of ($2 * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), NAT :]) st p = q & o ==> ( pr1 ( roots q)) });

      consider f be Function such that

       A3: ( dom f) = NAT and

       A4: (f . 0 ) = { ( root-tree [t, d]) where t be Symbol of G(), d be Element of NAT : t in ( Terminals G()) & d = T(t) or t ==> {} & d = A(t,{},{}) } and

       A5: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

      

       A6: for n be Nat holds (f . (n + 1)) = ((f . n) \/ { ( [o, A(o,pr1,pr2)] -tree p) where o be Symbol of G(), p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), NAT :]) st p = q & o ==> ( pr1 ( roots q)) }) by A5;

      

       A7: ex X be Subset of ( FinTrees [:the carrier of G(), NAT :]) st X = ( Union f) & (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, T(d)]) in X) & (for o be Symbol of G(), p be FinSequence of X st o ==> ( pr1 ( roots p)) holds ( [o, A(o,pr1,pr2)] -tree p) in X) & for F be Subset of ( FinTrees [:the carrier of G(), NAT :]) st (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree [d, T(d)]) in F) & (for o be Symbol of G(), p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, A(o,pr1,pr2)] -tree p) in F) holds X c= F from DTCMin( A3, A4, A6);

      consider TSG be Subset of ( FinTrees the carrier of G()) such that

       A8: TSG = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G(), NAT :]) : t in ( Union f) } and

       A9: for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree d) in TSG and

       A10: for o be Symbol of G(), p be FinSequence of TSG st o ==> ( roots p) holds (o -tree p) in TSG and

       A11: for F be Subset of ( FinTrees the carrier of G()) st (for d be Symbol of G() st d in ( Terminals G()) holds ( root-tree d) in F) & (for o be Symbol of G(), p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F) holds TSG c= F from DTCSymbols( A3, A4, A6);

      

       A12: TSG = ( TS G()) by A9, A10, A11, Def1;

      defpred R[ Nat] means for t be DecoratedTree of [:the carrier of G(), NAT :] st t in (f . $1) holds P[(t `1 )];

      

       A13: R[ 0 ]

      proof

        let tt be DecoratedTree of [:the carrier of G(), NAT :];

        set p = ( <*> ( TS G()));

        assume tt in (f . 0 );

        then

        consider t be Symbol of G(), d be Element of NAT such that

         A14: tt = ( root-tree [t, d]) and

         A15: t in ( Terminals G()) & d = 0 or t ==> ( roots p) & d = 0 by A4, Th3;

        

         A16: (tt `1 ) = ( root-tree t) by A14, TREES_4: 25;

        

         A17: (t -tree p) = ( root-tree t) by TREES_4: 20;

        for T be DecoratedTree of the carrier of G() st T in ( rng p) holds P[T];

        hence thesis by A1, A2, A15, A16, A17;

      end;

       A18:

      now

        let n be Nat;

        assume

         A19: R[n];

        thus R[(n + 1)]

        proof

          let x be DecoratedTree of [:the carrier of G(), NAT :];

          assume that

           A20: x in (f . (n + 1)) and

           A21: not P[(x `1 )];

          x in ((f . n) \/ { ( [o, 0 ] -tree p) where o be Symbol of G(), p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), NAT :]) st p = q & o ==> ( pr1 ( roots q)) }) by A5, A20;

          then x in (f . n) or x in { ( [o, 0 ] -tree p) where o be Symbol of G(), p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G(), NAT :]) st p = q & o ==> ( pr1 ( roots q)) } by XBOOLE_0:def 3;

          then

          consider o be Symbol of G(), p be Element of ((f . n) * ) such that

           A22: x = ( [o, 0 ] -tree p) and

           A23: ex q be FinSequence of ( FinTrees [:the carrier of G(), NAT :]) st p = q & o ==> ( pr1 ( roots q)) by A19, A21;

          

           A24: ( Union f) = ( union ( rng f)) by CARD_3:def 4;

          n in NAT by ORDINAL1:def 12;

          then

           A25: (f . n) in ( rng f) by A3, FUNCT_1:def 3;

          

           A26: ( rng p) c= (f . n) by FINSEQ_1:def 4;

          

           A27: (f . n) c= ( Union f) by A24, A25, ZFMISC_1: 74;

          

           A28: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          defpred P[ set, set] means ex dt be Element of ( FinTrees [:the carrier of G(), NAT :]) st dt = (p . $1) & (dt `1 ) = $2 & dt in ( Union f);

          

           A29: for k be Nat st k in ( Seg ( len p)) holds ex x be Element of ( FinTrees the carrier of G()) st P[k, x]

          proof

            let k be Nat;

            assume k in ( Seg ( len p));

            then

             A30: (p . k) in ( rng p) by A28, FUNCT_1:def 3;

            

             A31: ( rng p) c= ( Union f) by A26, A27;

            then (p . k) in ( Union f) by A30;

            then

            reconsider dt = (p . k) as Element of ( FinTrees [:the carrier of G(), NAT :]) by A7;

            

             A32: (dt `1 ) = (( pr1 (the carrier of G(), NAT )) * dt) by TREES_3:def 12;

            

             A33: ( rng dt) c= [:the carrier of G(), NAT :] by RELAT_1:def 19;

            ( dom ( pr1 (the carrier of G(), NAT ))) = [:the carrier of G(), NAT :] by FUNCT_2:def 1;

            then ( dom (dt `1 )) = ( dom dt) by A32, A33, RELAT_1: 27;

            then

            reconsider x = (dt `1 ) as Element of ( FinTrees the carrier of G()) by TREES_3:def 8;

            take x, dt;

            thus thesis by A30, A31;

          end;

          consider p1 be FinSequence of ( FinTrees the carrier of G()) such that

           A34: ( dom p1) = ( Seg ( len p)) and

           A35: for k be Nat st k in ( Seg ( len p)) holds P[k, (p1 . k)] from FINSEQ_1:sch 5( A29);

          reconsider p as FinSequence of ( Trees [:the carrier of G(), NAT :]) by A23, Th1;

          

           A36: ( dom ( roots p1)) = ( dom p1) by TREES_3:def 18;

          

           A37: ( dom ( pr1 ( roots p))) = ( dom ( roots p)) by MCART_1:def 12;

          then

           A38: ( dom ( pr1 ( roots p))) = ( dom p1) by A28, A34, TREES_3:def 18;

          now

            let k be Nat;

            assume

             A39: k in ( dom p1);

            then

            consider dt be Element of ( FinTrees [:the carrier of G(), NAT :]) such that

             A40: dt = (p . k) and

             A41: (dt `1 ) = (p1 . k) and dt in ( Union f) by A34, A35;

            reconsider r = {} as Node of dt by TREES_1: 22;

            ex T be DecoratedTree st T = (p1 . k) & (( roots p1) . k) = (T . {} ) by A39, TREES_3:def 18;

            then

             A42: (( roots p1) . k) = ((dt . r) `1 ) by A41, TREES_3: 39;

            ex T be DecoratedTree st T = (p . k) & (( roots p) . k) = (T . {} ) by A28, A34, A39, TREES_3:def 18;

            hence (( roots p1) . k) = (( pr1 ( roots p)) . k) by A37, A38, A39, A40, A42, MCART_1:def 12;

          end;

          then

           A43: ( roots p1) = ( pr1 ( roots p)) by A36, A38, FINSEQ_1: 13;

          ( rng p1) c= ( TS G())

          proof

            let x be object;

            assume x in ( rng p1);

            then

            consider k be object such that

             A44: k in ( dom p1) and

             A45: x = (p1 . k) by FUNCT_1:def 3;

            reconsider k as Element of NAT by A44;

            ex dt be Element of ( FinTrees [:the carrier of G(), NAT :]) st dt = (p . k) & (dt `1 ) = (p1 . k) & dt in ( Union f) by A34, A35, A44;

            hence thesis by A8, A12, A45;

          end;

          then

          reconsider p1 as FinSequence of ( TS G()) by FINSEQ_1:def 4;

          now

            let t be DecoratedTree of the carrier of G();

            assume t in ( rng p1);

            then

            consider k be object such that

             A46: k in ( dom p1) and

             A47: t = (p1 . k) by FUNCT_1:def 3;

            reconsider k as Element of NAT by A46;

            

             A48: ex dt be Element of ( FinTrees [:the carrier of G(), NAT :]) st (dt = (p . k)) & ((dt `1 ) = (p1 . k)) & (dt in ( Union f)) by A34, A35, A46;

            (p . k) in ( rng p) by A28, A34, A46, FUNCT_1:def 3;

            hence P[t] by A19, A26, A47, A48;

          end;

          then

           A49: P[(o -tree p1)] by A2, A23, A43;

          reconsider p1 as FinSequence of ( Trees the carrier of G()) by Th1;

          now

            let k be Nat;

            assume k in ( dom p);

            then ex dt be Element of ( FinTrees [:the carrier of G(), NAT :]) st dt = (p . k) & (dt `1 ) = (p1 . k) & dt in ( Union f) by A28, A35;

            hence for T be DecoratedTree of [:the carrier of G(), NAT :] st T = (p . k) holds (p1 . k) = (T `1 );

          end;

          hence contradiction by A21, A22, A28, A34, A49, TREES_4: 27;

        end;

      end;

      

       A50: for n be Nat holds R[n] from NAT_1:sch 2( A13, A18);

      let t be DecoratedTree of the carrier of G();

      assume t in ( TS G());

      then

      consider tt be Element of ( FinTrees [:the carrier of G(), NAT :]) such that

       A51: t = (tt `1 ) and

       A52: tt in ( Union f) by A8, A12;

      ex n be object st n in NAT & tt in (f . n) by A3, A52, CARD_5: 2;

      hence thesis by A50, A51;

    end;

    scheme :: DTCONSTR:sch8

    DTConstrIndDef { G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() } :

ex f be Function of ( TS G()), D() st (for t be Symbol of G() st t in ( Terminals G()) holds (f . ( root-tree t)) = TermVal(t)) & for nt be Symbol of G(), ts be FinSequence of ( TS G()) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = NTermVal(nt,roots,*);

      set G = G();

      deffunc NTV( Symbol of G, FinSequence) = NTermVal($1,pr1,pr2);

      deffunc F( set, set) = ($2 \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G, p be Element of ($2 * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D():]) st p = q & o ==> ( pr1 ( roots q)) });

      consider f be Function such that

       A1: ( dom f) = NAT and

       A2: (f . 0 ) = { ( root-tree [t, d]) where t be Symbol of G, d be Element of D() : t in ( Terminals G) & d = TermVal(t) or t ==> {} & d = NTermVal(t,{},{}) } and

       A3: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

      

       A4: for n be Nat holds (f . (n + 1)) = ((f . n) \/ { ( [o, NTermVal(o,pr1,pr2)] -tree p) where o be Symbol of G, p be Element of ((f . n) * ) : ex q be FinSequence of ( FinTrees [:the carrier of G, D():]) st p = q & o ==> ( pr1 ( roots q)) }) by A3;

      ex X1 be Subset of ( FinTrees the carrier of G) st X1 = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G, D():]) : t in ( Union f) } & (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in X1) & (for o be Symbol of G, p be FinSequence of X1 st o ==> ( roots p) holds (o -tree p) in X1) & for F be Subset of ( FinTrees the carrier of G) st (for d be Symbol of G st d in ( Terminals G) holds ( root-tree d) in F) & (for o be Symbol of G, p be FinSequence of F st o ==> ( roots p) holds (o -tree p) in F) holds X1 c= F from DTCSymbols( A1, A2, A4);

      then

       A5: ( TS G) = { (t `1 ) where t be Element of ( FinTrees [:the carrier of G, D():]) : t in ( Union f) } by Def1;

      defpred P[ object, object] means for dt be DecoratedTree of [:the carrier of G, D():] st dt in ( Union f) & $1 = (dt `1 ) holds $2 = ((dt `2 ) . {} );

      

       A6: for e be object st e in ( TS G) holds ex u be object st u in D() & P[e, u]

      proof

        let e be object;

        assume e in ( TS G);

        then

        consider DT be Element of ( FinTrees [:the carrier of G, D():]) such that

         A7: e = (DT `1 ) and

         A8: DT in ( Union f) by A5;

        reconsider r = {} as Node of (DT `2 ) by TREES_1: 22;

        take u = ((DT `2 ) . r);

        thus u in D();

        

         A9: for dt1,dt2 be DecoratedTree of [:the carrier of G, D():] st dt1 in ( Union f) & dt2 in ( Union f) & (dt1 `1 ) = (dt2 `1 ) holds dt1 = dt2 from DTCUniq( A1, A2, A4);

        let dt be DecoratedTree of [:the carrier of G, D():];

        assume that

         A10: dt in ( Union f) and

         A11: e = (dt `1 );

        thus thesis by A7, A8, A9, A10, A11;

      end;

      consider ff be Function such that

       A12: ( dom ff) = ( TS G) & ( rng ff) c= D() and

       A13: for e be object st e in ( TS G) holds P[e, (ff . e)] from FUNCT_1:sch 6( A6);

      reconsider ff as Function of ( TS G), D() by A12, FUNCT_2:def 1, RELSET_1: 4;

      take ff;

      consider X be Subset of ( FinTrees [:the carrier of G, D():]) such that

       A14: X = ( Union f) and

       A15: for d be Symbol of G st d in ( Terminals G) holds ( root-tree [d, TermVal(d)]) in X and

       A16: for o be Symbol of G, p be FinSequence of X st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in X and for F be Subset of ( FinTrees [:the carrier of G, D():]) st (for d be Symbol of G st d in ( Terminals G) holds ( root-tree [d, TermVal(d)]) in F) & (for o be Symbol of G, p be FinSequence of F st o ==> ( pr1 ( roots p)) holds ( [o, NTermVal(o,pr1,pr2)] -tree p) in F) holds X c= F from DTCMin( A1, A2, A4);

      hereby

        let t be Symbol of G;

        assume

         A17: t in ( Terminals G);

        

         A18: (( root-tree [t, TermVal(t)]) `1 ) = ( root-tree t) by TREES_4: 25;

        

         A19: (( root-tree [t, TermVal(t)]) `2 ) = ( root-tree TermVal(t)) by TREES_4: 25;

        ( root-tree [t, TermVal(t)]) in ( Union f) by A14, A15, A17;

        then ( root-tree t) in ( TS G) by A5, A18;

        

        hence (ff . ( root-tree t)) = (( root-tree TermVal(t)) . {} ) by A13, A14, A15, A17, A18, A19

        .= TermVal(t) by TREES_4: 3;

      end;

      let nt be Symbol of G, ts be FinSequence of ( TS G);

      set rts = ( roots ts);

      assume

       A20: nt ==> rts;

      set x = (ff * ts);

      

       A21: ( dom ts) = ( Seg ( len ts)) by FINSEQ_1:def 3;

      defpred P[ set, set] means ex dt be DecoratedTree of [:the carrier of G, D():] st dt = $2 & (dt `1 ) = (ts . $1) & dt in ( Union f);

      

       A22: for k be Nat st k in ( Seg ( len ts)) holds ex x be Element of ( FinTrees [:the carrier of G, D():]) st P[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len ts));

        then

         A23: (ts . k) in ( rng ts) by A21, FUNCT_1:def 3;

        ( rng ts) c= ( TS G) by FINSEQ_1:def 4;

        then (ts . k) in ( TS G) by A23;

        then ex x be Element of ( FinTrees [:the carrier of G, D():]) st (ts . k) = (x `1 ) & x in ( Union f) by A5;

        hence thesis;

      end;

      consider dts be FinSequence of ( FinTrees [:the carrier of G, D():]) such that

       A24: ( dom dts) = ( Seg ( len ts)) and

       A25: for k be Nat st k in ( Seg ( len ts)) holds P[k, (dts . k)] from FINSEQ_1:sch 5( A22);

      ( rng dts) c= X

      proof

        let x be object;

        assume x in ( rng dts);

        then

        consider k be object such that

         A26: k in ( dom ts) and

         A27: x = (dts . k) by A21, A24, FUNCT_1:def 3;

        reconsider k as Element of NAT by A26;

        ex dt be DecoratedTree of [:the carrier of G, D():] st dt = x & (dt `1 ) = (ts . k) & dt in ( Union f) by A21, A25, A26, A27;

        hence thesis by A14;

      end;

      then

      reconsider dts as FinSequence of X by FINSEQ_1:def 4;

      

       A28: ( dom ( roots ts)) = ( dom ts) by TREES_3:def 18;

      

       A29: ( dom ( pr1 ( roots dts))) = ( dom ( roots dts)) by MCART_1:def 12;

      

       A30: ( dom ( pr2 ( roots dts))) = ( dom ( roots dts)) by MCART_1:def 13;

      

       A31: ( dom ( pr1 ( roots dts))) = ( dom ts) by A21, A24, A29, TREES_3:def 18;

      

       A32: ( dom ( pr2 ( roots dts))) = ( dom ts) by A21, A24, A30, TREES_3:def 18;

      now

        let k be Nat;

        assume

         A33: k in ( dom ts);

        then

        consider dt be DecoratedTree of [:the carrier of G, D():] such that

         A34: dt = (dts . k) and

         A35: (dt `1 ) = (ts . k) and dt in ( Union f) by A21, A25;

        reconsider r = {} as Node of dt by TREES_1: 22;

        ex T be DecoratedTree st T = (ts . k) & (( roots ts) . k) = (T . {} ) by A33, TREES_3:def 18;

        then

         A36: (( roots ts) . k) = ((dt . r) `1 ) by A35, TREES_3: 39;

        ex T be DecoratedTree st T = (dts . k) & (( roots dts) . k) = (T . {} ) by A21, A24, A33, TREES_3:def 18;

        hence (( roots ts) . k) = (( pr1 ( roots dts)) . k) by A29, A31, A33, A34, A36, MCART_1:def 12;

      end;

      then

       A37: ( roots ts) = ( pr1 ( roots dts)) by A28, A31, FINSEQ_1: 13;

      then

       A38: ( [nt, NTV(nt,dts)] -tree dts) in X by A16, A20;

      

       A39: ( rng dts) c= ( FinTrees [:the carrier of G, D():]) by FINSEQ_1:def 4;

      ( FinTrees [:the carrier of G, D():]) c= ( Trees [:the carrier of G, D():]) by TREES_3: 21;

      then ( rng dts) c= ( Trees [:the carrier of G, D():]) by A39;

      then

      reconsider dts9 = dts as FinSequence of ( Trees [:the carrier of G, D():]) by FINSEQ_1:def 4;

      

       A40: ( rng ts) c= ( FinTrees the carrier of G) by FINSEQ_1:def 4;

      ( FinTrees the carrier of G) c= ( Trees the carrier of G) by TREES_3: 21;

      then ( rng ts) c= ( Trees the carrier of G) by A40;

      then

      reconsider ts9 = ts as FinSequence of ( Trees the carrier of G) by FINSEQ_1:def 4;

      now

        let i be Nat;

        assume i in ( dom dts);

        then

         A41: ex dt be DecoratedTree of [:the carrier of G, D():] st (dt = (dts . i)) & ((dt `1 ) = (ts . i)) & (dt in ( Union f)) by A24, A25;

        let T be DecoratedTree of [:the carrier of G, D():];

        assume T = (dts . i);

        hence (ts . i) = (T `1 ) by A41;

      end;

      then

       A42: (( [nt, NTV(nt,dts)] -tree dts9) `1 ) = (nt -tree ts9) by A21, A24, TREES_4: 27;

      

       A43: ( rng ts) c= ( dom ff) by A12, FINSEQ_1:def 4;

      then

       A44: ( dom (ff * ts)) = ( dom ts) by RELAT_1: 27;

      now

        let k be Nat;

        assume

         A45: k in ( dom ts);

        then

        consider dt be DecoratedTree of [:the carrier of G, D():] such that

         A46: dt = (dts . k) and

         A47: (dt `1 ) = (ts . k) and

         A48: dt in ( Union f) by A21, A25;

        reconsider r = {} as Node of dt by TREES_1: 22;

        

         A49: (ts . k) in ( rng ts) by A45, FUNCT_1:def 3;

        

         A50: (x . k) = (ff . (dt `1 )) by A44, A45, A47, FUNCT_1: 12

        .= ((dt `2 ) . {} ) by A12, A13, A43, A47, A48, A49

        .= ((dt . r) `2 ) by TREES_3: 39;

        ex T be DecoratedTree st T = (dts . k) & (( roots dts) . k) = (T . r) by A21, A24, A45, TREES_3:def 18;

        hence (x . k) = (( pr2 ( roots dts)) . k) by A29, A31, A45, A46, A50, MCART_1:def 13;

      end;

      then

       A51: x = ( pr2 ( roots dts)) by A32, A44, FINSEQ_1: 13;

      reconsider r = {} as Node of ( [nt, NTermVal(nt,rts,x)] -tree dts) by TREES_1: 22;

      (nt -tree ts) in ( TS G) by A5, A14, A38, A42;

      

      then (ff . (nt -tree ts)) = ((( [nt, NTermVal(nt,rts,x)] -tree dts) `2 ) . r) by A13, A14, A16, A20, A37, A42, A51

      .= ((( [nt, NTermVal(nt,rts,x)] -tree dts) . r) `2 ) by TREES_3: 39

      .= ( [nt, NTermVal(nt,rts,x)] `2 ) by TREES_4:def 4;

      hence thesis;

    end;

    scheme :: DTCONSTR:sch9

    DTConstrUniqDef { G() -> non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set) -> Element of D() , f1,f2() -> Function of ( TS G()), D() } :

f1() = f2()

      provided

       A1: (for t be Symbol of G() st t in ( Terminals G()) holds (f1() . ( root-tree t)) = TermVal(t)) & for nt be Symbol of G(), ts be FinSequence of ( TS G()) st nt ==> ( roots ts) holds (f1() . (nt -tree ts)) = NTermVal(nt,roots,*)

       and

       A2: (for t be Symbol of G() st t in ( Terminals G()) holds (f2() . ( root-tree t)) = TermVal(t)) & for nt be Symbol of G(), ts be FinSequence of ( TS G()) st nt ==> ( roots ts) holds (f2() . (nt -tree ts)) = NTermVal(nt,roots,*);

      set G = G();

      defpred P[ set] means (f1() . $1) = (f2() . $1);

       A3:

      now

        let s be Symbol of G;

        assume

         A4: s in ( Terminals G);

        

        then (f1() . ( root-tree s)) = TermVal(s) by A1

        .= (f2() . ( root-tree s)) by A2, A4;

        hence P[( root-tree s)];

      end;

       A5:

      now

        let nt be Symbol of G, ts be FinSequence of ( TS G);

        assume that

         A6: nt ==> ( roots ts) and

         A7: for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t];

        

         A8: ( rng ts) c= ( TS G) by FINSEQ_1:def 4;

        then ( rng ts) c= ( dom f1()) by FUNCT_2:def 1;

        then

         A9: ( dom (f1() * ts)) = ( dom ts) by RELAT_1: 27;

        reconsider ntv1 = (f1() * ts) as FinSequence;

        reconsider ntv1 as FinSequence of D();

        ( rng ts) c= ( dom f2()) by A8, FUNCT_2:def 1;

        then

         A10: ( dom (f2() * ts)) = ( dom ts) by RELAT_1: 27;

        now

          let x be object;

          assume

           A11: x in ( dom ts);

          then

          reconsider t = (ts . x) as Element of ( FinTrees the carrier of G) by Th2;

          t in ( rng ts) by A11, FUNCT_1:def 3;

          then

           A12: (f1() . t) = (f2() . t) by A7;

          

          thus ((f1() * ts) . x) = (f1() . t) by A9, A11, FUNCT_1: 12

          .= ((f2() * ts) . x) by A10, A11, A12, FUNCT_1: 12;

        end;

        then

         A13: (f1() * ts) = (f2() * ts) by A9, A10, FUNCT_1: 2;

        (f1() . (nt -tree ts)) = NTermVal(nt,roots,ntv1) by A1, A6

        .= (f2() . (nt -tree ts)) by A2, A6, A13;

        hence P[(nt -tree ts)];

      end;

      for t be DecoratedTree of the carrier of G st t in ( TS G) holds P[t] from DTConstrInd( A3, A5);

      then for x be object st x in ( TS G) holds (f1() . x) = (f2() . x);

      hence thesis by FUNCT_2: 12;

    end;

    begin

    defpred P[ set, set] means $1 = 1 & ($2 = <* 0 *> or $2 = <*1*>);

    definition

      :: DTCONSTR:def2

      func PeanoNat -> strict non empty DTConstrStr means

      : Def2: the carrier of it = { 0 , 1} & for x be Symbol of it , y be FinSequence of the carrier of it holds x ==> y iff x = 1 & (y = <* 0 *> or y = <*1*>);

      existence

      proof

        thus ex G be strict non empty DTConstrStr st the carrier of G = { 0 , 1} & for x be Symbol of G, p be FinSequence of the carrier of G holds x ==> p iff P[x, p] from DTConstrStrEx;

      end;

      uniqueness

      proof

        thus for G1,G2 be strict non empty DTConstrStr st (the carrier of G1 = { 0 , 1} & for x be Symbol of G1, p be FinSequence of the carrier of G1 holds x ==> p iff P[x, p]) & (the carrier of G2 = { 0 , 1} & for x be Symbol of G2, p be FinSequence of the carrier of G2 holds x ==> p iff P[x, p]) holds G1 = G2 from DTConstrStrUniq;

      end;

    end

    set PN = PeanoNat ;

    

     Lm2: the carrier of PN = { 0 , 1} by Def2;

    then

    reconsider O = 0 , S = 1 as Symbol of PN by TARSKI:def 2;

    

     Lm3: S ==> <*O*> by Def2;

    

     Lm4: S ==> <*S*> by Def2;

    

     Lm5: S ==> <*O*> by Def2;

    

     Lm6: S ==> <*S*> by Def2;

    

     Lm7: ( Terminals PN) = { x where x be Symbol of PN : not ex tnt be FinSequence st x ==> tnt } by LANG1:def 2;

     Lm8:

    now

      given x be FinSequence such that

       A1: O ==> x;

       [O, x] in the Rules of PN by A1, LANG1:def 1;

      then x in (the carrier of PN * ) by ZFMISC_1: 87;

      then x is FinSequence of the carrier of PN by FINSEQ_2:def 3;

      hence contradiction by A1, Def2;

    end;

    then

     Lm9: O in ( Terminals PN) by Lm7;

    

     Lm10: ( Terminals PN) c= {O}

    proof

      let x be object;

      assume x in ( Terminals PN);

      then

      consider y be Symbol of PN such that

       A1: x = y and

       A2: not ex tnt be FinSequence st y ==> tnt by Lm7;

      y = O or y = S & {O, S} <> {} by Lm2, TARSKI:def 2;

      hence thesis by A1, A2, Lm5, TARSKI:def 1;

    end;

    

     Lm11: ( NonTerminals PN) = { x where x be Symbol of PN : ex tnt be FinSequence st x ==> tnt } by LANG1:def 3;

    then

     Lm12: S in ( NonTerminals PN) by Lm5;

    then

     Lm13: {S} c= ( NonTerminals PN) by ZFMISC_1: 31;

    

     Lm14: ( NonTerminals PN) c= {S}

    proof

      let x be object;

      assume x in ( NonTerminals PN);

      then

      consider y be Symbol of PN such that

       A1: x = y and

       A2: ex tnt be FinSequence st y ==> tnt by Lm11;

      y = O or y = S by Lm2, TARSKI:def 2;

      hence thesis by A1, A2, Lm8, TARSKI:def 1;

    end;

    then

     Lm15: ( NonTerminals PN) = {S} by Lm13;

    reconsider TSPN = ( TS PN) as non empty Subset of ( FinTrees the carrier of PN) by Def1, Lm9;

    begin

    definition

      let G be non empty DTConstrStr;

      :: DTCONSTR:def3

      attr G is with_terminals means

      : Def3: ( Terminals G) <> {} ;

      :: DTCONSTR:def4

      attr G is with_nonterminals means

      : Def4: ( NonTerminals G) <> {} ;

      :: DTCONSTR:def5

      attr G is with_useful_nonterminals means

      : Def5: for nt be Symbol of G st nt in ( NonTerminals G) holds ex p be FinSequence of ( TS G) st nt ==> ( roots p);

    end

    

     Lm16: PN is with_terminals with_nonterminals with_useful_nonterminals

    proof

      thus ( Terminals PN) <> {} by Lm9;

      thus ( NonTerminals PN) <> {} by Lm12;

      reconsider rO = ( root-tree O) as Element of TSPN by Def1, Lm9;

      reconsider p = <*rO qua Element of TSPN qua non empty set*> as FinSequence of TSPN;

      reconsider p as FinSequence of ( TS PN);

      let nt be Symbol of PN;

      assume nt in ( NonTerminals PN);

      then

       A1: nt = S by Lm14, TARSKI:def 1;

      take p;

      

       A2: ( dom <*rO*>) = ( Seg 1) by FINSEQ_1: 38;

      

       A3: ( dom <*O*>) = ( Seg 1) by FINSEQ_1: 38;

      now

        let i be Element of NAT ;

        assume

         A4: i in ( dom p);

        reconsider rO as DecoratedTree;

        take rO;

        

         A5: i = 1 by A2, A4, FINSEQ_1: 2, TARSKI:def 1;

        ( <*O*> . 1) = O by FINSEQ_1: 40;

        hence rO = (p . i) & ( <*O*> . i) = (rO . {} ) by A5, FINSEQ_1: 40, TREES_4: 3;

      end;

      hence thesis by A1, A2, A3, Lm5, TREES_3:def 18;

    end;

    registration

      cluster with_terminals with_nonterminals with_useful_nonterminals strict for non empty DTConstrStr;

      existence by Lm16;

    end

    definition

      let G be with_terminals non empty DTConstrStr;

      :: original: Terminals

      redefine

      func Terminals G -> non empty Subset of G ;

      coherence

      proof

        defpred P[ Element of G] means not ex tnt be FinSequence st $1 ==> tnt;

        { t where t be Element of G : P[t] } c= the carrier of G from FRAENKEL:sch 10;

        hence thesis by Def3, LANG1:def 2;

      end;

    end

    registration

      let G be with_terminals non empty DTConstrStr;

      cluster ( TS G) -> non empty;

      coherence

      proof

        ex t be object st t in ( Terminals G) by XBOOLE_0:def 1;

        hence thesis by Def1;

      end;

    end

    registration

      let G be with_useful_nonterminals non empty DTConstrStr;

      cluster ( TS G) -> non empty;

      coherence

      proof

        set s = the Symbol of G;

        per cases ;

          suppose not ex tnt be FinSequence st s ==> tnt;

          then s in { t where t be Symbol of G : not ex tnt be FinSequence st t ==> tnt };

          then s in ( Terminals G) by LANG1:def 2;

          hence thesis by Def1;

        end;

          suppose ex tnt be FinSequence st s ==> tnt;

          then s in { t where t be Symbol of G : ex tnt be FinSequence st t ==> tnt };

          then s in ( NonTerminals G) by LANG1:def 3;

          then ex p be FinSequence of ( TS G) st (s ==> ( roots p)) by Def5;

          hence thesis by Def1;

        end;

      end;

    end

    definition

      let G be with_nonterminals non empty DTConstrStr;

      :: original: NonTerminals

      redefine

      func NonTerminals G -> non empty Subset of G ;

      coherence

      proof

        defpred P[ Element of G] means ex tnt be FinSequence st $1 ==> tnt;

        { t where t be Element of G : P[t] } c= the carrier of G from FRAENKEL:sch 10;

        hence thesis by Def4, LANG1:def 3;

      end;

    end

    definition

      let G be with_terminals non empty DTConstrStr;

      mode Terminal of G is Element of ( Terminals G);

    end

    definition

      let G be with_nonterminals non empty DTConstrStr;

      mode NonTerminal of G is Element of ( NonTerminals G);

    end

    definition

      let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;

      let nt be NonTerminal of G;

      :: DTCONSTR:def6

      mode SubtreeSeq of nt -> FinSequence of ( TS G) means

      : Def6: nt ==> ( roots it );

      existence by Def5;

    end

    definition

      let G be with_terminals non empty DTConstrStr;

      let t be Terminal of G;

      :: original: root-tree

      redefine

      func root-tree t -> Element of ( TS G) ;

      coherence by Def1;

    end

    definition

      let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;

      let nt be NonTerminal of G;

      let p be SubtreeSeq of nt;

      :: original: -tree

      redefine

      func nt -tree p -> Element of ( TS G) ;

      coherence

      proof

        nt ==> ( roots p) by Def6;

        hence thesis by Def1;

      end;

    end

    theorem :: DTCONSTR:9

    

     Th9: for G be with_terminals non empty DTConstrStr, tsg be Element of ( TS G), s be Terminal of G st (tsg . {} ) = s holds tsg = ( root-tree s)

    proof

      let G be with_terminals non empty DTConstrStr, tsg be Element of ( TS G), s be Terminal of G;

      assume

       A1: (tsg . {} ) = s;

      defpred P[ DecoratedTree of the carrier of G] means for s be Terminal of G st ($1 . {} ) = s holds $1 = ( root-tree s);

      

       A2: for s be Symbol of G st s in ( Terminals G) holds P[( root-tree s)] by TREES_4: 3;

       A3:

      now

        let nt be Symbol of G, ts be FinSequence of ( TS G);

        assume that

         A4: nt ==> ( roots ts) and for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t];

        thus P[(nt -tree ts)]

        proof

          let s be Terminal of G;

          assume

           A5: ((nt -tree ts) . {} ) = s;

          

           A6: ((nt -tree ts) . {} ) = nt by TREES_4:def 4;

          

           A7: s in ( Terminals G);

          ( Terminals G) = { t where t be Symbol of G : not ex tnt be FinSequence st t ==> tnt } by LANG1:def 2;

          then ex t be Symbol of G st s = t & not ex tnt be FinSequence st t ==> tnt by A7;

          hence thesis by A4, A5, A6;

        end;

      end;

      for t be DecoratedTree of the carrier of G st t in ( TS G) holds P[t] from DTConstrInd( A2, A3);

      hence thesis by A1;

    end;

    theorem :: DTCONSTR:10

    

     Th10: for G be with_terminals with_nonterminals non empty DTConstrStr, tsg be Element of ( TS G), nt be NonTerminal of G st (tsg . {} ) = nt holds ex ts be FinSequence of ( TS G) st tsg = (nt -tree ts) & nt ==> ( roots ts)

    proof

      let G be with_terminals with_nonterminals non empty DTConstrStr;

      defpred P[ DecoratedTree of the carrier of G] means for nt be NonTerminal of G st ($1 . {} ) = nt holds ex ts be FinSequence of ( TS G) st $1 = (nt -tree ts) & nt ==> ( roots ts);

       A1:

      now

        let s be Symbol of G;

        assume

         A2: s in ( Terminals G);

        thus P[( root-tree s)]

        proof

          let nt be NonTerminal of G;

          assume (( root-tree s) . {} ) = nt;

          then

           A3: s = nt by TREES_4: 3;

          ( Terminals G) = { t where t be Symbol of G : not ex tnt be FinSequence st t ==> tnt } by LANG1:def 2;

          then

           A4: ex t be Symbol of G st s = t & not ex tnt be FinSequence st t ==> tnt by A2;

          

           A5: nt in ( NonTerminals G);

          ( NonTerminals G) = { t where t be Symbol of G : ex tnt be FinSequence st t ==> tnt } by LANG1:def 3;

          then ex t be Symbol of G st nt = t & ex tnt be FinSequence st t ==> tnt by A5;

          hence thesis by A3, A4;

        end;

      end;

       A6:

      now

        let nnt be Symbol of G, tts be FinSequence of ( TS G);

        assume that

         A7: nnt ==> ( roots tts) and for t be DecoratedTree of the carrier of G st t in ( rng tts) holds P[t];

        thus P[(nnt -tree tts)]

        proof

          let nt be NonTerminal of G;

          assume

           A8: ((nnt -tree tts) . {} ) = nt;

          take ts = tts;

          thus thesis by A7, A8, TREES_4:def 4;

        end;

      end;

      

       A9: for t be DecoratedTree of the carrier of G st t in ( TS G) holds P[t] from DTConstrInd( A1, A6);

      let tsg be Element of ( TS G), nt be NonTerminal of G;

      assume (tsg . {} ) = nt;

      hence thesis by A9;

    end;

    begin

    registration

      cluster PeanoNat -> with_terminals with_nonterminals with_useful_nonterminals;

      coherence by Lm16;

    end

    set PN = PeanoNat ;

    reconsider O as Terminal of PN by Lm9;

    reconsider S as NonTerminal of PN by Lm12;

    definition

      let nt be NonTerminal of PeanoNat , t be Element of ( TS PeanoNat );

      :: original: -tree

      redefine

      func nt -tree t -> Element of ( TS PeanoNat ) ;

      coherence

      proof

        reconsider r = {} as Node of t by TREES_1: 22;

        (t . r) = 0 or (t . r) = 1 by Lm2, TARSKI:def 2;

        then

         A1: ( roots <*t*>) = <* 0 *> or ( roots <*t*>) = <*1*> by Th4;

        nt = S by Lm15, TARSKI:def 1;

        then (nt -tree <*t*>) in ( TS PN) by A1, Def1, Lm5, Lm6;

        hence thesis by TREES_4:def 5;

      end;

    end

    definition

      let x be FinSequence of NAT ;

      :: DTCONSTR:def7

      func plus-one x -> Element of NAT equals ((x . 1) + 1);

      coherence ;

    end

    deffunc N( set, set, FinSequence of NAT ) = ( plus-one $3);

    definition

      :: DTCONSTR:def8

      func PN-to-NAT -> Function of ( TS PeanoNat ), NAT means

      : Def8: (for t be Symbol of PeanoNat st t in ( Terminals PeanoNat ) holds (it . ( root-tree t)) = 0 ) & for nt be Symbol of PeanoNat , ts be FinSequence of ( TS PeanoNat ) st nt ==> ( roots ts) holds (it . (nt -tree ts)) = ( plus-one (it * ts));

      existence

      proof

        thus ex f be Function of ( TS PeanoNat ), NAT st (for t be Symbol of PeanoNat st t in ( Terminals PeanoNat ) holds (f . ( root-tree t)) = T(t)) & for nt be Symbol of PeanoNat , ts be FinSequence of ( TS PeanoNat ) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = N(nt,roots,) from DTConstrIndDef;

      end;

      uniqueness

      proof

        let it1,it2 be Function of ( TS PeanoNat ), NAT such that

         A1: (for t be Symbol of PeanoNat st t in ( Terminals PeanoNat ) holds (it1 . ( root-tree t)) = T(t)) & for nt be Symbol of PeanoNat , ts be FinSequence of ( TS PeanoNat ) st nt ==> ( roots ts) holds (it1 . (nt -tree ts)) = N(nt,roots,) and

         A2: (for t be Symbol of PeanoNat st t in ( Terminals PeanoNat ) holds (it2 . ( root-tree t)) = T(t)) & for nt be Symbol of PeanoNat , ts be FinSequence of ( TS PeanoNat ) st nt ==> ( roots ts) holds (it2 . (nt -tree ts)) = N(nt,roots,);

        thus it1 = it2 from DTConstrUniqDef( A1, A2);

      end;

    end

    definition

      let x be Element of ( TS PeanoNat );

      :: DTCONSTR:def9

      func PNsucc x -> Element of ( TS PeanoNat ) equals (1 -tree <*x*>);

      coherence

      proof

        reconsider r = {} as Node of x by TREES_1: 22;

        

         A1: ( roots <*x*>) = <*(x . r)*> by Th4;

        (x . r) = O or (x . r) = S by Lm2, TARSKI:def 2;

        hence thesis by A1, Def1, Lm5, Lm6;

      end;

    end

    deffunc F( set, Element of ( TS PeanoNat )) = ( PNsucc $2);

    definition

      :: DTCONSTR:def10

      func NAT-to-PN -> sequence of ( TS PeanoNat ) means

      : Def10: (it . 0 ) = ( root-tree 0 ) & for n be Nat holds (it . (n + 1)) = ( PNsucc (it . n));

      existence

      proof

        ex f be sequence of ( TS PeanoNat ) st (f . 0 ) = ( root-tree O) & for n be Nat holds (f . (n + 1)) = F(n,) from NAT_1:sch 12;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be sequence of ( TS PeanoNat );

        assume

         A1: not thesis;

        then

         A2: (it1 . 0 ) = ( root-tree O);

        

         A3: for n be Nat holds (it1 . (n + 1)) = F(n,) by A1;

        

         A4: (it2 . 0 ) = ( root-tree O) by A1;

        

         A5: for n be Nat holds (it2 . (n + 1)) = F(n,) by A1;

        it1 = it2 from NAT_1:sch 16( A2, A3, A4, A5);

        hence thesis by A1;

      end;

    end

    theorem :: DTCONSTR:11

    for pn be Element of ( TS PeanoNat ) holds pn = ( NAT-to-PN . ( PN-to-NAT . pn))

    proof

      defpred P[ DecoratedTree of the carrier of PN] means $1 = ( NAT-to-PN . ( PN-to-NAT . $1));

       A1:

      now

        let s be Symbol of PN;

        assume

         A2: s in ( Terminals PN);

        

        then ( NAT-to-PN . ( PN-to-NAT . ( root-tree s))) = ( NAT-to-PN . 0 ) by Def8

        .= ( root-tree O) by Def10;

        hence P[( root-tree s)] by A2, Lm10, TARSKI:def 1;

      end;

       A3:

      now

        let nt be Symbol of PN, ts be FinSequence of ( TS PN);

        assume that

         A4: nt ==> ( roots ts) and

         A5: for t be DecoratedTree of the carrier of PN st t in ( rng ts) holds P[t];

        

         A6: nt <> O by A4, Lm8;

        ( roots ts) = <*O*> or ( roots ts) = <*S*> by A4, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider dt be Element of ( FinTrees the carrier of PN) such that

         A7: ts = <*dt*> and

         A8: dt in ( TS PN) by Th5;

        reconsider dt as Element of ( TS PN) by A8;

        ( rng ts) = {dt} by A7, FINSEQ_1: 38;

        then dt in ( rng ts) by TARSKI:def 1;

        then

         A9: dt = ( NAT-to-PN . ( PN-to-NAT . dt)) by A5;

        

         A10: ( PN-to-NAT * ts) = <*( PN-to-NAT . dt)*> by A7, FINSEQ_2: 35;

        set N = ( PN-to-NAT . dt);

        

         A11: ( plus-one <*N*>) = (N + 1) by FINSEQ_1: 40;

        ( NAT-to-PN . (N + 1)) = ( PNsucc dt) by A9, Def10

        .= (nt -tree ts) by A6, A7, Lm2, TARSKI:def 2;

        hence P[(nt -tree ts)] by A4, A10, A11, Def8;

      end;

      for t be DecoratedTree of the carrier of PN st t in ( TS PN) holds P[t] from DTConstrInd( A1, A3);

      hence thesis;

    end;

    

     Lm17: 0 = ( PN-to-NAT . ( root-tree O)) by Def8

    .= ( PN-to-NAT . ( NAT-to-PN . 0 )) by Def10;

     Lm18:

    now

      let n be Element of NAT ;

      assume

       A1: n = ( PN-to-NAT . ( NAT-to-PN . n));

      reconsider dt = ( NAT-to-PN . n) as Element of ( TS PN);

      reconsider r = {} as Node of dt by TREES_1: 22;

      

       A2: (dt . r) = O or (dt . r) = S by Lm2, TARSKI:def 2;

      

       A3: ( NAT-to-PN . (n + 1)) = ( PNsucc ( NAT-to-PN . n)) by Def10

      .= (S -tree <*( NAT-to-PN . n)*>);

      

       A4: S ==> ( roots <*( NAT-to-PN . n)*>) by A2, Lm3, Lm4, Th4;

       <*( PN-to-NAT . ( NAT-to-PN . n))*> = ( PN-to-NAT * <*( NAT-to-PN . n)*>) by FINSEQ_2: 35;

      

      then ( PN-to-NAT . (S -tree <*( NAT-to-PN . n)*>)) = ( plus-one <*n*>) by A1, A4, Def8

      .= (n + 1) by FINSEQ_1: 40;

      hence (n + 1) = ( PN-to-NAT . ( NAT-to-PN . (n + 1))) by A3;

    end;

    theorem :: DTCONSTR:12

    for n be Nat holds n = ( PN-to-NAT . ( NAT-to-PN . n))

    proof

      defpred P[ Nat] means $1 = ( PN-to-NAT . ( NAT-to-PN . $1));

      

       A1: P[ 0 ] by Lm17;

      

       A2: for n be Nat st P[n] holds P[(n + 1)] by Lm18;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

    end;

    begin

    definition

      let G be non empty DTConstrStr, tsg be DecoratedTree of the carrier of G;

      assume

       A1: tsg in ( TS G);

      defpred C[ object] means $1 in ( Terminals G);

      deffunc F( object) = <*$1*>;

      deffunc G( object) = {} ;

       A2:

      now

        let x be object;

        assume x in the carrier of G;

        hereby

          assume

           A3: C[x];

          then

          reconsider T = ( Terminals G) as non empty set;

          reconsider x9 = x as Element of T by A3;

           <*x9*> is FinSequence of T;

          hence F(x) in (( Terminals G) * );

        end;

        assume not C[x];

        ( <*> ( Terminals G)) = {} ;

        hence G(x) in (( Terminals G) * );

      end;

      consider s2t be Function of the carrier of G, (( Terminals G) * ) such that

       A4: for s be object st s in the carrier of G holds ( C[s] implies (s2t . s) = F(s)) & ( not C[s] implies (s2t . s) = G(s)) from FUNCT_2:sch 5( A2);

      deffunc T( Symbol of G) = (s2t . $1);

      deffunc N( set, set, FinSequence of (( Terminals G) * )) = ( FlattenSeq $3);

      deffunc F( object) = <*$1*>;

      :: DTCONSTR:def11

      func TerminalString tsg -> FinSequence of ( Terminals G) means

      : Def11: ex f be Function of ( TS G), (( Terminals G) * ) st it = (f . tsg) & (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = <*t*>) & for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = ( FlattenSeq (f * ts));

      existence

      proof

        consider f be Function of ( TS G), (( Terminals G) * ) such that

         A5: (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = T(t)) & for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = N(nt,roots,*) from DTConstrIndDef;

        (f . tsg) is Element of (( Terminals G) * ) by A1, FUNCT_2: 5;

        then

        reconsider IT = (f . tsg) as FinSequence of ( Terminals G);

        take IT, f;

        thus IT = (f . tsg);

        hereby

          let t be Symbol of G;

          assume

           A6: t in ( Terminals G);

          then (f . ( root-tree t)) = (s2t . t) by A5;

          hence (f . ( root-tree t)) = <*t*> by A4, A6;

        end;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of ( Terminals G);

        given f1 be Function of ( TS G), (( Terminals G) * ) such that

         A7: it1 = (f1 . tsg) and

         A8: for t be Symbol of G st t in ( Terminals G) holds (f1 . ( root-tree t)) = <*t*> and

         A9: for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f1 . (nt -tree ts)) = ( FlattenSeq (f1 * ts));

        given f2 be Function of ( TS G), (( Terminals G) * ) such that

         A10: it2 = (f2 . tsg) and

         A11: for t be Symbol of G st t in ( Terminals G) holds (f2 . ( root-tree t)) = <*t*> and

         A12: for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f2 . (nt -tree ts)) = ( FlattenSeq (f2 * ts));

         A13:

        now

          hereby

            let t be Symbol of G;

            assume

             A14: t in ( Terminals G);

            

            hence (f1 . ( root-tree t)) = <*t*> by A8

            .= T(t) by A4, A14;

          end;

          thus for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f1 . (nt -tree ts)) = N(nt,roots,*) by A9;

        end;

         A15:

        now

          hereby

            let t be Symbol of G;

            assume

             A16: t in ( Terminals G);

            

            hence (f2 . ( root-tree t)) = <*t*> by A11

            .= T(t) by A4, A16;

          end;

          thus for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f2 . (nt -tree ts)) = N(nt,roots,*) by A12;

        end;

        f1 = f2 from DTConstrUniqDef( A13, A15);

        hence thesis by A7, A10;

      end;

       A17:

      now

        let x be object;

        assume x in the carrier of G;

        then

        reconsider x9 = x as Element of G;

         <*x9*> is FinSequence of the carrier of G;

        hence F(x) in (the carrier of G * );

      end;

      consider s2s be Function of the carrier of G, (the carrier of G * ) such that

       A18: for s be object st s in the carrier of G holds (s2s . s) = F(s) from FUNCT_2:sch 2( A17);

      deffunc T( Symbol of G) = (s2s . $1);

      deffunc N( Symbol of G, set, FinSequence of (the carrier of G * )) = ((s2s . $1) ^ ( FlattenSeq $3));

      :: DTCONSTR:def12

      func PreTraversal tsg -> FinSequence of the carrier of G means

      : Def12: ex f be Function of ( TS G), (the carrier of G * ) st it = (f . tsg) & (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = <*t*>) & for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f * ts) holds (f . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq x));

      existence

      proof

        deffunc T( Symbol of G) = (s2s . $1);

        deffunc N( Symbol of G, set, FinSequence of (the carrier of G * )) = ((s2s . $1) ^ ( FlattenSeq $3));

        consider f be Function of ( TS G), (the carrier of G * ) such that

         A19: (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = T(t)) & for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = N(nt,roots,*) from DTConstrIndDef;

        (f . tsg) is Element of (the carrier of G * ) by A1, FUNCT_2: 5;

        then

        reconsider IT = (f . tsg) as FinSequence of the carrier of G;

        take IT, f;

        thus IT = (f . tsg);

        hereby

          let t be Symbol of G;

          assume t in ( Terminals G);

          then (f . ( root-tree t)) = (s2s . t) by A19;

          hence (f . ( root-tree t)) = <*t*> by A18;

        end;

        let nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence;

        assume that

         A20: rts = ( roots ts) and

         A21: nt ==> rts;

        let x be FinSequence of (the carrier of G * );

        assume x = (f * ts);

        

        hence (f . (nt -tree ts)) = ((s2s . nt) ^ ( FlattenSeq x)) by A19, A20, A21

        .= ( <*nt*> ^ ( FlattenSeq x)) by A18;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of the carrier of G;

        given f1 be Function of ( TS G), (the carrier of G * ) such that

         A22: it1 = (f1 . tsg) and

         A23: for t be Symbol of G st t in ( Terminals G) holds (f1 . ( root-tree t)) = <*t*> and

         A24: for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f1 * ts) holds (f1 . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq x));

        given f2 be Function of ( TS G), (the carrier of G * ) such that

         A25: it2 = (f2 . tsg) and

         A26: for t be Symbol of G st t in ( Terminals G) holds (f2 . ( root-tree t)) = <*t*> and

         A27: for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f2 * ts) holds (f2 . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq x));

         A28:

        now

          hereby

            let t be Symbol of G;

            assume t in ( Terminals G);

            

            hence (f1 . ( root-tree t)) = <*t*> by A23

            .= T(t) by A18;

          end;

          let nt be Symbol of G, ts be FinSequence of ( TS G);

          assume nt ==> ( roots ts);

          

          hence (f1 . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq (f1 * ts))) by A24

          .= N(nt,roots,*) by A18;

        end;

         A29:

        now

          hereby

            let t be Symbol of G;

            assume t in ( Terminals G);

            

            hence (f2 . ( root-tree t)) = <*t*> by A26

            .= T(t) by A18;

          end;

          let nt be Symbol of G, ts be FinSequence of ( TS G);

          assume nt ==> ( roots ts);

          

          hence (f2 . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq (f2 * ts))) by A27

          .= N(nt,roots,*) by A18;

        end;

        f1 = f2 from DTConstrUniqDef( A28, A29);

        hence thesis by A22, A25;

      end;

      deffunc T( Symbol of G) = (s2s . $1);

      deffunc N( Symbol of G, set, FinSequence of (the carrier of G * )) = (( FlattenSeq $3) ^ (s2s . $1));

      :: DTCONSTR:def13

      func PostTraversal tsg -> FinSequence of the carrier of G means

      : Def13: ex f be Function of ( TS G), (the carrier of G * ) st it = (f . tsg) & (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = <*t*>) & for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f * ts) holds (f . (nt -tree ts)) = (( FlattenSeq x) ^ <*nt*>);

      existence

      proof

        consider f be Function of ( TS G), (the carrier of G * ) such that

         A30: (for t be Symbol of G st t in ( Terminals G) holds (f . ( root-tree t)) = T(t)) & for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = N(nt,roots,*) from DTConstrIndDef;

        (f . tsg) is Element of (the carrier of G * ) by A1, FUNCT_2: 5;

        then

        reconsider IT = (f . tsg) as FinSequence of the carrier of G;

        take IT, f;

        thus IT = (f . tsg);

        hereby

          let t be Symbol of G;

          assume t in ( Terminals G);

          then (f . ( root-tree t)) = (s2s . t) by A30;

          hence (f . ( root-tree t)) = <*t*> by A18;

        end;

        let nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence;

        assume that

         A31: rts = ( roots ts) and

         A32: nt ==> rts;

        let x be FinSequence of (the carrier of G * );

        assume x = (f * ts);

        

        hence (f . (nt -tree ts)) = (( FlattenSeq x) ^ (s2s . nt)) by A30, A31, A32

        .= (( FlattenSeq x) ^ <*nt*>) by A18;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of the carrier of G;

        given f1 be Function of ( TS G), (the carrier of G * ) such that

         A33: it1 = (f1 . tsg) and

         A34: for t be Symbol of G st t in ( Terminals G) holds (f1 . ( root-tree t)) = <*t*> and

         A35: for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f1 * ts) holds (f1 . (nt -tree ts)) = (( FlattenSeq x) ^ <*nt*>);

        given f2 be Function of ( TS G), (the carrier of G * ) such that

         A36: it2 = (f2 . tsg) and

         A37: for t be Symbol of G st t in ( Terminals G) holds (f2 . ( root-tree t)) = <*t*> and

         A38: for nt be Symbol of G, ts be FinSequence of ( TS G), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of G * ) st x = (f2 * ts) holds (f2 . (nt -tree ts)) = (( FlattenSeq x) ^ <*nt*>);

         A39:

        now

          hereby

            let t be Symbol of G;

            assume t in ( Terminals G);

            

            hence (f1 . ( root-tree t)) = <*t*> by A34

            .= T(t) by A18;

          end;

          let nt be Symbol of G, ts be FinSequence of ( TS G);

          assume nt ==> ( roots ts);

          

          hence (f1 . (nt -tree ts)) = (( FlattenSeq (f1 * ts)) ^ <*nt*>) by A35

          .= N(nt,roots,*) by A18;

        end;

         A40:

        now

          hereby

            let t be Symbol of G;

            assume t in ( Terminals G);

            

            hence (f2 . ( root-tree t)) = <*t*> by A37

            .= T(t) by A18;

          end;

          let nt be Symbol of G, ts be FinSequence of ( TS G);

          assume nt ==> ( roots ts);

          

          hence (f2 . (nt -tree ts)) = (( FlattenSeq (f2 * ts)) ^ <*nt*>) by A38

          .= N(nt,roots,*) by A18;

        end;

        f1 = f2 from DTConstrUniqDef( A39, A40);

        hence thesis by A33, A36;

      end;

    end

    definition

      let G be with_nonterminals non empty non empty DTConstrStr, nt be Symbol of G;

      :: DTCONSTR:def14

      func TerminalLanguage nt -> Subset of (( Terminals G) * ) equals { ( TerminalString tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

      coherence

      proof

        set TL = { ( TerminalString tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

        TL c= (( Terminals G) * )

        proof

          let x be object;

          assume x in TL;

          then ex tsg be Element of ( FinTrees the carrier of G) st (x = ( TerminalString tsg)) & (tsg in ( TS G)) & ((tsg . {} ) = nt);

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

      :: DTCONSTR:def15

      func PreTraversalLanguage nt -> Subset of (the carrier of G * ) equals { ( PreTraversal tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

      coherence

      proof

        set TL = { ( PreTraversal tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

        TL c= (the carrier of G * )

        proof

          let x be object;

          assume x in TL;

          then ex tsg be Element of ( FinTrees the carrier of G) st (x = ( PreTraversal tsg)) & (tsg in ( TS G)) & ((tsg . {} ) = nt);

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

      :: DTCONSTR:def16

      func PostTraversalLanguage nt -> Subset of (the carrier of G * ) equals { ( PostTraversal tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

      coherence

      proof

        set TL = { ( PostTraversal tsg) where tsg be Element of ( FinTrees the carrier of G) : tsg in ( TS G) & (tsg . {} ) = nt };

        TL c= (the carrier of G * )

        proof

          let x be object;

          assume x in TL;

          then ex tsg be Element of ( FinTrees the carrier of G) st (x = ( PostTraversal tsg)) & (tsg in ( TS G)) & ((tsg . {} ) = nt);

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    theorem :: DTCONSTR:13

    

     Th13: for t be DecoratedTree of the carrier of PeanoNat st t in ( TS PeanoNat ) holds ( TerminalString t) = <* 0 *>

    proof

      consider f be Function of ( TS PN), (( Terminals PN) * ) such that

       A1: ( TerminalString ( root-tree O qua Symbol of PN)) = (f . ( root-tree O)) and

       A2: for t be Symbol of PN st t in ( Terminals PN) holds (f . ( root-tree t)) = <*t*> and

       A3: for nt be Symbol of PN, ts be FinSequence of ( TS PN) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = ( FlattenSeq (f * ts)) by Def11;

      defpred P[ DecoratedTree of the carrier of PN] means ( TerminalString $1) = <* 0 *>;

       A4:

      now

        let s be Symbol of PN;

        assume s in ( Terminals PN);

        then s = O by Lm10, TARSKI:def 1;

        hence P[( root-tree s)] by A1, A2;

      end;

       A5:

      now

        let nt be Symbol of PN, ts be FinSequence of ( TS PN);

        assume that

         A6: nt ==> ( roots ts) and

         A7: for t be DecoratedTree of the carrier of PN st t in ( rng ts) holds P[t];

        

         A8: (nt -tree ts) in ( TS PN) by A6, Def1;

        ( roots ts) = <*O*> or ( roots ts) = <*1*> by A6, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider x be Element of ( FinTrees the carrier of PN) such that

         A9: ts = <*x*> and

         A10: x in ( TS PN) by Th5;

        reconsider x9 = x as Element of ( TS PN) by A10;

        ( rng ts) = {x} by A9, FINSEQ_1: 39;

        then

         A11: x in ( rng ts) by TARSKI:def 1;

        (f . x9) is Element of (( Terminals PN) * );

        

        then

         A12: (f . x9) = ( TerminalString x) by A2, A3, Def11

        .= <*O*> by A7, A11;

        (f * ts) = <*(f . x)*> by A9, FINSEQ_2: 35;

        

        then (f . (nt -tree ts)) = ( FlattenSeq <*(f . x9)*>) by A3, A6

        .= <*O*> by A12, PRE_POLY: 1;

        hence P[(nt -tree ts)] by A2, A3, A8, Def11;

      end;

      thus for t be DecoratedTree of the carrier of PN st t in ( TS PN) holds P[t] from DTConstrInd( A4, A5);

    end;

    theorem :: DTCONSTR:14

    for nt be Symbol of PeanoNat holds ( TerminalLanguage nt) = { <* 0 *>}

    proof

      let nt be Symbol of PeanoNat ;

      

       A1: nt = S or nt = O by Lm2, TARSKI:def 2;

      hereby

        let x be object;

        assume x in ( TerminalLanguage nt);

        then ex tsg be Element of ( FinTrees the carrier of PN) st x = ( TerminalString tsg) & tsg in ( TS PN) & (tsg . {} ) = nt;

        then x = <*O*> by Th13;

        hence x in { <* 0 *>} by TARSKI:def 1;

      end;

      let x be object;

      assume x in { <* 0 *>};

      then

       A2: x = <*O*> by TARSKI:def 1;

      reconsider prtO = ( root-tree O) as Element of ( TS PN) qua non empty set;

      reconsider rtO = ( root-tree O) as Element of ( TS PN);

      reconsider srtO = <*prtO*> as FinSequence of ( TS PN);

      

       A3: (rtO . {} ) = O by TREES_4: 3;

      then S ==> ( roots <*rtO*>) by Lm5, Th4;

      then

       A4: (S -tree <*prtO*>) in ( TS PN) by Def1;

      then

       A5: ( TerminalString (S -tree srtO)) = x by A2, Th13;

      

       A6: ((S -tree <*rtO*>) . {} ) = S by TREES_4:def 4;

      ( TerminalString rtO) = x by A2, Th13;

      hence thesis by A1, A3, A4, A5, A6;

    end;

    theorem :: DTCONSTR:15

    

     Th15: for t be Element of ( TS PeanoNat ) holds ( PreTraversal t) = ((( height ( dom t)) |-> 1) ^ <* 0 *>)

    proof

      consider f be Function of ( TS PN), (the carrier of PN * ) such that

       A1: ( PreTraversal ( root-tree O qua Symbol of PN)) = (f . ( root-tree O)) and

       A2: for t be Symbol of PN st t in ( Terminals PN) holds (f . ( root-tree t)) = <*t*> and

       A3: for nt be Symbol of PN, ts be FinSequence of ( TS PN), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of PN * ) st x = (f * ts) holds (f . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq x)) by Def12;

      reconsider rtO = ( root-tree O) as Element of ( TS PN);

      defpred P[ DecoratedTree of the carrier of PN] means ex t be Element of ( TS PN) st $1 = t & ( PreTraversal t) = ((( height ( dom t)) |-> 1) ^ <* 0 *>);

       A4:

      now

        let s be Symbol of PN;

        assume

         A5: s in ( Terminals PN);

        thus P[( root-tree s)]

        proof

          take t = rtO;

          thus ( root-tree s) = t by A5, Lm10, TARSKI:def 1;

          

          thus ( PreTraversal t) = <*O*> by A1, A2

          .= ( {} ^ <*O*>) by FINSEQ_1: 34

          .= (( 0 |-> 1) ^ <* 0 *>)

          .= ((( height ( dom t)) |-> 1) ^ <* 0 *>) by TREES_1: 42, TREES_4: 3;

        end;

      end;

       A6:

      now

        let nt be Symbol of PN, ts be FinSequence of ( TS PN);

        assume that

         A7: nt ==> ( roots ts) and

         A8: for t be DecoratedTree of the carrier of PN st t in ( rng ts) holds P[t];

        reconsider t9 = (nt -tree ts) as Element of ( TS PN) by A7, Def1;

        

         A9: nt = S by A7, Def2;

        ( roots ts) = <*O*> or ( roots ts) = <*1*> by A7, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider x be Element of ( FinTrees the carrier of PN) such that

         A10: ts = <*x*> and

         A11: x in ( TS PN) by Th5;

        reconsider x9 = x as Element of ( TS PN) by A11;

        ( rng ts) = {x} by A10, FINSEQ_1: 39;

        then x in ( rng ts) by TARSKI:def 1;

        then

         A12: ex t9 be Element of ( TS PN) st x = t9 & ( PreTraversal t9) = ((( height ( dom t9)) |-> 1) ^ <* 0 *>) by A8;

        (f . x9) is Element of (the carrier of PN * );

        then

         A13: (f . x9) = ((( height ( dom x9)) |-> 1) ^ <* 0 *>) by A2, A3, A12, Def12;

        (f * ts) = <*(f . x)*> by A10, FINSEQ_2: 35;

        

        then

         A14: (f . (nt -tree ts)) = ( <*nt*> ^ ( FlattenSeq <*(f . x9)*>)) by A3, A7

        .= ( <*nt*> ^ ((( height ( dom x9)) |-> 1) ^ <* 0 *>)) by A13, PRE_POLY: 1

        .= (( <*nt*> ^ (( height ( dom x9)) |-> 1)) ^ <* 0 *>) by FINSEQ_1: 32

        .= (((1 |-> 1) ^ (( height ( dom x9)) |-> 1)) ^ <* 0 *>) by A9, FINSEQ_2: 59

        .= (((( height ( dom x9)) + 1) |-> 1) ^ <* 0 *>) by FINSEQ_2: 123

        .= ((( height ( ^ ( dom x9))) |-> 1) ^ <* 0 *>) by TREES_3: 80;

        

         A15: ( dom (nt -tree x9)) = ( ^ ( dom x9)) by TREES_4: 13;

        

         A16: t9 = (nt -tree x9) by A10, TREES_4:def 5;

        (f . t9) is Element of (the carrier of PN * );

        then ( PreTraversal (nt -tree ts)) = (f . (nt -tree ts)) by A2, A3, Def12;

        hence P[(nt -tree ts)] by A14, A15, A16;

      end;

      

       A17: for t be DecoratedTree of the carrier of PN st t in ( TS PN) holds P[t] from DTConstrInd( A4, A6);

      let t be Element of ( TS PeanoNat );

       P[t] by A17;

      hence thesis;

    end;

    theorem :: DTCONSTR:16

    for nt be Symbol of PeanoNat holds (nt = 0 implies ( PreTraversalLanguage nt) = { <* 0 *>}) & (nt = 1 implies ( PreTraversalLanguage nt) = { ((n |-> 1) ^ <* 0 *>) where n be Element of NAT : n <> 0 })

    proof

      let nt be Symbol of PeanoNat ;

      reconsider rtO = ( root-tree O) as Element of ( TS PN);

      ( height ( dom ( root-tree 0 ))) = 0 by TREES_1: 42, TREES_4: 3;

      then ( PreTraversal rtO) = (( 0 |-> 1) ^ <*O*>) by Th15;

      

      then

       A1: ( PreTraversal rtO) = ( {} ^ <*O*>)

      .= <*O*> by FINSEQ_1: 34;

      thus nt = 0 implies ( PreTraversalLanguage nt) = { <* 0 *>}

      proof

        assume

         A2: nt = 0 ;

        hereby

          let x be object;

          assume x in ( PreTraversalLanguage nt);

          then

          consider tsg be Element of ( FinTrees the carrier of PN) such that

           A3: x = ( PreTraversal tsg) and

           A4: tsg in ( TS PN) and

           A5: (tsg . {} ) = O by A2;

          tsg = ( root-tree O) by A4, A5, Th9;

          hence x in { <* 0 *>} by A1, A3, TARSKI:def 1;

        end;

        let x be object;

        assume x in { <* 0 *>};

        then

         A6: x = <*O*> by TARSKI:def 1;

        (rtO . {} ) = O by TREES_4: 3;

        hence thesis by A1, A2, A6;

      end;

      assume

       A7: nt = 1;

      hereby

        let x be object;

        assume x in ( PreTraversalLanguage nt);

        then

        consider tsg be Element of ( FinTrees the carrier of PN) such that

         A8: x = ( PreTraversal tsg) and

         A9: tsg in ( TS PN) and

         A10: (tsg . {} ) = S by A7;

        consider ts be FinSequence of ( TS PN) such that

         A11: tsg = (S -tree ts) and

         A12: S ==> ( roots ts) by A9, A10, Th10;

        ( roots ts) = <* 0 *> or ( roots ts) = <*1*> by A12, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider t be Element of ( FinTrees the carrier of PN) such that

         A13: ts = <*t*> and t in ( TS PN) by Th5;

        tsg = (S -tree t) by A11, A13, TREES_4:def 5;

        then ( dom tsg) = ( ^ ( dom t)) by TREES_4: 13;

        then

         A14: ( height ( dom tsg)) = (( height ( dom t)) + 1) by TREES_3: 80;

        x = ((( height ( dom tsg)) |-> 1) ^ <* 0 *>) by A8, A9, Th15;

        hence x in { ((n |-> 1) ^ <* 0 *>) where n be Element of NAT : n <> 0 } by A14;

      end;

      let x be object;

      assume x in { ((n |-> 1) ^ <* 0 *>) where n be Element of NAT : n <> 0 };

      then

      consider n be Element of NAT such that

       A15: x = ((n |-> 1) ^ <* 0 *>) and

       A16: n <> 0 ;

      defpred P[ Nat] means $1 <> 0 implies ex tsg be Element of ( TS PN) st (tsg . {} ) = S & ( PreTraversal tsg) = (($1 |-> 1) ^ <* 0 *>);

      

       A17: P[ 0 ];

       A18:

      now

        let n be Nat;

        assume

         A19: P[n];

        thus P[(n + 1)]

        proof

          assume (n + 1) <> 0 ;

          per cases ;

            suppose n <> 0 ;

            then

            consider tsg be Element of ( TS PN) such that (tsg . {} ) = S and

             A20: ( PreTraversal tsg) = ((n |-> 1) ^ <* 0 *>) by A19;

            ( PreTraversal tsg) = ((( height ( dom tsg)) |-> 1) ^ <* 0 *>) by Th15;

            then

             A21: (n |-> 1) = (( height ( dom tsg)) |-> 1) by A20, FINSEQ_1: 33;

            ( len (n |-> 1)) = n by CARD_1:def 7;

            then

             A22: ( height ( dom tsg)) = n by A21, CARD_1:def 7;

            take tsg9 = (S -tree tsg);

            

             A23: tsg9 = (S -tree <*tsg*>) by TREES_4:def 5;

            ( height ( dom tsg9)) = ( height ( ^ ( dom tsg))) by TREES_4: 13

            .= (n + 1) by A22, TREES_3: 80;

            hence thesis by A23, Th15, TREES_4:def 4;

          end;

            suppose

             A24: n = 0 ;

            take tsg9 = (S -tree rtO);

            

             A25: tsg9 = (S -tree <*rtO*>) by TREES_4:def 5;

            ( height ( dom tsg9)) = ( height ( ^ ( dom rtO))) by TREES_4: 13

            .= (( height ( dom rtO)) + 1) by TREES_3: 80

            .= (n + 1) by A24, TREES_1: 42, TREES_4: 3;

            hence thesis by A25, Th15, TREES_4:def 4;

          end;

        end;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A18);

      then ex tsg be Element of ( TS PN) st (tsg . {} ) = S & ( PreTraversal tsg) = ((n |-> 1) ^ <* 0 *>) by A16;

      hence thesis by A7, A15;

    end;

    theorem :: DTCONSTR:17

    

     Th17: for t be Element of ( TS PeanoNat ) holds ( PostTraversal t) = ( <* 0 *> ^ (( height ( dom t)) |-> 1))

    proof

      consider f be Function of ( TS PN), (the carrier of PN * ) such that

       A1: ( PostTraversal ( root-tree O qua Symbol of PN)) = (f . ( root-tree O)) and

       A2: for t be Symbol of PN st t in ( Terminals PN) holds (f . ( root-tree t)) = <*t*> and

       A3: for nt be Symbol of PN, ts be FinSequence of ( TS PN), rts be FinSequence st rts = ( roots ts) & nt ==> rts holds for x be FinSequence of (the carrier of PN * ) st x = (f * ts) holds (f . (nt -tree ts)) = (( FlattenSeq x) ^ <*nt*>) by Def13;

      reconsider rtO = ( root-tree O) as Element of ( TS PN);

      defpred P[ DecoratedTree of the carrier of PN] means ex t be Element of ( TS PN) st $1 = t & ( PostTraversal t) = ( <* 0 *> ^ (( height ( dom t)) |-> 1));

       A4:

      now

        let s be Symbol of PN;

        assume

         A5: s in ( Terminals PN);

        thus P[( root-tree s)]

        proof

          take t = rtO;

          thus ( root-tree s) = t by A5, Lm10, TARSKI:def 1;

          

          thus ( PostTraversal t) = <*O*> by A1, A2

          .= ( <*O*> ^ {} ) by FINSEQ_1: 34

          .= ( <* 0 *> ^ ( 0 |-> 1))

          .= ( <* 0 *> ^ (( height ( dom t)) |-> 1)) by TREES_1: 42, TREES_4: 3;

        end;

      end;

       A6:

      now

        let nt be Symbol of PN, ts be FinSequence of ( TS PN);

        assume that

         A7: nt ==> ( roots ts) and

         A8: for t be DecoratedTree of the carrier of PN st t in ( rng ts) holds P[t];

        reconsider t9 = (nt -tree ts) as Element of ( TS PN) by A7, Def1;

        

         A9: nt = S by A7, Def2;

        ( roots ts) = <*O*> or ( roots ts) = <*1*> by A7, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider x be Element of ( FinTrees the carrier of PN) such that

         A10: ts = <*x*> and

         A11: x in ( TS PN) by Th5;

        reconsider x9 = x as Element of ( TS PN) by A11;

        ( rng ts) = {x} by A10, FINSEQ_1: 39;

        then x in ( rng ts) by TARSKI:def 1;

        then

         A12: ex t9 be Element of ( TS PN) st x = t9 & ( PostTraversal t9) = ( <*O*> ^ (( height ( dom t9)) |-> 1)) by A8;

        (f . x9) is Element of (the carrier of PN * );

        then

         A13: (f . x9) = ( <*O*> ^ (( height ( dom x9)) |-> 1)) by A2, A3, A12, Def13;

        (f * ts) = <*(f . x)*> by A10, FINSEQ_2: 35;

        

        then

         A14: (f . (nt -tree ts)) = (( FlattenSeq <*(f . x9)*>) ^ <*nt*>) by A3, A7

        .= (( <*O*> ^ (( height ( dom x9)) |-> 1)) ^ <*nt*>) by A13, PRE_POLY: 1

        .= ( <*O*> ^ ((( height ( dom x9)) |-> 1) ^ <*nt*>)) by FINSEQ_1: 32

        .= ( <*O*> ^ ((( height ( dom x9)) |-> 1) ^ (1 |-> 1))) by A9, FINSEQ_2: 59

        .= ( <*O*> ^ ((( height ( dom x9)) + 1) |-> 1)) by FINSEQ_2: 123

        .= ( <*O*> ^ (( height ( ^ ( dom x9))) |-> 1)) by TREES_3: 80;

        

         A15: ( dom (nt -tree x9)) = ( ^ ( dom x9)) by TREES_4: 13;

        

         A16: t9 = (nt -tree x9) by A10, TREES_4:def 5;

        (f . t9) is Element of (the carrier of PN * );

        then ( PostTraversal (nt -tree ts)) = (f . (nt -tree ts)) by A2, A3, Def13;

        hence P[(nt -tree ts)] by A14, A15, A16;

      end;

      

       A17: for t be DecoratedTree of the carrier of PN st t in ( TS PN) holds P[t] from DTConstrInd( A4, A6);

      let t be Element of ( TS PeanoNat );

       P[t] by A17;

      hence thesis;

    end;

    theorem :: DTCONSTR:18

    for nt be Symbol of PeanoNat holds (nt = 0 implies ( PostTraversalLanguage nt) = { <* 0 *>}) & (nt = 1 implies ( PostTraversalLanguage nt) = { ( <* 0 *> ^ (n |-> 1)) where n be Element of NAT : n <> 0 })

    proof

      let nt be Symbol of PeanoNat ;

      reconsider rtO = ( root-tree O) as Element of ( TS PN);

      ( height ( dom ( root-tree 0 ))) = 0 by TREES_1: 42, TREES_4: 3;

      then ( PostTraversal rtO) = ( <* 0 *> ^ ( 0 |-> 1)) by Th17;

      

      then

       A1: ( PostTraversal rtO) = ( <*O*> ^ {} )

      .= <*O*> by FINSEQ_1: 34;

      thus nt = 0 implies ( PostTraversalLanguage nt) = { <* 0 *>}

      proof

        assume

         A2: nt = 0 ;

        hereby

          let x be object;

          assume x in ( PostTraversalLanguage nt);

          then

          consider tsg be Element of ( FinTrees the carrier of PN) such that

           A3: x = ( PostTraversal tsg) and

           A4: tsg in ( TS PN) and

           A5: (tsg . {} ) = O by A2;

          tsg = ( root-tree O) by A4, A5, Th9;

          hence x in { <* 0 *>} by A1, A3, TARSKI:def 1;

        end;

        let x be object;

        assume x in { <* 0 *>};

        then

         A6: x = <*O*> by TARSKI:def 1;

        (rtO . {} ) = O by TREES_4: 3;

        hence thesis by A1, A2, A6;

      end;

      assume

       A7: nt = 1;

      hereby

        let x be object;

        assume x in ( PostTraversalLanguage nt);

        then

        consider tsg be Element of ( FinTrees the carrier of PN) such that

         A8: x = ( PostTraversal tsg) and

         A9: tsg in ( TS PN) and

         A10: (tsg . {} ) = S by A7;

        consider ts be FinSequence of ( TS PN) such that

         A11: tsg = (S -tree ts) and

         A12: S ==> ( roots ts) by A9, A10, Th10;

        ( roots ts) = <* 0 *> or ( roots ts) = <*1*> by A12, Def2;

        then ( len ( roots ts)) = 1 by FINSEQ_1: 40;

        then

        consider t be Element of ( FinTrees the carrier of PN) such that

         A13: ts = <*t*> and t in ( TS PN) by Th5;

        tsg = (S -tree t) by A11, A13, TREES_4:def 5;

        then ( dom tsg) = ( ^ ( dom t)) by TREES_4: 13;

        then

         A14: ( height ( dom tsg)) = (( height ( dom t)) + 1) by TREES_3: 80;

        x = ( <* 0 *> ^ (( height ( dom tsg)) |-> 1)) by A8, A9, Th17;

        hence x in { ( <* 0 *> ^ (n |-> 1)) where n be Element of NAT : n <> 0 } by A14;

      end;

      let x be object;

      assume x in { ( <* 0 *> ^ (n |-> 1)) where n be Element of NAT : n <> 0 };

      then

      consider n be Element of NAT such that

       A15: x = ( <* 0 *> ^ (n |-> 1)) and

       A16: n <> 0 ;

      defpred P[ Nat] means $1 <> 0 implies ex tsg be Element of ( TS PN) st (tsg . {} ) = S & ( PostTraversal tsg) = ( <* 0 *> ^ ($1 |-> 1));

      

       A17: P[ 0 ];

       A18:

      now

        let n be Nat;

        assume

         A19: P[n];

        thus P[(n + 1)]

        proof

          assume (n + 1) <> 0 ;

          per cases ;

            suppose n <> 0 ;

            then

            consider tsg be Element of ( TS PN) such that (tsg . {} ) = S and

             A20: ( PostTraversal tsg) = ( <* 0 *> ^ (n |-> 1)) by A19;

            ( PostTraversal tsg) = ( <* 0 *> ^ (( height ( dom tsg)) |-> 1)) by Th17;

            then

             A21: (n |-> 1) = (( height ( dom tsg)) |-> 1) by A20, FINSEQ_1: 33;

            ( len (n |-> 1)) = n by CARD_1:def 7;

            then

             A22: ( height ( dom tsg)) = n by A21, CARD_1:def 7;

            take tsg9 = (S -tree tsg);

            

             A23: tsg9 = (S -tree <*tsg*>) by TREES_4:def 5;

            ( height ( dom tsg9)) = ( height ( ^ ( dom tsg))) by TREES_4: 13

            .= (n + 1) by A22, TREES_3: 80;

            hence thesis by A23, Th17, TREES_4:def 4;

          end;

            suppose

             A24: n = 0 ;

            take tsg9 = (S -tree rtO);

            

             A25: tsg9 = (S -tree <*rtO*>) by TREES_4:def 5;

            ( height ( dom tsg9)) = ( height ( ^ ( dom rtO))) by TREES_4: 13

            .= (( height ( dom rtO)) + 1) by TREES_3: 80

            .= (n + 1) by A24, TREES_1: 42, TREES_4: 3;

            hence thesis by A25, Th17, TREES_4:def 4;

          end;

        end;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A18);

      then ex tsg be Element of ( TS PN) st (tsg . {} ) = S & ( PostTraversal tsg) = ( <* 0 *> ^ (n |-> 1)) by A16;

      hence thesis by A7, A15;

    end;