bintree1.miz



    begin

    definition

      let D be non empty set, t be DecoratedTree of D;

      :: BINTREE1:def1

      func root-label t -> Element of D equals (t . {} );

      coherence

      proof

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

        (t . r) is Element of D;

        hence thesis;

      end;

    end

    theorem :: BINTREE1:1

    for D be non empty set, t be DecoratedTree of D holds ( roots <*t*>) = <*( root-label t)*> by DTCONSTR: 4;

    theorem :: BINTREE1:2

    for D be non empty set, t1,t2 be DecoratedTree of D holds ( roots <*t1, t2*>) = <*( root-label t1), ( root-label t2)*> by DTCONSTR: 6;

    definition

      let IT be Tree;

      :: BINTREE1:def2

      attr IT is binary means for t be Element of IT st not t in ( Leaves IT) holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)};

    end

    theorem :: BINTREE1:3

    for T be Tree, t be Element of T holds ( succ t) = {} iff t in ( Leaves T)

    proof

      let T be Tree, t be Element of T;

      hereby

        assume ( succ t) = {} ;

        then not (t ^ <* 0 *>) in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } by TREES_2:def 5;

        then not (t ^ <* 0 *>) in T;

        hence t in ( Leaves T) by TREES_1: 54;

      end;

      set x = the Element of ( succ t);

      assume t in ( Leaves T);

      then

       A1: not (t ^ <* 0 *>) in T by TREES_1: 54;

      assume ( succ t) <> {} ;

      then x in ( succ t);

      then x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } by TREES_2:def 5;

      then

      consider n be Nat such that x = (t ^ <*n*>) and

       A2: (t ^ <*n*>) in T;

       0 <= n by NAT_1: 2;

      hence contradiction by A1, A2, TREES_1:def 3;

    end;

    registration

      cluster ( elementary_tree 0 ) -> binary;

      coherence

      proof

        set T = ( elementary_tree 0 );

        let t be Element of T;

        now

          let s be FinSequence of NAT ;

          assume s in T;

          then s = {} by TARSKI:def 1, TREES_1: 29;

          hence not t is_a_proper_prefix_of s by TARSKI:def 1, TREES_1: 29;

        end;

        hence thesis by TREES_1:def 5;

      end;

      cluster ( elementary_tree 2) -> binary;

      coherence

      proof

        set T = ( elementary_tree 2);

        let t be Element of T;

        assume

         A1: not t in ( Leaves T);

        per cases by ENUMSET1:def 1, TREES_1: 53;

          suppose

           A2: t = {} ;

          

           A3: for x be object holds x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } iff x in {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let x be object;

            hereby

              assume x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T };

              then

               A4: ex n be Nat st x = (t ^ <*n*>) & (t ^ <*n*>) in T;

              then

              reconsider x9 = x as FinSequence;

              per cases by A4, ENUMSET1:def 1, TREES_1: 53;

                suppose x = {} ;

                hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by A4;

              end;

                suppose x = <* 0 *>;

                then x9 = (t ^ <* 0 *>) by A2, FINSEQ_1: 34;

                hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

              end;

                suppose x = <*1*>;

                then x9 = (t ^ <*1*>) by A2, FINSEQ_1: 34;

                hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

              end;

            end;

            assume

             A5: x in {(t ^ <* 0 *>), (t ^ <*1*>)};

            then

            reconsider x9 = x as FinSequence by TARSKI:def 2;

            

             A6: x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A5, TARSKI:def 2;

            then x9 = <* 0 *> or x9 = <*1*> by A2, FINSEQ_1: 34;

            then x9 in T by ENUMSET1:def 1, TREES_1: 53;

            hence thesis by A6;

          end;

          ( succ t) = { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } by TREES_2:def 5;

          hence thesis by A3, TARSKI: 2;

        end;

          suppose

           A7: t = <* 0 *>;

          now

            assume

             A8: (t ^ <* 0 *>) in T;

            per cases by A8, ENUMSET1:def 1, TREES_1: 53;

              suppose (t ^ <* 0 *>) = {} ;

              hence contradiction;

            end;

              suppose (t ^ <* 0 *>) = <* 0 *>;

              then (( len <* 0 *>) + ( len <* 0 *>)) = ( len <* 0 *>) by A7, FINSEQ_1: 22;

              hence contradiction by FINSEQ_1: 39;

            end;

              suppose (t ^ <* 0 *>) = <*1*>;

              then (( len <* 0 *>) + ( len <* 0 *>)) = ( len <*1*>) by A7, FINSEQ_1: 22;

              then (1 + ( len <* 0 *>)) = ( len <*1*>) by FINSEQ_1: 39;

              then (1 + 1) = ( len <*1*>) by FINSEQ_1: 39;

              hence contradiction by FINSEQ_1: 39;

            end;

          end;

          hence thesis by A1, TREES_1: 54;

        end;

          suppose

           A9: t = <*1*>;

          now

            assume

             A10: (t ^ <* 0 *>) in T;

            per cases by A10, ENUMSET1:def 1, TREES_1: 53;

              suppose (t ^ <* 0 *>) = {} ;

              hence contradiction;

            end;

              suppose (t ^ <* 0 *>) = <* 0 *>;

              then (( len <*1*>) + ( len <* 0 *>)) = ( len <* 0 *>) by A9, FINSEQ_1: 22;

              hence contradiction by FINSEQ_1: 39;

            end;

              suppose (t ^ <* 0 *>) = <*1*>;

              then (( len <*1*>) + ( len <* 0 *>)) = ( len <*1*>) by A9, FINSEQ_1: 22;

              hence contradiction by FINSEQ_1: 39;

            end;

          end;

          hence thesis by A1, TREES_1: 54;

        end;

      end;

    end

    theorem :: BINTREE1:4

    ( elementary_tree 0 ) is binary;

    theorem :: BINTREE1:5

    ( elementary_tree 2) is binary;

    registration

      cluster binary finite for Tree;

      existence

      proof

        take ( elementary_tree 0 );

        thus thesis;

      end;

    end

    definition

      let IT be DecoratedTree;

      :: BINTREE1:def3

      attr IT is binary means

      : Def3: ( dom IT) is binary;

    end

    registration

      let D be non empty set;

      cluster binary finite for DecoratedTree of D;

      existence

      proof

        set t = the binary finite Tree;

        set T = the Function of t, D;

        reconsider T as DecoratedTree of D;

        take T;

        thus ( dom T) is binary & T is finite by FUNCT_2:def 1;

      end;

    end

    registration

      cluster binary finite for DecoratedTree;

      existence

      proof

        set t = the binary finite DecoratedTree of { {} };

        take t;

        thus thesis;

      end;

    end

    registration

      cluster binary -> finite-order for Tree;

      coherence

      proof

        let T be Tree;

        assume

         A1: T is binary;

        now

          let t be Element of T;

          assume

           A2: (t ^ <*2*>) in T;

          then

           A3: (t ^ <* 0 *>) in T by TREES_1:def 3;

          per cases ;

            suppose t in ( Leaves T);

            hence contradiction by A3, TREES_1: 54;

          end;

            suppose

             A4: not t in ( Leaves T);

             A5:

            now

              

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

              assume <*2*> = <* 0 *>;

              hence contradiction by A6, FINSEQ_1: 40;

            end;

             A7:

            now

              

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

              assume <*2*> = <*1*>;

              hence contradiction by A8, FINSEQ_1: 40;

            end;

            (t ^ <*2*>) in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } by A2;

            then

             A9: (t ^ <*2*>) in ( succ t) by TREES_2:def 5;

            ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by A1, A4;

            then (t ^ <*2*>) = (t ^ <* 0 *>) or (t ^ <*2*>) = (t ^ <*1*>) by A9, TARSKI:def 2;

            hence contradiction by A5, A7, FINSEQ_1: 33;

          end;

        end;

        hence thesis by TREES_2:def 2;

      end;

    end

    theorem :: BINTREE1:6

    

     Th6: for T0,T1 be Tree, t be Element of ( tree (T0,T1)) holds (for p be Element of T0 st t = ( <* 0 *> ^ p) holds t in ( Leaves ( tree (T0,T1))) iff p in ( Leaves T0)) & for p be Element of T1 st t = ( <*1*> ^ p) holds t in ( Leaves ( tree (T0,T1))) iff p in ( Leaves T1)

    proof

      let T0,T1 be Tree, t be Element of ( tree (T0,T1));

      set RT = ( tree (T0,T1));

      hereby

        let p be Element of T0;

        assume

         A1: t = ( <* 0 *> ^ p);

        hereby

          assume

           A2: t in ( Leaves RT);

          assume not p in ( Leaves T0);

          then

          consider n be Nat such that

           A3: (p ^ <*n*>) in T0 by TREES_1: 55;

          ( <* 0 *> ^ (p ^ <*n*>)) in RT by A3, TREES_3: 69;

          then (( <* 0 *> ^ p) ^ <*n*>) in RT by FINSEQ_1: 32;

          hence contradiction by A1, A2, TREES_1: 55;

        end;

        assume

         A4: p in ( Leaves T0);

        assume not t in ( Leaves RT);

        then

        consider n be Nat such that

         A5: (t ^ <*n*>) in RT by TREES_1: 55;

        ( <* 0 *> ^ (p ^ <*n*>)) in RT by A1, A5, FINSEQ_1: 32;

        then (p ^ <*n*>) in T0 by TREES_3: 69;

        hence contradiction by A4, TREES_1: 55;

      end;

      let p be Element of T1;

      assume

       A6: t = ( <*1*> ^ p);

      hereby

        assume

         A7: t in ( Leaves RT);

        assume not p in ( Leaves T1);

        then

        consider n be Nat such that

         A8: (p ^ <*n*>) in T1 by TREES_1: 55;

        ( <*1*> ^ (p ^ <*n*>)) in RT by A8, TREES_3: 70;

        then (( <*1*> ^ p) ^ <*n*>) in RT by FINSEQ_1: 32;

        hence contradiction by A6, A7, TREES_1: 55;

      end;

      assume

       A9: p in ( Leaves T1);

      assume not t in ( Leaves RT);

      then

      consider n be Nat such that

       A10: (t ^ <*n*>) in RT by TREES_1: 55;

      ( <*1*> ^ (p ^ <*n*>)) in RT by A6, A10, FINSEQ_1: 32;

      then (p ^ <*n*>) in T1 by TREES_3: 70;

      hence contradiction by A9, TREES_1: 55;

    end;

    theorem :: BINTREE1:7

    

     Th7: for T0,T1 be Tree, t be Element of ( tree (T0,T1)) holds (t = {} implies ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)}) & (for p be Element of T0 st t = ( <* 0 *> ^ p) holds for sp be FinSequence holds sp in ( succ p) iff ( <* 0 *> ^ sp) in ( succ t)) & for p be Element of T1 st t = ( <*1*> ^ p) holds for sp be FinSequence holds sp in ( succ p) iff ( <*1*> ^ sp) in ( succ t)

    proof

      let T0,T1 be Tree, t be Element of ( tree (T0,T1));

      set RT = ( tree (T0,T1));

      hereby

        assume

         A1: t = {} ;

         {} in T1 & <*1*> = ( <*1*> ^ {} ) by FINSEQ_1: 34, TREES_1: 22;

        then <*1*> in RT by TREES_3: 68;

        then

         A2: (t ^ <*1*>) in RT by A1, FINSEQ_1: 34;

        

         A3: ( succ t) = { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in RT } by TREES_2:def 5;

         {} in T0 & <* 0 *> = ( <* 0 *> ^ {} ) by FINSEQ_1: 34, TREES_1: 22;

        then <* 0 *> in RT by TREES_3: 68;

        then

         A4: (t ^ <* 0 *>) in RT by A1, FINSEQ_1: 34;

        now

          let x1 be object;

          hereby

            assume x1 in ( succ t);

            then

            consider n be Nat such that

             A5: x1 = (t ^ <*n*>) and

             A6: (t ^ <*n*>) in RT by A3;

            reconsider x = x1 as FinSequence by A5;

            ex p be FinSequence st (p in T0 & x = ( <* 0 *> ^ p) or p in T1 & x = ( <*1*> ^ p)) by A5, A6, TREES_3: 68;

            then

             A7: (x . 1) = 0 or (x . 1) = 1 by FINSEQ_1: 41;

            x1 = <*n*> by A1, A5, FINSEQ_1: 34;

            then x = <* 0 *> or x = <*1*> by A7, FINSEQ_1: 40;

            then x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A1, FINSEQ_1: 34;

            hence x1 in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

          end;

          assume x1 in {(t ^ <* 0 *>), (t ^ <*1*>)};

          then x1 = (t ^ <* 0 *>) or x1 = (t ^ <*1*>) by TARSKI:def 2;

          hence x1 in ( succ t) by A3, A4, A2;

        end;

        hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI: 2;

      end;

      hereby

        let p be Element of T0 such that

         A8: t = ( <* 0 *> ^ p);

        let sp be FinSequence;

        hereby

          assume sp in ( succ p);

          then sp in { (p ^ <*n*>) where n be Nat : (p ^ <*n*>) in T0 } by TREES_2:def 5;

          then

          consider n be Nat such that

           A9: sp = (p ^ <*n*>) and

           A10: (p ^ <*n*>) in T0;

          ( <* 0 *> ^ (p ^ <*n*>)) in RT by A10, TREES_3: 69;

          then (( <* 0 *> ^ p) ^ <*n*>) in RT by FINSEQ_1: 32;

          then (t ^ <*n*>) in { (t ^ <*k*>) where k be Nat : (t ^ <*k*>) in RT } by A8;

          then (t ^ <*n*>) in ( succ t) by TREES_2:def 5;

          hence ( <* 0 *> ^ sp) in ( succ t) by A8, A9, FINSEQ_1: 32;

        end;

        set zsp = ( <* 0 *> ^ sp);

        assume zsp in ( succ t);

        then zsp in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in RT } by TREES_2:def 5;

        then

        consider n be Nat such that

         A11: zsp = (t ^ <*n*>) and

         A12: (t ^ <*n*>) in RT;

        ( <* 0 *> ^ (p ^ <*n*>)) in RT by A8, A12, FINSEQ_1: 32;

        then (p ^ <*n*>) in T0 by TREES_3: 69;

        then (p ^ <*n*>) in { (p ^ <*k*>) where k be Nat : (p ^ <*k*>) in T0 };

        then

         A13: (p ^ <*n*>) in ( succ p) by TREES_2:def 5;

        ( <* 0 *> ^ sp) = ( <* 0 *> ^ (p ^ <*n*>)) by A8, A11, FINSEQ_1: 32;

        hence sp in ( succ p) by A13, FINSEQ_1: 33;

      end;

      let p be Element of T1 such that

       A14: t = ( <*1*> ^ p);

      let sp be FinSequence;

      hereby

        assume sp in ( succ p);

        then sp in { (p ^ <*n*>) where n be Nat : (p ^ <*n*>) in T1 } by TREES_2:def 5;

        then

        consider n be Nat such that

         A15: sp = (p ^ <*n*>) and

         A16: (p ^ <*n*>) in T1;

        ( <*1*> ^ (p ^ <*n*>)) in RT by A16, TREES_3: 70;

        then (( <*1*> ^ p) ^ <*n*>) in RT by FINSEQ_1: 32;

        then (t ^ <*n*>) in { (t ^ <*k*>) where k be Nat : (t ^ <*k*>) in RT } by A14;

        then (t ^ <*n*>) in ( succ t) by TREES_2:def 5;

        hence ( <*1*> ^ sp) in ( succ t) by A14, A15, FINSEQ_1: 32;

      end;

      set zsp = ( <*1*> ^ sp);

      assume zsp in ( succ t);

      then zsp in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in RT } by TREES_2:def 5;

      then

      consider n be Nat such that

       A17: zsp = (t ^ <*n*>) and

       A18: (t ^ <*n*>) in RT;

      ( <*1*> ^ (p ^ <*n*>)) in RT by A14, A18, FINSEQ_1: 32;

      then (p ^ <*n*>) in T1 by TREES_3: 70;

      then (p ^ <*n*>) in { (p ^ <*k*>) where k be Nat : (p ^ <*k*>) in T1 };

      then

       A19: (p ^ <*n*>) in ( succ p) by TREES_2:def 5;

      ( <*1*> ^ sp) = ( <*1*> ^ (p ^ <*n*>)) by A14, A17, FINSEQ_1: 32;

      hence thesis by A19, FINSEQ_1: 33;

    end;

    theorem :: BINTREE1:8

    

     Th8: for T1,T2 be Tree holds T1 is binary & T2 is binary iff ( tree (T1,T2)) is binary

    proof

      let T1,T2 be Tree;

      set RT = ( tree (T1,T2));

      hereby

        assume that

         A1: T1 is binary and

         A2: T2 is binary;

        now

          let t be Element of RT;

          assume

           A3: not t in ( Leaves RT);

          per cases by TREES_3: 68;

            suppose t = {} ;

            hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by Th7;

          end;

            suppose ex p be FinSequence st p in T1 & t = ( <* 0 *> ^ p) or p in T2 & t = ( <*1*> ^ p);

            then

            consider p be FinSequence such that

             A4: p in T1 & t = ( <* 0 *> ^ p) or p in T2 & t = ( <*1*> ^ p);

             A5:

            now

              assume that

               A6: p in T2 and

               A7: t = ( <*1*> ^ p);

              reconsider p as Element of T2 by A6;

              per cases ;

                suppose p in ( Leaves T2);

                hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by A3, A7, Th6;

              end;

                suppose not p in ( Leaves T2);

                then

                 A8: ( succ p) = {(p ^ <* 0 *>), (p ^ <*1*>)} by A2;

                now

                  let x be object;

                  hereby

                    assume

                     A9: x in ( succ t);

                    then x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in RT } by TREES_2:def 5;

                    then

                    consider n be Nat such that

                     A10: x = (t ^ <*n*>) and

                     A11: (t ^ <*n*>) in RT;

                    

                     A12: x = ( <*1*> ^ (p ^ <*n*>)) by A7, A10, FINSEQ_1: 32;

                    then

                    reconsider pn = (p ^ <*n*>) as Element of T2 by A10, A11, TREES_3: 70;

                    pn in ( succ p) by A7, A9, A12, Th7;

                    then pn = (p ^ <* 0 *>) or pn = (p ^ <*1*>) by A8, TARSKI:def 2;

                    then x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A10, FINSEQ_1: 33;

                    hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

                  end;

                  assume x in {(t ^ <* 0 *>), (t ^ <*1*>)};

                  then x = (( <*1*> ^ p) ^ <* 0 *>) or x = (( <*1*> ^ p) ^ <*1*>) by A7, TARSKI:def 2;

                  then

                   A13: x = ( <*1*> ^ (p ^ <* 0 *>)) or x = ( <*1*> ^ (p ^ <*1*>)) by FINSEQ_1: 32;

                  (p ^ <* 0 *>) in ( succ p) & (p ^ <*1*>) in ( succ p) by A8, TARSKI:def 2;

                  hence x in ( succ t) by A7, A13, Th7;

                end;

                hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI: 2;

              end;

            end;

            now

              assume that

               A14: p in T1 and

               A15: t = ( <* 0 *> ^ p);

              reconsider p as Element of T1 by A14;

              per cases ;

                suppose p in ( Leaves T1);

                hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by A3, A15, Th6;

              end;

                suppose not p in ( Leaves T1);

                then

                 A16: ( succ p) = {(p ^ <* 0 *>), (p ^ <*1*>)} by A1;

                now

                  let x be object;

                  hereby

                    assume

                     A17: x in ( succ t);

                    then x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in RT } by TREES_2:def 5;

                    then

                    consider n be Nat such that

                     A18: x = (t ^ <*n*>) and

                     A19: (t ^ <*n*>) in RT;

                    

                     A20: x = ( <* 0 *> ^ (p ^ <*n*>)) by A15, A18, FINSEQ_1: 32;

                    then

                    reconsider pn = (p ^ <*n*>) as Element of T1 by A18, A19, TREES_3: 69;

                    pn in ( succ p) by A15, A17, A20, Th7;

                    then pn = (p ^ <* 0 *>) or pn = (p ^ <*1*>) by A16, TARSKI:def 2;

                    then x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A18, FINSEQ_1: 33;

                    hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

                  end;

                  assume x in {(t ^ <* 0 *>), (t ^ <*1*>)};

                  then x = (( <* 0 *> ^ p) ^ <* 0 *>) or x = (( <* 0 *> ^ p) ^ <*1*>) by A15, TARSKI:def 2;

                  then

                   A21: x = ( <* 0 *> ^ (p ^ <* 0 *>)) or x = ( <* 0 *> ^ (p ^ <*1*>)) by FINSEQ_1: 32;

                  (p ^ <* 0 *>) in ( succ p) & (p ^ <*1*>) in ( succ p) by A16, TARSKI:def 2;

                  hence x in ( succ t) by A15, A21, Th7;

                end;

                hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI: 2;

              end;

            end;

            hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by A4, A5;

          end;

        end;

        hence ( tree (T1,T2)) is binary;

      end;

      assume

       A22: RT is binary;

      now

        let t be Element of T1;

        reconsider zt = ( <* 0 *> ^ t) as Element of RT by TREES_3: 69;

        assume not t in ( Leaves T1);

        then not zt in ( Leaves RT) by Th6;

        then

         A23: ( succ zt) = {(( <* 0 *> ^ t) ^ <* 0 *>), (( <* 0 *> ^ t) ^ <*1*>)} by A22;

        

         A24: ( succ zt) = { (zt ^ <*n*>) where n be Nat : (zt ^ <*n*>) in RT } by TREES_2:def 5;

        now

          let x be object;

          hereby

            assume x in ( succ t);

            then x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T1 } by TREES_2:def 5;

            then

            consider n be Nat such that

             A25: x = (t ^ <*n*>) and

             A26: (t ^ <*n*>) in T1;

            ( <* 0 *> ^ (t ^ <*n*>)) in RT by A26, TREES_3: 69;

            then (zt ^ <*n*>) in RT by FINSEQ_1: 32;

            then (zt ^ <*n*>) in { (zt ^ <*k*>) where k be Nat : (zt ^ <*k*>) in RT };

            then (zt ^ <*n*>) = (zt ^ <* 0 *>) or (zt ^ <*n*>) = (zt ^ <*1*>) by A23, A24, TARSKI:def 2;

            then x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A25, FINSEQ_1: 33;

            hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

          end;

          assume x in {(t ^ <* 0 *>), (t ^ <*1*>)};

          then

           A27: x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by TARSKI:def 2;

          (( <* 0 *> ^ t) ^ <*1*>) in ( succ zt) by A23, TARSKI:def 2;

          then

           A28: ( <* 0 *> ^ (t ^ <*1*>)) in ( succ zt) by FINSEQ_1: 32;

          (( <* 0 *> ^ t) ^ <* 0 *>) in ( succ zt) by A23, TARSKI:def 2;

          then ( <* 0 *> ^ (t ^ <* 0 *>)) in ( succ zt) by FINSEQ_1: 32;

          hence x in ( succ t) by A27, A28, Th7;

        end;

        hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI: 2;

      end;

      hence T1 is binary;

      now

        let t be Element of T2;

        reconsider zt = ( <*1*> ^ t) as Element of RT by TREES_3: 70;

        assume not t in ( Leaves T2);

        then not zt in ( Leaves RT) by Th6;

        then

         A29: ( succ zt) = {(( <*1*> ^ t) ^ <* 0 *>), (( <*1*> ^ t) ^ <*1*>)} by A22;

        

         A30: ( succ zt) = { (zt ^ <*n*>) where n be Nat : (zt ^ <*n*>) in RT } by TREES_2:def 5;

        now

          let x be object;

          hereby

            assume x in ( succ t);

            then x in { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T2 } by TREES_2:def 5;

            then

            consider n be Nat such that

             A31: x = (t ^ <*n*>) and

             A32: (t ^ <*n*>) in T2;

            ( <*1*> ^ (t ^ <*n*>)) in RT by A32, TREES_3: 70;

            then (zt ^ <*n*>) in RT by FINSEQ_1: 32;

            then (zt ^ <*n*>) in { (zt ^ <*k*>) where k be Nat : (zt ^ <*k*>) in RT };

            then (zt ^ <*n*>) = (zt ^ <* 0 *>) or (zt ^ <*n*>) = (zt ^ <*1*>) by A29, A30, TARSKI:def 2;

            then x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by A31, FINSEQ_1: 33;

            hence x in {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI:def 2;

          end;

          assume x in {(t ^ <* 0 *>), (t ^ <*1*>)};

          then

           A33: x = (t ^ <* 0 *>) or x = (t ^ <*1*>) by TARSKI:def 2;

          (( <*1*> ^ t) ^ <*1*>) in ( succ zt) by A29, TARSKI:def 2;

          then

           A34: ( <*1*> ^ (t ^ <*1*>)) in ( succ zt) by FINSEQ_1: 32;

          (( <*1*> ^ t) ^ <* 0 *>) in ( succ zt) by A29, TARSKI:def 2;

          then ( <*1*> ^ (t ^ <* 0 *>)) in ( succ zt) by FINSEQ_1: 32;

          hence x in ( succ t) by A33, A34, Th7;

        end;

        hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: BINTREE1:9

    

     Th9: for T1,T2 be DecoratedTree, x be set holds T1 is binary & T2 is binary iff (x -tree (T1,T2)) is binary

    proof

      let T1,T2 be DecoratedTree, x be set;

      hereby

        assume T1 is binary & T2 is binary;

        then ( dom T1) is binary & ( dom T2) is binary;

        then

         A1: ( tree (( dom T1),( dom T2))) is binary by Th8;

        ( dom (x -tree (T1,T2))) = ( tree (( dom T1),( dom T2))) by TREES_4: 14;

        hence (x -tree (T1,T2)) is binary by A1;

      end;

      assume (x -tree (T1,T2)) is binary;

      then

       A2: ( dom (x -tree (T1,T2))) is binary;

      ( dom (x -tree (T1,T2))) = ( tree (( dom T1),( dom T2))) by TREES_4: 14;

      then ( dom T1) is binary & ( dom T2) is binary by A2, Th8;

      hence thesis;

    end;

    registration

      let D be non empty set, x be Element of D, T1,T2 be binary finite DecoratedTree of D;

      cluster (x -tree (T1,T2)) -> binary finiteD -valued;

      coherence

      proof

        set t1t2 = <*T1, T2*>;

        ( dom T1) is finite;

        then

         A1: T1 in ( FinTrees D) by TREES_3:def 8;

        ( dom T2) is finite;

        then

         A2: T2 in ( FinTrees D) by TREES_3:def 8;

        ( rng <*T1, T2*>) = ( rng ( <*T1*> ^ <*T2*>)) by FINSEQ_1:def 9

        .= (( rng <*T1*>) \/ ( rng <*T2*>)) by FINSEQ_1: 31

        .= ( {T1} \/ ( rng <*T2*>)) by FINSEQ_1: 39

        .= ( {T1} \/ {T2}) by FINSEQ_1: 39

        .= {T1, T2} by ENUMSET1: 1;

        then for x be object st x in ( rng t1t2) holds x in ( FinTrees D) by A1, A2, TARSKI:def 2;

        then ( rng t1t2) c= ( FinTrees D) by TARSKI:def 3;

        then

        reconsider T1T2 = t1t2 as FinSequence of ( FinTrees D) by FINSEQ_1:def 4;

        (x -tree (T1,T2)) = (x -tree T1T2) by TREES_4:def 6;

        then ( dom (x -tree (T1,T2))) is finite;

        hence thesis by Th9, FINSET_1: 10;

      end;

    end

    definition

      let IT be non empty DTConstrStr;

      :: BINTREE1:def4

      attr IT is binary means

      : Def4: for s be Symbol of IT, p be FinSequence st s ==> p holds ex x1,x2 be Symbol of IT st p = <*x1, x2*>;

    end

    registration

      cluster binary with_terminals with_nonterminals with_useful_nonterminals strict for non empty DTConstrStr;

      existence

      proof

        reconsider 01 = { 0 , 1} as non empty set;

        reconsider a90 = 0 , a91 = 1 as Element of 01 by TARSKI:def 2;

        reconsider a9119 = ( <*a91*> ^ <*a91*>) as Element of (01 * );

        reconsider P = { [a90, a9119]} as Relation of 01, (01 * );

        take cherry = DTConstrStr (# 01, P #);

        reconsider a90, a91 as Symbol of cherry;

        hereby

          let s be Symbol of cherry, p be FinSequence;

          assume

           A1: s ==> p;

          take x1 = a91, x2 = a91;

           [s, p] in P by A1, LANG1:def 1;

          then [s, p] = [ 0 , a9119] by TARSKI:def 1;

          

          then p = a9119 by XTUPLE_0: 1

          .= <*1, 1*> by FINSEQ_1:def 9;

          hence p = <*x1, x2*>;

        end;

        now

          let s be FinSequence;

          assume a91 ==> s;

          then [1, s] in P by LANG1:def 1;

          then [1, s] = [ 0 , a9119] by TARSKI:def 1;

          hence contradiction by XTUPLE_0: 1;

        end;

        then

         A2: a91 in { t where t be Symbol of cherry : not ex s be FinSequence st t ==> s };

        then

         A3: a91 in ( Terminals cherry) by LANG1:def 2;

        thus ( Terminals cherry) <> {} by A2, LANG1:def 2;

         [a90, a9119] in P by TARSKI:def 1;

        then a90 ==> a9119 by LANG1:def 1;

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

        hence ( NonTerminals cherry) <> {} by LANG1:def 3;

        

         A4: { s where s be Symbol of cherry : ex p be FinSequence st s ==> p } = ( NonTerminals cherry) by LANG1:def 3;

        hereby

          reconsider X = ( TS cherry) as non empty set by A3, DTCONSTR:def 1;

          let nt be Symbol of cherry;

          reconsider rt1 = ( root-tree a91) as Element of X by A3, DTCONSTR:def 1;

          reconsider q = ( <*rt1*> ^ <*rt1*>) as FinSequence of ( TS cherry);

          q = <*( root-tree 1), ( root-tree 1)*> by FINSEQ_1:def 9;

          then

           A5: ( roots q) = <*(( root-tree a91) . {} ), (( root-tree a91) . {} )*> by DTCONSTR: 6;

          assume nt in ( NonTerminals cherry);

          then ex s be Symbol of cherry st nt = s & ex p be FinSequence st s ==> p by A4;

          then

          consider p be FinSequence such that

           A6: nt ==> p;

          take q9 = q;

           [nt, p] in P by A6, LANG1:def 1;

          then

           A7: [nt, p] = [ 0 , a9119] by TARSKI:def 1;

          a9119 = <*1, 1*> & (( root-tree 1) . {} ) = 1 by FINSEQ_1:def 9, TREES_4: 3;

          hence nt ==> ( roots q9) by A6, A7, A5, XTUPLE_0: 1;

        end;

        thus thesis;

      end;

    end

    scheme :: BINTREE1:sch1

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

ex G be binary strict non empty DTConstrStr st the carrier of G = S() & for x,y,z be Symbol of G holds x ==> <*y, z*> iff P[x, y, z];

      defpred Q[ set, FinSequence] means P[$1, ($2 . 1), ($2 . 2)] & $2 = <*($2 . 1), ($2 . 2)*>;

      consider G be strict non empty DTConstrStr such that

       A1: the carrier of G = S() and

       A2: for x be Symbol of G, p be FinSequence of the carrier of G holds x ==> p iff Q[x, p] from DTCONSTR:sch 1;

      now

        let s be Symbol of G, p be FinSequence;

        assume

         A3: s ==> p;

        then [s, p] in the Rules of G by LANG1:def 1;

        then p in (the carrier of G * ) by ZFMISC_1: 87;

        then

        reconsider pp = p as FinSequence of the carrier of G by FINSEQ_1:def 11;

        pp = <*(pp . 1), (pp . 2)*> by A2, A3;

        

        then ( rng pp) = ( rng ( <*(pp . 1)*> ^ <*(pp . 2)*>)) by FINSEQ_1:def 9

        .= (( rng <*(pp . 1)*>) \/ ( rng <*(pp . 2)*>)) by FINSEQ_1: 31

        .= ( {(pp . 1)} \/ ( rng <*(pp . 2)*>)) by FINSEQ_1: 39

        .= ( {(pp . 1)} \/ {(pp . 2)}) by FINSEQ_1: 39

        .= {(pp . 1), (pp . 2)} by ENUMSET1: 1;

        then (pp . 1) in ( rng pp) & (pp . 2) in ( rng pp) by TARSKI:def 2;

        then

        reconsider pp1 = (pp . 1), pp2 = (pp . 2) as Symbol of G;

        take pp1, pp2;

        thus p = <*pp1, pp2*> by A2, A3;

      end;

      then

       A4: G is binary;

      now

        let x,y,z be Symbol of G;

        reconsider yz = <*y, z*> as FinSequence of the carrier of G;

        (yz . 1) = y & (yz . 2) = z by FINSEQ_1: 44;

        hence x ==> <*y, z*> iff P[x, y, z] by A2;

      end;

      hence thesis by A1, A4;

    end;

    theorem :: BINTREE1:10

    

     Th10: for G be binary with_terminals with_nonterminals non empty DTConstrStr, ts be FinSequence of ( TS G), nt be Symbol of G st nt ==> ( roots ts) holds nt is NonTerminal of G & ( dom ts) = {1, 2} & 1 in ( dom ts) & 2 in ( dom ts) & ex tl,tr be Element of ( TS G) st ( roots ts) = <*( root-label tl), ( root-label tr)*> & tl = (ts . 1) & tr = (ts . 2) & (nt -tree ts) = (nt -tree (tl,tr)) & tl in ( rng ts) & tr in ( rng ts)

    proof

      let G be binary with_terminals with_nonterminals non empty DTConstrStr, ts be FinSequence of ( TS G), nt be Symbol of G;

      assume

       A1: nt ==> ( roots ts);

      then

      consider rtl,rtr be Symbol of G such that

       A2: ( roots ts) = <*rtl, rtr*> by Def4;

      nt in { s where s be Symbol of G : ex rts be FinSequence st s ==> rts } by A1;

      hence nt is NonTerminal of G by LANG1:def 3;

      

       A3: ( len <*rtl, rtr*>) = 2 by FINSEQ_1: 44;

      

       A4: ( dom <*rtl, rtr*>) = ( dom ts) by A2, TREES_3:def 18;

      hence ( dom ts) = {1, 2} by A3, FINSEQ_1: 2, FINSEQ_1:def 3;

      hence

       A5: 1 in ( dom ts) & 2 in ( dom ts) by TARSKI:def 2;

      then

      consider tl be DecoratedTree such that

       A6: tl = (ts . 1) and

       A7: ( <*rtl, rtr*> . 1) = (tl . {} ) by A2, TREES_3:def 18;

      

       A8: ( rng ts) c= ( TS G) & tl in ( rng ts) by A5, A6, FINSEQ_1:def 4, FUNCT_1:def 3;

      consider tr be DecoratedTree such that

       A9: tr = (ts . 2) and

       A10: ( <*rtl, rtr*> . 2) = (tr . {} ) by A2, A5, TREES_3:def 18;

      tr in ( rng ts) by A5, A9, FUNCT_1:def 3;

      then

      reconsider tl, tr as Element of ( TS G) by A8;

      take tl, tr;

      ( <*rtl, rtr*> . 1) = rtl by FINSEQ_1: 44;

      hence ( roots ts) = <*( root-label tl), ( root-label tr)*> by A2, A7, A10, FINSEQ_1: 44;

      ( Seg ( len <*rtl, rtr*>)) = ( dom <*rtl, rtr*>) by FINSEQ_1:def 3

      .= ( Seg ( len ts)) by A4, FINSEQ_1:def 3;

      then ( len ts) = 2 by A3, FINSEQ_1: 6;

      then ts = <*tl, tr*> by A6, A9, FINSEQ_1: 44;

      hence tl = (ts . 1) & tr = (ts . 2) & (nt -tree ts) = (nt -tree (tl,tr)) by A6, A9, TREES_4:def 6;

      thus thesis by A5, A6, A9, FUNCT_1:def 3;

    end;

    scheme :: BINTREE1:sch2

    BinDTConstrInd { G() -> binary with_terminals with_nonterminals non empty DTConstrStr , P[ set] } :

for t be Element of ( TS G()) holds P[t]

      provided

       A1: for s be Terminal of G() holds P[( root-tree s)]

       and

       A2: for nt be NonTerminal of G(), tl,tr be Element of ( TS G()) st nt ==> <*( root-label tl), ( root-label tr)*> & P[tl] & P[tr] holds P[(nt -tree (tl,tr))];

      

       A3: 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)]

      proof

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

         A4: nt ==> ( roots ts) and

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

        

         A6: nt is NonTerminal of G() by A4, Th10;

        consider tl,tr be Element of ( TS G()) such that

         A7: ( roots ts) = <*( root-label tl), ( root-label tr)*> and tl = (ts . 1) and tr = (ts . 2) and

         A8: (nt -tree ts) = (nt -tree (tl,tr)) and

         A9: tl in ( rng ts) & tr in ( rng ts) by A4, Th10;

        P[tl] & P[tr] by A5, A9;

        hence thesis by A2, A4, A6, A7, A8;

      end;

      

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

      for t be DecoratedTree of the carrier of G() st t in ( TS G()) holds P[t] from DTCONSTR:sch 7( A10, A3);

      hence thesis;

    end;

    scheme :: BINTREE1:sch3

    BinDTConstrIndDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr , D() -> non empty set , TermVal( set) -> Element of D() , NTermVal( set, set, set, set, set) -> Element of D() } :

ex f be Function of ( TS G()), D() st (for t be Terminal of G() holds (f . ( root-tree t)) = TermVal(t)) & for nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of D() st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = NTermVal(nt,rtl,rtr,xl,xr);

      deffunc BNTV( Symbol of G(), FinSequence, FinSequence of D()) = NTermVal($1,.,.,.,.);

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

       A1: for t be Symbol of G() st t in ( Terminals G()) holds (f . ( root-tree t)) = TermVal(t) and

       A2: for nt be Symbol of G(), ts be FinSequence of ( TS G()) st nt ==> ( roots ts) holds (f . (nt -tree ts)) = BNTV(nt,roots,*) from DTCONSTR:sch 8;

      take f;

      thus for t be Terminal of G() holds (f . ( root-tree t)) = TermVal(t) by A1;

      let nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G();

      assume that

       A3: rtl = ( root-label tl) and

       A4: rtr = ( root-label tr) and

       A5: nt ==> <*rtl, rtr*>;

      reconsider rts = <*rtl, rtr*> as FinSequence;

      reconsider ts = <*tl, tr*> as FinSequence of ( TS G());

      

       A6: (ts . 1) = tl by FINSEQ_1: 44;

      let xl,xr be Element of D();

      

       A7: ( dom ts) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      reconsider x = <*xl, xr*> as FinSequence of D();

      

       A8: ( dom x) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      

       A9: (ts . 2) = tr by FINSEQ_1: 44;

      

       A10: ( dom f) = ( TS G()) by FUNCT_2:def 1;

       A11:

      now

        let y be object;

         A12:

        now

          assume that

           A13: y in ( dom ts) and (ts . y) in ( dom f);

          per cases by A7, A13, TARSKI:def 2;

            suppose y = 1;

            hence y in ( dom x) by A8, TARSKI:def 2;

          end;

            suppose y = 2;

            hence y in ( dom x) by A8, TARSKI:def 2;

          end;

        end;

        now

          assume

           A14: y in ( dom x);

          per cases by A8, A14, TARSKI:def 2;

            suppose y = 1;

            hence y in ( dom ts) & (ts . y) in ( dom f) by A10, A6, A7, TARSKI:def 2;

          end;

            suppose y = 2;

            hence y in ( dom ts) & (ts . y) in ( dom f) by A10, A9, A7, TARSKI:def 2;

          end;

        end;

        hence y in ( dom x) iff y in ( dom ts) & (ts . y) in ( dom f) by A12;

      end;

      assume

       A15: xl = (f . tl) & xr = (f . tr);

      now

        let y be object;

        assume y in ( dom x);

        then y = 1 or y = 2 by A8, TARSKI:def 2;

        hence (x . y) = (f . (ts . y)) by A15, A6, A9, FINSEQ_1: 44;

      end;

      then

       A16: x = (f * ts) by A11, FUNCT_1: 10;

      

       A17: (rts . 2) = rtr by FINSEQ_1: 44;

      

       A18: (rts . 1) = rtl by FINSEQ_1: 44;

       A19:

      now

        let i be Element of NAT ;

        assume i in ( dom ts);

        then i in ( Seg ( len ts)) by FINSEQ_1:def 3;

        then

         A20: i in ( Seg 2) by FINSEQ_1: 44;

        per cases by A20, FINSEQ_1: 2, TARSKI:def 2;

          suppose i = 1;

          hence ex T be DecoratedTree st T = (ts . i) & (rts . i) = (T . {} ) by A3, A6, A18;

        end;

          suppose i = 2;

          hence ex T be DecoratedTree st T = (ts . i) & (rts . i) = (T . {} ) by A4, A9, A17;

        end;

      end;

      ( dom rts) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then rts = ( roots ts) by A7, A19, TREES_3:def 18;

      then

       A21: (f . (nt -tree ts)) = NTermVal(nt,.,.,.,.) by A2, A5, A16;

      

       A22: (x . 1) = xl & (x . 2) = xr by FINSEQ_1: 44;

      (rts . 1) = rtl & (rts . 2) = rtr by FINSEQ_1: 44;

      hence thesis by A21, A22, TREES_4:def 6;

    end;

    scheme :: BINTREE1:sch4

    BinDTConstrUniqDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr , D() -> non empty set , f1,f2() -> Function of ( TS G()), D() , TermVal( set) -> Element of D() , NTermVal( set, set, set, set, set) -> Element of D() } :

f1() = f2()

      provided

       A1: (for t be Terminal of G() holds (f1() . ( root-tree t)) = TermVal(t)) & for nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of D() st xl = (f1() . tl) & xr = (f1() . tr) holds (f1() . (nt -tree (tl,tr))) = NTermVal(nt,rtl,rtr,xl,xr)

       and

       A2: (for t be Terminal of G() holds (f2() . ( root-tree t)) = TermVal(t)) & for nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of D() st xl = (f2() . tl) & xr = (f2() . tr) holds (f2() . (nt -tree (tl,tr))) = NTermVal(nt,rtl,rtr,xl,xr);

      deffunc BNTV( Symbol of G(), FinSequence, FinSequence of D()) = NTermVal($1,.,.,.,.);

       A3:

      now

        thus for t be Symbol of G() st t in ( Terminals G()) holds (f2() . ( root-tree t)) = TermVal(t) by A2;

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

        set rts = ( roots ts);

        set x = (f2() * ts);

        assume

         A4: nt ==> rts;

        then

        consider tl,tr be Element of ( TS G()) such that

         A5: ( roots ts) = <*( root-label tl), ( root-label tr)*> and

         A6: tl = (ts . 1) and

         A7: tr = (ts . 2) and

         A8: (nt -tree ts) = (nt -tree (tl,tr)) and tl in ( rng ts) and tr in ( rng ts) by Th10;

        

         A9: nt is NonTerminal of G() by A4, Th10;

        reconsider xr = (f2() . tr) as Element of D();

        2 in ( dom ts) by A4, Th10;

        then

         A10: (x . 2) = xr by A7, FUNCT_1: 13;

        reconsider xl = (f2() . tl) as Element of D();

        1 in ( dom ts) by A4, Th10;

        then

         A11: (x . 1) = xl by A6, FUNCT_1: 13;

        ( root-label tl) = (rts . 1) & ( root-label tr) = (rts . 2) by A5, FINSEQ_1: 44;

        hence (f2() . (nt -tree ts)) = BNTV(nt,rts,x) by A2, A4, A5, A8, A9, A11, A10;

      end;

       A12:

      now

        thus for t be Symbol of G() st t in ( Terminals G()) holds (f1() . ( root-tree t)) = TermVal(t) by A1;

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

        set rts = ( roots ts);

        set x = (f1() * ts);

        assume

         A13: nt ==> rts;

        then

        consider tl,tr be Element of ( TS G()) such that

         A14: ( roots ts) = <*( root-label tl), ( root-label tr)*> and

         A15: tl = (ts . 1) and

         A16: tr = (ts . 2) and

         A17: (nt -tree ts) = (nt -tree (tl,tr)) and tl in ( rng ts) and tr in ( rng ts) by Th10;

        

         A18: nt is NonTerminal of G() by A13, Th10;

        reconsider xr = (f1() . tr) as Element of D();

        2 in ( dom ts) by A13, Th10;

        then

         A19: (x . 2) = xr by A16, FUNCT_1: 13;

        reconsider xl = (f1() . tl) as Element of D();

        1 in ( dom ts) by A13, Th10;

        then

         A20: (x . 1) = xl by A15, FUNCT_1: 13;

        ( root-label tl) = (rts . 1) & ( root-label tr) = (rts . 2) by A14, FINSEQ_1: 44;

        hence (f1() . (nt -tree ts)) = BNTV(nt,rts,x) by A1, A13, A14, A17, A18, A20, A19;

      end;

      thus thesis from DTCONSTR:sch 9( A12, A3);

    end;

    scheme :: BINTREE1:sch5

    BinDTCDefLambda { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr , A,B() -> non empty set , F( set, set) -> Element of B() , H( set, set, set, set) -> Element of B() } :

ex f be Function of ( TS G()), ( Funcs (A(),B())) st (for t be Terminal of G() holds ex g be Function of A(), B() st g = (f . ( root-tree t)) & for a be Element of A() holds (g . a) = F(t,a)) & for nt be NonTerminal of G(), t1,t2 be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be Function of A(), B() st g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) & for a be Element of A() holds (g . a) = H(nt,f1,f2,a);

      defpred P[ set, set, set, set] means for a be Element of A() holds for ntv be Function of A(), B() st ntv = $4 holds (ntv . a) = H($1,$2,$3,a);

      defpred P[ set, set] means for tv be Function of A(), B() st tv = $2 holds for a be Element of A() holds (tv . a) = F($1,a);

      reconsider FAB = ( Funcs (A(),B())) as non empty set;

       A1:

      now

        let x be Element of ( Terminals G());

        deffunc F( set) = F(x,$1);

        consider y be Function of A(), B() such that

         A2: for a be Element of A() holds (y . a) = F(a) from FUNCT_2:sch 4;

        A() = ( dom y) & ( rng y) c= B() by FUNCT_2:def 1;

        then

        reconsider y as Element of FAB by FUNCT_2:def 2;

        take y;

        thus P[x, y] by A2;

      end;

      consider TV be Function of ( Terminals G()), FAB such that

       A3: for e be Element of ( Terminals G()) holds P[e, (TV . e)] from FUNCT_2:sch 3( A1);

      deffunc TermVal( Terminal of G()) = (TV . $1);

       A4:

      now

        let x be Element of ( NonTerminals G()), y,z be Element of FAB;

        deffunc F( set) = H(x,y,z,$1);

        consider fab be Function of A(), B() such that

         A5: for a be Element of A() holds (fab . a) = F(a) from FUNCT_2:sch 4;

        A() = ( dom fab) & ( rng fab) c= B() by FUNCT_2:def 1;

        then

        reconsider fab as Element of FAB by FUNCT_2:def 2;

        take fab;

        thus P[x, y, z, fab] by A5;

      end;

      consider NTV be Function of [:( NonTerminals G()), FAB, FAB:], FAB such that

       A6: for x be Element of ( NonTerminals G()), y,z be Element of FAB holds P[x, y, z, (NTV . [x, y, z])] from MULTOP_1:sch 1( A4);

      deffunc NTermVal( Element of ( NonTerminals G()), set, set, Element of FAB, Element of FAB) = (NTV . [$1, $4, $5]);

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

       A7: (for t be Terminal of G() holds (f . ( root-tree t)) = TermVal(t)) & for nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of FAB st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = NTermVal(nt,rtl,rtr,xl,xr) from BinDTConstrIndDef;

      reconsider f9 = f as Function of ( TS G()), ( Funcs (A(),B()));

      take f9;

      hereby

        let t be Terminal of G();

        consider TVt be Function such that

         A8: (TV . t) = TVt and

         A9: ( dom TVt) = A() & ( rng TVt) c= B() by FUNCT_2:def 2;

        reconsider TVt as Function of A(), B() by A9, FUNCT_2:def 1, RELSET_1: 4;

        take TVt;

        thus TVt = (f9 . ( root-tree t)) by A7, A8;

        let a be Element of A();

        thus (TVt . a) = F(t,a) by A3, A8;

      end;

      let nt be NonTerminal of G(), t1,t2 be Element of ( TS G()), rtl,rtr be Symbol of G();

      assume

       A10: rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*>;

      ex f2 be Function st (f . t2) = f2 & ( dom f2) = A() & ( rng f2) c= B() by FUNCT_2:def 2;

      then

      reconsider f2 = (f . t2) as Function of A(), B() by FUNCT_2:def 1, RELSET_1: 4;

      ex f1 be Function st (f . t1) = f1 & ( dom f1) = A() & ( rng f1) c= B() by FUNCT_2:def 2;

      then

      reconsider f1 = (f . t1) as Function of A(), B() by FUNCT_2:def 1, RELSET_1: 4;

      (NTV . [nt, (f . t1), (f . t2)]) in FAB;

      then

      consider ntvval be Function such that

       A11: ntvval = (NTV . [nt, f1, f2]) and

       A12: ( dom ntvval) = A() & ( rng ntvval) c= B() by FUNCT_2:def 2;

      reconsider ntvval as Function of A(), B() by A12, FUNCT_2:def 1, RELSET_1: 4;

      take ntvval, f1, f2;

      thus ntvval = (f9 . (nt -tree (t1,t2))) & f1 = (f9 . t1) & f2 = (f9 . t2) by A7, A10, A11;

      thus thesis by A6, A11;

    end;

    scheme :: BINTREE1:sch6

    BinDTCDefLambdaUniq { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr , A,B() -> non empty set , f1,f2() -> Function of ( TS G()), ( Funcs (A(),B())) , F( set, set) -> Element of B() , H( set, set, set, set) -> Element of B() } :

f1() = f2()

      provided

       A1: (for t be Terminal of G() holds ex g be Function of A(), B() st g = (f1() . ( root-tree t)) & for a be Element of A() holds (g . a) = F(t,a)) & for nt be NonTerminal of G(), t1,t2 be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be Function of A(), B() st g = (f1() . (nt -tree (t1,t2))) & f1 = (f1() . t1) & f2 = (f1() . t2) & for a be Element of A() holds (g . a) = H(nt,f1,f2,a)

       and

       A2: (for t be Terminal of G() holds ex g be Function of A(), B() st g = (f2() . ( root-tree t)) & for a be Element of A() holds (g . a) = F(t,a)) & for nt be NonTerminal of G(), t1,t2 be Element of ( TS G()), rtl,rtr be Symbol of G() st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be Function of A(), B() st g = (f2() . (nt -tree (t1,t2))) & f1 = (f2() . t1) & f2 = (f2() . t2) & for a be Element of A() holds (g . a) = H(nt,f1,f2,a);

      defpred P[ set, set, set, set] means for a be Element of A() holds for ntv be Function of A(), B() st ntv = $4 holds (ntv . a) = H($1,$2,$3,a);

      defpred P[ set, set] means for tv be Function of A(), B() st tv = $2 holds for a be Element of A() holds (tv . a) = F($1,a);

      reconsider FAB = ( Funcs (A(),B())) as non empty set;

      reconsider f29 = f2() as Function of ( TS G()), FAB;

       A3:

      now

        let x be Element of ( Terminals G());

        deffunc F( Element of A()) = F(x,$1);

        consider y be Function of A(), B() such that

         A4: for a be Element of A() holds (y . a) = F(a) from FUNCT_2:sch 4;

        A() = ( dom y) & ( rng y) c= B() by FUNCT_2:def 1;

        then

        reconsider y as Element of FAB by FUNCT_2:def 2;

        take y;

        thus P[x, y] by A4;

      end;

      consider TV be Function of ( Terminals G()), FAB such that

       A5: for e be Element of ( Terminals G()) holds P[e, (TV . e)] from FUNCT_2:sch 3( A3);

      deffunc TermVal( Terminal of G()) = (TV . $1);

       A6:

      now

        let x be Element of ( NonTerminals G()), y,z be Element of FAB;

        deffunc F( Element of A()) = H(x,y,z,$1);

        consider fab be Function of A(), B() such that

         A7: for a be Element of A() holds (fab . a) = F(a) from FUNCT_2:sch 4;

        A() = ( dom fab) & ( rng fab) c= B() by FUNCT_2:def 1;

        then

        reconsider fab as Element of FAB by FUNCT_2:def 2;

        take fab;

        thus P[x, y, z, fab] by A7;

      end;

      consider NTV be Function of [:( NonTerminals G()), FAB, FAB:], FAB such that

       A8: for x be Element of ( NonTerminals G()), y be Element of FAB, z be Element of FAB holds P[x, y, z, (NTV . [x, y, z])] from MULTOP_1:sch 1( A6);

      deffunc NTV( NonTerminal of G(), set, set, Element of FAB, Element of FAB) = (NTV . [$1, $4, $5]);

       A9:

      now

        hereby

          let t be Terminal of G();

          consider TVt be Function such that

           A10: (TV . t) = TVt and

           A11: ( dom TVt) = A() and

           A12: ( rng TVt) c= B() by FUNCT_2:def 2;

          reconsider TVt as Function of A(), B() by A11, A12, FUNCT_2:def 1, RELSET_1: 4;

          consider g be Function of A(), B() such that

           A13: g = (f2() . ( root-tree t)) and

           A14: for a be Element of A() holds (g . a) = F(t,a) by A2;

          now

            thus A() = ( dom g) by FUNCT_2:def 1;

            thus A() = ( dom TVt) by A11;

            let x be object;

            assume x in A();

            then

            reconsider xx = x as Element of A();

            (g . xx) = F(t,xx) by A14

            .= (TVt . xx) by A5, A10;

            hence (g . x) = (TVt . x);

          end;

          hence (f29 . ( root-tree t)) = TermVal(t) by A13, A10, FUNCT_1: 2;

        end;

        let nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G();

        assume rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*>;

        then

        consider g,ff1,ff2 be Function of A(), B() such that

         A15: g = (f2() . (nt -tree (tl,tr))) and

         A16: ff1 = (f2() . tl) & ff2 = (f2() . tr) & for a be Element of A() holds (g . a) = H(nt,ff1,ff2,a) by A2;

        let xl,xr be Element of FAB;

        consider ntvnt be Function such that

         A17: ntvnt = (NTV . [nt, xl, xr]) and

         A18: ( dom ntvnt) = A() & ( rng ntvnt) c= B() by FUNCT_2:def 2;

        reconsider ntvnt as Function of A(), B() by A18, FUNCT_2:def 1, RELSET_1: 4;

        assume

         A19: xl = (f29 . tl) & xr = (f29 . tr);

        now

          thus A() = ( dom g) by FUNCT_2:def 1;

          thus A() = ( dom ntvnt) by FUNCT_2:def 1;

          let x be object;

          assume x in A();

          then

          reconsider xx = x as Element of A();

          (g . xx) = H(nt,xl,xr,xx) by A19, A16

          .= (ntvnt . xx) by A8, A17;

          hence (g . x) = (ntvnt . x);

        end;

        hence (f29 . (nt -tree (tl,tr))) = NTV(nt,rtl,rtr,xl,xr) by A15, A17, FUNCT_1: 2;

      end;

      reconsider f19 = f1() as Function of ( TS G()), FAB;

       A20:

      now

        hereby

          let t be Terminal of G();

          consider TVt be Function such that

           A21: (TV . t) = TVt and

           A22: ( dom TVt) = A() and

           A23: ( rng TVt) c= B() by FUNCT_2:def 2;

          reconsider TVt as Function of A(), B() by A22, A23, FUNCT_2:def 1, RELSET_1: 4;

          consider g be Function of A(), B() such that

           A24: g = (f1() . ( root-tree t)) and

           A25: for a be Element of A() holds (g . a) = F(t,a) by A1;

          now

            thus A() = ( dom g) by FUNCT_2:def 1;

            thus A() = ( dom TVt) by A22;

            let x be object;

            assume x in A();

            then

            reconsider xx = x as Element of A();

            (g . xx) = F(t,xx) by A25

            .= (TVt . xx) by A5, A21;

            hence (g . x) = (TVt . x);

          end;

          hence (f19 . ( root-tree t)) = TermVal(t) by A24, A21, FUNCT_1: 2;

        end;

        let nt be NonTerminal of G(), tl,tr be Element of ( TS G()), rtl,rtr be Symbol of G();

        assume rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*>;

        then

        consider g,ff1,ff2 be Function of A(), B() such that

         A26: g = (f1() . (nt -tree (tl,tr))) and

         A27: ff1 = (f1() . tl) & ff2 = (f1() . tr) & for a be Element of A() holds (g . a) = H(nt,ff1,ff2,a) by A1;

        let xl,xr be Element of FAB;

        consider ntvnt be Function such that

         A28: ntvnt = (NTV . [nt, xl, xr]) and

         A29: ( dom ntvnt) = A() & ( rng ntvnt) c= B() by FUNCT_2:def 2;

        reconsider ntvnt as Function of A(), B() by A29, FUNCT_2:def 1, RELSET_1: 4;

        assume

         A30: xl = (f19 . tl) & xr = (f19 . tr);

        now

          thus A() = ( dom g) by FUNCT_2:def 1;

          thus A() = ( dom ntvnt) by FUNCT_2:def 1;

          let x be object;

          assume x in A();

          then

          reconsider xx = x as Element of A();

          (g . xx) = H(nt,xl,xr,xx) by A30, A27

          .= (ntvnt . xx) by A8, A28;

          hence (g . x) = (ntvnt . x);

        end;

        hence (f19 . (nt -tree (tl,tr))) = NTV(nt,rtl,rtr,xl,xr) by A26, A28, FUNCT_1: 2;

      end;

      f19 = f29 from BinDTConstrUniqDef( A20, A9);

      hence thesis;

    end;

    registration

      let G be binary with_terminals with_nonterminals non empty DTConstrStr;

      cluster -> binary for Element of ( TS G);

      coherence

      proof

        defpred P[ DecoratedTree] means $1 is binary;

         A1:

        now

          let s be Terminal of G;

          ( dom ( root-tree s)) is binary by TREES_4: 3;

          hence P[( root-tree s)] by Def3;

        end;

        

         A2: for nt be NonTerminal of G, tl,tr be Element of ( TS G) st nt ==> <*( root-label tl), ( root-label tr)*> & P[tl] & P[tr] holds P[(nt -tree (tl,tr))] by Th9;

        thus for x be Element of ( TS G) holds P[x] from BinDTConstrInd( A1, A2);

      end;

    end