trees_4.miz



    begin

    definition

      let T be DecoratedTree;

      mode Node of T is Element of ( dom T);

    end

    reserve x,y,z for object,

i,j,n for Nat,

p,q,r for FinSequence,

v for FinSequence of NAT ;

     Lm1:

    now

      let x be set, y;

      let p be FinSequence of x;

      assume y in ( dom p) or 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 (p . y) in x by A1;

    end;

    definition

      let T1,T2 be DecoratedTree;

      :: original: =

      redefine

      :: TREES_4:def1

      pred T1 = T2 means ( dom T1) = ( dom T2) & for p be Node of T1 holds (T1 . p) = (T2 . p);

      compatibility

      proof

        (for p be Node of T1 holds (T1 . p) = (T2 . p)) & ( dom T1) = ( dom T2) implies for x be object st x in ( dom T1) holds (T1 . x) = (T2 . x);

        hence thesis by FUNCT_1: 2;

      end;

    end

    theorem :: TREES_4:1

    

     Th1: for i,j be Nat st ( elementary_tree i) c= ( elementary_tree j) holds i <= j

    proof

      let i,j be Nat;

      assume that

       A1: ( elementary_tree i) c= ( elementary_tree j) and

       A2: i > j;

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

       <*j*> in ( elementary_tree i) by A2, TREES_1: 28;

      then

       A3: ex n be Nat st n < j & <*j*> = <*n*> by A1, TREES_1: 30;

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

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: TREES_4:2

    

     Th2: for i,j be Nat st ( elementary_tree i) = ( elementary_tree j) holds i = j

    proof

      let i,j be Nat;

      assume ( elementary_tree i) = ( elementary_tree j);

      then i <= j & i >= j by Th1;

      hence thesis by XXREAL_0: 1;

    end;

    

     Lm2: n < ( len p) implies (n + 1) in ( dom p) & (p . (n + 1)) in ( rng p)

    proof

      assume

       A1: n < ( len p);

      n >= 0 by NAT_1: 2;

      then

       A2: (n + 1) >= ( 0 + 1) by XREAL_1: 7;

      (n + 1) <= ( len p) by A1, NAT_1: 13;

      then (n + 1) in ( dom p) by A2, FINSEQ_3: 25;

      hence thesis by FUNCT_1:def 3;

    end;

     Lm3:

    now

      let n;

      let x be set;

      let p be FinSequence of x;

      assume n < ( len p);

      then

       A1: (p . (n + 1)) in ( rng p) by Lm2;

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

      hence (p . (n + 1)) in x by A1;

    end;

    definition

      let x be object;

      :: TREES_4:def2

      func root-tree x -> DecoratedTree equals (( elementary_tree 0 ) --> x);

      correctness ;

    end

    definition

      let D be non empty set, d be Element of D;

      :: original: root-tree

      redefine

      func root-tree d -> Element of ( FinTrees D) ;

      coherence

      proof

        ( dom (( elementary_tree 0 ) --> d)) = ( elementary_tree 0 );

        hence thesis by TREES_3:def 8;

      end;

    end

    theorem :: TREES_4:3

    

     Th3: ( dom ( root-tree x)) = ( elementary_tree 0 ) & (( root-tree x) . {} ) = x

    proof

       {} in ( elementary_tree 0 ) by TARSKI:def 1, TREES_1: 29;

      hence thesis by FUNCOP_1: 7;

    end;

    theorem :: TREES_4:4

    ( root-tree x) = ( root-tree y) implies x = y

    proof

      (( root-tree x) . {} ) = x by Th3;

      hence thesis by Th3;

    end;

    theorem :: TREES_4:5

    

     Th5: for T be DecoratedTree st ( dom T) = ( elementary_tree 0 ) holds T = ( root-tree (T . {} )) by TARSKI:def 1, TREES_1: 29;

    theorem :: TREES_4:6

    ( root-tree x) = { [ {} , x]}

    proof

      

      thus ( root-tree x) = [: { {} }, {x}:] by FUNCOP_1:def 2, TREES_1: 29

      .= { [ {} , x]} by ZFMISC_1: 29;

    end;

    definition

      let x;

      let p be FinSequence;

      :: TREES_4:def3

      func x -flat_tree (p) -> DecoratedTree means

      : Def3: ( dom it ) = ( elementary_tree ( len p)) & (it . {} ) = x & for n st n < ( len p) holds (it . <*n*>) = (p . (n + 1));

      existence

      proof

        defpred X[ object, object] means $1 = {} & $2 = x or ex n st $1 = <*n*> & $2 = (p . (n + 1));

        

         A1: for z be object st z in ( elementary_tree ( len p)) holds ex y be object st X[z, y]

        proof

          let z be object;

          assume z in ( elementary_tree ( len p));

          then

          reconsider z as Element of ( elementary_tree ( len p));

          reconsider z as FinSequence of NAT ;

          

           A2: z = {} or ex n st n < ( len p) & z = <*n*> by TREES_1: 30;

          now

            given n such that

             A3: z = <*n*> and n < ( len p);

            take y = (p . (n + 1)), n;

            thus z = <*n*> & y = (p . (n + 1)) by A3;

          end;

          hence thesis by A2;

        end;

        consider f be Function such that

         A4: ( dom f) = ( elementary_tree ( len p)) & for y be object st y in ( elementary_tree ( len p)) holds X[y, (f . y)] from CLASSES1:sch 1( A1);

        reconsider f as DecoratedTree by A4, TREES_2:def 8;

        take f;

        thus ( dom f) = ( elementary_tree ( len p)) by A4;

         {} in ( dom f) & for n st {} = <*n*> holds (f . {} ) <> (p . (n + 1)) by TREES_1: 22;

        hence (f . {} ) = x by A4;

        let n;

        assume n < ( len p);

        then <*n*> in ( dom f) by A4, TREES_1: 28;

        then

        consider k be Nat such that

         A5: <*n*> = <*k*> and

         A6: (f . <*n*>) = (p . (k + 1)) by A4;

        k = ( <*n*> . 1) by A5, FINSEQ_1: 40

        .= n by FINSEQ_1: 40;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let T1,T2 be DecoratedTree such that

         A7: ( dom T1) = ( elementary_tree ( len p)) and

         A8: (T1 . {} ) = x and

         A9: for n st n < ( len p) holds (T1 . <*n*>) = (p . (n + 1)) and

         A10: ( dom T2) = ( elementary_tree ( len p)) and

         A11: (T2 . {} ) = x and

         A12: for n st n < ( len p) holds (T2 . <*n*>) = (p . (n + 1));

        now

          let x be object;

          assume x in ( elementary_tree ( len p));

          then

          reconsider x9 = x as Element of ( elementary_tree ( len p));

          

           A13: x9 = {} or ex n st n < ( len p) & x9 = <*n*> by TREES_1: 30;

          now

            given n such that

             A14: n < ( len p) & x = <*n*>;

            

            thus (T1 . x) = (p . (n + 1)) by A9, A14

            .= (T2 . x) by A12, A14;

          end;

          hence (T1 . x) = (T2 . x) by A8, A11, A13;

        end;

        hence thesis by A7, A10;

      end;

    end

    theorem :: TREES_4:7

    (x -flat_tree p) = (y -flat_tree q) implies x = y & p = q

    proof

      assume

       A1: (x -flat_tree p) = (y -flat_tree q);

      ((x -flat_tree p) . {} ) = x by Def3;

      hence x = y by A1, Def3;

      

       A2: ( dom (x -flat_tree p)) = ( elementary_tree ( len p)) & ( dom (y -flat_tree q)) = ( elementary_tree ( len q)) by Def3;

      then

       A3: ( len p) = ( len q) by A1, Th2;

      now

        let i be Nat;

        assume that

         A4: i >= 1 and

         A5: i <= ( len p);

        consider n be Nat such that

         A6: i = (1 + n) by A4, NAT_1: 10;

        

         A7: n in NAT & n < ( len p) by A5, A6, NAT_1: 13, ORDINAL1:def 12;

        then (p . i) = ((x -flat_tree p) . <*n*>) by A6, Def3;

        hence (p . i) = (q . i) by A1, A3, A6, A7, Def3;

      end;

      hence thesis by A1, A2, Th2;

    end;

    theorem :: TREES_4:8

    

     Th8: for j be Element of NAT st j < i holds (( elementary_tree i) | <*j*>) = ( elementary_tree 0 )

    proof

      let j be Element of NAT ;

      set p = (i |-> ( elementary_tree 0 )), T = ( tree p);

      assume

       A1: j < i;

      then

       A2: (1 + j) >= 1 & (j + 1) <= i by NAT_1: 11, NAT_1: 13;

      ( len p) = i by CARD_1:def 7;

      then

       A3: ( elementary_tree i) = T & (T | <*j*>) = (p . (j + 1)) by A1, TREES_3: 49, TREES_3: 54;

      (j + 1) in ( Seg i) by A2;

      hence thesis by A3, FUNCOP_1: 7;

    end;

    theorem :: TREES_4:9

    

     Th9: for i be Element of NAT st i < ( len p) holds ((x -flat_tree p) | <*i*>) = ( root-tree (p . (i + 1)))

    proof

      let i be Element of NAT ;

      reconsider t = {} as Element of (( dom (x -flat_tree p)) | <*i*>) by TREES_1: 22;

      assume

       A1: i < ( len p);

      then

       A2: ((x -flat_tree p) . <*i*>) = (p . (i + 1)) by Def3;

      

       A3: ( dom (x -flat_tree p)) = ( elementary_tree ( len p)) by Def3;

      (( elementary_tree ( len p)) | <*i*>) = ( elementary_tree 0 ) by A1, Th8;

      then

       A4: ( dom ((x -flat_tree p) | <*i*>)) = ( elementary_tree 0 ) by A3, TREES_2:def 10;

      ( <*i*> ^ t) = <*i*> & (((x -flat_tree p) | <*i*>) . t) = ((x -flat_tree p) . ( <*i*> ^ t)) by FINSEQ_1: 34, TREES_2:def 10;

      hence thesis by A2, A4, Th5;

    end;

    definition

      let x be object, p;

      :: TREES_4:def4

      func x -tree (p) -> DecoratedTree means

      : Def4: (ex q be DTree-yielding FinSequence st p = q & ( dom it ) = ( tree ( doms q))) & (it . {} ) = x & for n be Nat st n < ( len p) holds (it | <*n*>) = (p . (n + 1));

      existence

      proof

        reconsider pp = p as Function-yielding FinSequence by A1;

        

         A2: ( dom ( doms pp)) = ( dom p) by A1, TREES_3: 37;

        reconsider q = ( doms pp) as Tree-yielding FinSequence by A1;

        defpred X[ object, object] means $1 = {} & $2 = x or $1 <> {} & ex n, r st $1 = ( <*n*> ^ r) & $2 = (p .. ((n + 1),r));

        

         A3: for y be object st y in ( tree q) holds ex z be object st X[y, z]

        proof

          let y be object;

          assume y in ( tree q);

          then

          reconsider s = y as Element of ( tree q);

          now

            assume y <> {} ;

            then

            consider w be FinSequence of NAT , n be Element of NAT such that

             A4: s = ( <*n*> ^ w) by FINSEQ_2: 130;

            reconsider w as FinSequence;

            take z = (p .. ((n + 1),w));

            thus y = {} & z = x or y <> {} & ex n, r st y = ( <*n*> ^ r) & z = (p .. ((n + 1),r)) by A4;

          end;

          hence thesis;

        end;

        consider T be Function such that

         A5: ( dom T) = ( tree q) & for y be object st y in ( tree q) holds X[y, (T . y)] from CLASSES1:sch 1( A3);

        reconsider T as DecoratedTree by A5, TREES_2:def 8;

        take T;

        thus ex q be DTree-yielding FinSequence st p = q & ( dom T) = ( tree ( doms q)) by A1, A5;

         {} in ( tree q) by TREES_1: 22;

        hence (T . {} ) = x by A5;

        

         A6: ( len p) = ( len q) by A2, FINSEQ_3: 29;

        let n be Nat;

        assume

         A7: n < ( len p);

        then

         A8: (n + 1) in ( dom p) by Lm2;

        then

        reconsider t = (p . (n + 1)) as DecoratedTree by A1, TREES_3: 24;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        

         A9: ( dom t) = (q . (n + 1)) by A8, FUNCT_6: 22;

        

         A10: ( dom t) = (q . (n + 1)) by A8, FUNCT_6: 22

        .= (( dom T) | <*nn*>) by A5, A6, A7, TREES_3: 49;

        

         A11: (( dom T) | <*n*>) = ( dom (T | <*n*>)) by TREES_2:def 10;

        now

          let r be FinSequence of NAT ;

          assume

           A12: r in ( dom t);

          then ( <*n*> ^ r) in ( dom T) by A5, A6, A7, A9, TREES_3:def 15;

          then

          consider m be Nat, s be FinSequence such that

           A13: ( <*n*> ^ r) = ( <*m*> ^ s) and

           A14: (T . ( <*n*> ^ r)) = (p .. ((m + 1),s)) by A5;

          

           A15: (( <*n*> ^ r) . 1) = n & (( <*m*> ^ s) . 1) = m by FINSEQ_1: 41;

          then (m + 1) in ( dom p) & r = s by A7, A13, Lm2, FINSEQ_1: 33;

          then (p .. ((m + 1),s)) = (t . r) by A12, A13, A15, FUNCT_5: 38;

          hence ((T | <*n*>) . r) = (t . r) by A10, A12, A14, TREES_2:def 10;

        end;

        hence thesis by A10, A11, TREES_2: 31;

      end;

      uniqueness

      proof

        let T1,T2 be DecoratedTree;

        given q1 be DTree-yielding FinSequence such that

         A16: p = q1 and

         A17: ( dom T1) = ( tree ( doms q1));

        assume that

         A18: (T1 . {} ) = x and

         A19: for n be Nat st n < ( len p) holds (T1 | <*n*>) = (p . (n + 1));

        given q2 be DTree-yielding FinSequence such that

         A20: p = q2 & ( dom T2) = ( tree ( doms q2));

        assume that

         A21: (T2 . {} ) = x and

         A22: for n be Nat st n < ( len p) holds (T2 | <*n*>) = (p . (n + 1));

        now

          let q be FinSequence of NAT ;

          assume

           A23: q in ( dom T1);

          now

            assume q <> {} ;

            then

            consider s be FinSequence of NAT , n be Element of NAT such that

             A24: q = ( <*n*> ^ s) by FINSEQ_2: 130;

            

             A25: <*n*> in ( dom T1) by A23, A24, TREES_1: 21;

            

             A26: n < ( len ( doms q1)) by A17, A23, A24, TREES_3: 48;

            ( len ( doms q1)) = ( len p) by A16, TREES_3: 38;

            then

             A27: (T1 | <*n*>) = (p . (n + 1)) & (T2 | <*n*>) = (p . (n + 1)) by A19, A22, A26;

            

             A28: s in (( dom T1) | <*n*>) by A23, A24, A25, TREES_1:def 6;

            then (T1 . q) = ((T1 | <*n*>) . s) by A24, TREES_2:def 10;

            hence (T1 . q) = (T2 . q) by A16, A17, A20, A24, A27, A28, TREES_2:def 10;

          end;

          hence (T1 . q) = (T2 . q) by A18, A21;

        end;

        hence thesis by A16, A17, A20;

      end;

    end

    definition

      let x be object;

      let T be DecoratedTree;

      :: TREES_4:def5

      func x -tree T -> DecoratedTree equals (x -tree <*T*>);

      correctness ;

    end

    definition

      let x be object;

      let T1,T2 be DecoratedTree;

      :: TREES_4:def6

      func x -tree (T1,T2) -> DecoratedTree equals (x -tree <*T1, T2*>);

      correctness ;

    end

    theorem :: TREES_4:10

    

     Th10: for p be DTree-yielding FinSequence holds ( dom (x -tree p)) = ( tree ( doms p))

    proof

      let p be DTree-yielding FinSequence;

      ex q be DTree-yielding FinSequence st p = q & ( dom (x -tree p)) = ( tree ( doms q)) by Def4;

      hence thesis;

    end;

    theorem :: TREES_4:11

    

     Th11: for p be DTree-yielding FinSequence holds y in ( dom (x -tree p)) iff y = {} or ex i be Nat, T be DecoratedTree, q be Node of T st i < ( len p) & T = (p . (i + 1)) & y = ( <*i*> ^ q)

    proof

      let p be DTree-yielding FinSequence;

      

       A1: ( dom (x -tree p)) = ( tree ( doms p)) by Th10;

       A2:

      now

        given i, q such that

         A3: i < ( len ( doms p)) and

         A4: q in (( doms p) . (i + 1)) and

         A5: y = ( <*i*> ^ q);

        ( len ( doms p)) = ( len p) by TREES_3: 38;

        then

         A6: (i + 1) in ( dom p) by A3, Lm2;

        then

        reconsider T = (p . (i + 1)) as DecoratedTree by TREES_3: 24;

        take i, T;

        reconsider q as Node of T by A4, A6, FUNCT_6: 22;

        take q;

        thus i < ( len p) & T = (p . (i + 1)) & y = ( <*i*> ^ q) by A3, A5, TREES_3: 38;

      end;

      now

        given i be Nat, T be DecoratedTree, q be Node of T such that

         A7: i < ( len p) and

         A8: T = (p . (i + 1)) and

         A9: y = ( <*i*> ^ q);

        reconsider q as FinSequence;

        take i, q;

        (i + 1) in ( dom p) by A7, Lm2;

        then (( doms p) . (i + 1)) = ( dom T) by A8, FUNCT_6: 22;

        hence i < ( len ( doms p)) & q in (( doms p) . (i + 1)) & y = ( <*i*> ^ q) by A7, A9, TREES_3: 38;

      end;

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

    end;

    theorem :: TREES_4:12

    

     Th12: for p be DTree-yielding FinSequence holds for i be Nat, T be DecoratedTree, q be Node of T st i < ( len p) & T = (p . (i + 1)) holds ((x -tree p) . ( <*i*> ^ q)) = (T . q)

    proof

      let p be DTree-yielding FinSequence, n be Nat, T be DecoratedTree;

      let q be Node of T;

      assume

       A1: n < ( len p) & T = (p . (n + 1));

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

      

       A2: ( <*n*> ^ q) in ( dom (x -tree p)) by Th11, A1;

      then <*n*> in ( dom (x -tree p)) by TREES_1: 21;

      then q in (( dom (x -tree p)) | <*n*>) by A2, TREES_1:def 6;

      then (((x -tree p) | <*n*>) . q) = ((x -tree p) . ( <*n*> ^ q)) by TREES_2:def 10;

      hence thesis by A1, Def4;

    end;

    theorem :: TREES_4:13

    for T be DecoratedTree holds ( dom (x -tree T)) = ( ^ ( dom T))

    proof

      let T be DecoratedTree;

      ( dom (x -tree <*T*>)) = ( tree ( doms <*T*>)) & ( doms <*T*>) = <*( dom T)*> by Th10, FINSEQ_3: 132;

      hence thesis by TREES_3:def 16;

    end;

    theorem :: TREES_4:14

    for T1,T2 be DecoratedTree holds ( dom (x -tree (T1,T2))) = ( tree (( dom T1),( dom T2)))

    proof

      let T1,T2 be DecoratedTree;

      ( dom (x -tree <*T1, T2*>)) = ( tree ( doms <*T1, T2*>)) & ( doms <*T1, T2*>) = <*( dom T1), ( dom T2)*> by Th10, FINSEQ_3: 133;

      hence thesis by TREES_3:def 17;

    end;

    theorem :: TREES_4:15

    for p,q be DTree-yielding FinSequence st (x -tree p) = (y -tree q) holds x = y & p = q

    proof

      let p,q be DTree-yielding FinSequence;

      assume

       A1: (x -tree p) = (y -tree q);

      ((x -tree p) . {} ) = x by Def4;

      hence x = y by A1, Def4;

      ( dom (x -tree p)) = ( tree ( doms p)) & ( dom (y -tree q)) = ( tree ( doms q)) by Th10;

      then

       A2: ( doms p) = ( doms q) by A1, TREES_3: 50;

      ( dom p) = ( dom ( doms p)) & ( dom ( doms q)) = ( dom q) by TREES_3: 37;

      then

       A3: ( len p) = ( len q) by A2, FINSEQ_3: 29;

      now

        let i be Nat;

        assume that

         A4: i >= 1 and

         A5: i <= ( len p);

        consider n be Nat such that

         A6: i = (1 + n) by A4, NAT_1: 10;

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

        

         A7: n < ( len p) by A5, A6, NAT_1: 13;

        then (p . i) = ((x -tree p) | <*n*>) by A6, Def4;

        hence (p . i) = (q . i) by A1, A3, A6, A7, Def4;

      end;

      hence thesis by A3;

    end;

    theorem :: TREES_4:16

    ( root-tree x) = (y -flat_tree p) implies x = y & p = {}

    proof

      assume

       A1: ( root-tree x) = (y -flat_tree p);

      

      thus x = (( root-tree x) . {} ) by Th3

      .= y by A1, Def3;

      ( dom (y -flat_tree p)) = ( elementary_tree ( len p)) by Def3;

      hence thesis by A1, Th2;

    end;

    theorem :: TREES_4:17

    ( root-tree x) = (y -tree p) & p is DTree-yielding implies x = y & p = {}

    proof

      assume that

       A1: ( root-tree x) = (y -tree p) and

       A2: p is DTree-yielding;

      reconsider p9 = p as DTree-yielding FinSequence by A2;

      

      thus x = (( root-tree x) . {} ) by Th3

      .= y by A1, A2, Def4;

      ( dom (y -tree p)) = ( tree ( doms p9)) by Th10;

      then

       A3: ( doms p9) = {} by A1, TREES_3: 50, TREES_3: 52;

      ( dom ( doms p9)) = ( dom p) by TREES_3: 37;

      hence thesis by A3;

    end;

    theorem :: TREES_4:18

    (x -flat_tree p) = (y -tree q) & q is DTree-yielding implies x = y & ( len p) = ( len q) & for i st i in ( dom p) holds (q . i) = ( root-tree (p . i))

    proof

      assume that

       A1: (x -flat_tree p) = (y -tree q) and

       A2: q is DTree-yielding;

      reconsider q9 = q as DTree-yielding FinSequence by A2;

      

      thus x = ((x -flat_tree p) . {} ) by Def3

      .= y by A1, A2, Def4;

      ( tree (( len p) |-> ( elementary_tree 0 ))) = ( elementary_tree ( len p)) by TREES_3: 54

      .= ( dom (x -flat_tree p)) by Def3

      .= ( tree ( doms q9)) by A1, Th10;

      then

       A3: (( len p) |-> ( elementary_tree 0 )) = ( doms q9) by TREES_3: 50;

      ( len ( doms q9)) = ( len q) by TREES_3: 38;

      hence

       A4: ( len p) = ( len q) by A3, CARD_1:def 7;

      let i;

      assume

       A5: i in ( dom p);

      then

       A6: i >= 1 by FINSEQ_3: 25;

      

       A7: i <= ( len p) by A5, FINSEQ_3: 25;

      consider n be Nat such that

       A8: i = (1 + n) by A6, NAT_1: 10;

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

      

       A9: n < ( len p) by A7, A8, NAT_1: 13;

      then ((x -flat_tree p) | <*n*>) = ( root-tree (p . i)) by A8, Th9;

      hence thesis by A1, A2, A4, A8, A9, Def4;

    end;

    theorem :: TREES_4:19

    for p be DTree-yielding FinSequence, n be Nat, q be FinSequence st ( <*n*> ^ q) in ( dom (x -tree p)) holds ((x -tree p) . ( <*n*> ^ q)) = (p .. ((n + 1),q))

    proof

      let p be DTree-yielding FinSequence, n be Nat, q be FinSequence;

      assume

       A1: ( <*n*> ^ q) in ( dom (x -tree p));

      then ( <*n*> ^ q) is Node of (x -tree p);

      then

      reconsider q9 = q as FinSequence of NAT by FINSEQ_1: 36;

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

      

       A2: <*n*> in ( dom (x -tree p)) by A1, TREES_1: 21;

      

       A3: ( <*n*> ^ q) in ( tree ( doms p)) by A1, Th10;

      

       A4: ( len ( doms p)) = ( len p) by TREES_3: 38;

      

       A5: q9 in (( dom (x -tree p)) | <*n*>) by A1, A2, TREES_1:def 6;

      

       A6: n < ( len p) by A3, A4, TREES_3: 48;

      

       A7: ( dom ((x -tree p) | <*n*>)) = (( dom (x -tree p)) | <*n*>) & (((x -tree p) | <*n*>) . q9) = ((x -tree p) . ( <*n*> ^ q)) by A5, TREES_2:def 10;

      (n + 1) in ( dom p) & (p . (n + 1)) = ((x -tree p) | <*n*>) by A6, Def4, Lm2;

      hence thesis by A5, A7, FUNCT_5: 38;

    end;

    theorem :: TREES_4:20

    (x -flat_tree {} ) = ( root-tree x) & (x -tree {} ) = ( root-tree x)

    proof

      ( len {} ) = 0 ;

      then

       A1: ( dom (x -flat_tree {} )) = ( elementary_tree 0 ) by Def3;

      now

        let y be object;

        assume y in ( elementary_tree 0 );

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

        hence ((x -flat_tree {} ) . y) = x by Def3;

      end;

      hence (x -flat_tree {} ) = ( root-tree x) by A1;

      reconsider e = {} as DTree-yielding FinSequence;

      

       A2: ( dom (x -tree {} )) = ( tree ( doms e)) by Th10

      .= ( elementary_tree 0 ) by FUNCT_6: 23, TREES_3: 52;

      now

        let y be object;

        assume y in ( elementary_tree 0 );

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

        hence ((x -tree e) . y) = x by Def4;

      end;

      hence thesis by A2;

    end;

    theorem :: TREES_4:21

    (x -flat_tree <*y*>) = ((( elementary_tree 1) --> x) with-replacement ( <* 0 *>,( root-tree y)))

    proof

      set T = ((( elementary_tree 1) --> x) with-replacement ( <* 0 *>,( root-tree y)));

      

       A1: ( dom (x -flat_tree <*y*>)) = ( elementary_tree ( len <*y*>)) by Def3

      .= ( elementary_tree 1) by FINSEQ_1: 40;

      

       A2: ( dom ( root-tree y)) = ( elementary_tree 0 );

      

       A3: ( dom (( elementary_tree 1) --> x)) = ( elementary_tree 1) & <* 0 *> in ( elementary_tree 1) by TARSKI:def 2, TREES_1: 51;

      

      then

       A4: ( dom T) = (( elementary_tree 1) with-replacement ( <* 0 *>,( elementary_tree 0 ))) by A2, TREES_2:def 11

      .= ( elementary_tree 1) by TREES_3: 58, TREES_3: 67;

      now

        let z be object;

        assume z in ( elementary_tree 1);

        then

         A5: z = {} or z = <* 0 *> by TARSKI:def 2, TREES_1: 51;

        

         A6: {} in ( elementary_tree 1) by TARSKI:def 2, TREES_1: 51;

        

         A7: not <* 0 *> is_a_prefix_of {} ;

        

         A8: ( len <*y*>) = 1 by FINSEQ_1: 40;

        

         A9: ( <*y*> . 1) = y & ((x -flat_tree <*y*>) . {} ) = x by Def3, FINSEQ_1: 40;

        

         A10: (T . {} ) = ((( elementary_tree 1) --> x) . {} ) by A3, A6, A7, TREES_3: 45;

        

         A11: ((x -flat_tree <*y*>) . <* 0 *>) = ( <*y*> . ( 0 + 1)) by A8, Def3;

        (T . <* 0 *>) = (( root-tree y) . {} ) by A3, TREES_3: 44;

        hence (T . z) = ((x -flat_tree <*y*>) . z) by A5, A6, A9, A10, A11, Th3, FUNCOP_1: 7;

      end;

      hence thesis by A1, A4;

    end;

    theorem :: TREES_4:22

    for T be DecoratedTree holds (x -tree <*T*>) = ((( elementary_tree 1) --> x) with-replacement ( <* 0 *>,T))

    proof

      let T be DecoratedTree;

      set D = ((( elementary_tree 1) --> x) with-replacement ( <* 0 *>,T));

      set W = (( elementary_tree 1) with-replacement ( <* 0 *>,( dom T)));

      

       A1: ( dom (x -tree <*T*>)) = ( tree ( doms <*T*>)) by Th10

      .= ( tree <*( dom T)*>) by FINSEQ_3: 132

      .= ( ^ ( dom T)) by TREES_3:def 16

      .= W by TREES_3: 58;

      

       A2: ( dom (( elementary_tree 1) --> x)) = ( elementary_tree 1);

      reconsider t1 = {} , t2 = <* 0 *> as Element of ( elementary_tree 1) by TARSKI:def 2, TREES_1: 51;

      t2 = t2;

      then

       A3: ( dom D) = W by A2, TREES_2:def 11;

      

       A4: {} in ( dom T) by TREES_1: 22;

      now

        let y be object;

        assume y in W;

        then

        reconsider q = y as Element of W;

        q in ( elementary_tree 1) or ex v st v in ( dom T) & q = (t2 ^ v) by TREES_1:def 9;

        then

         A5: q = {} or q = t2 & t2 = (t2 ^ t1) or ex v st v in ( dom T) & q = ( <* 0 *> ^ v) by FINSEQ_1: 34, TARSKI:def 2, TREES_1: 51;

         not t2 is_a_prefix_of t1;

        

        then

         A6: (D . {} ) = ((( elementary_tree 1) --> x) . t1) by A2, TREES_3: 45

        .= x

        .= ((x -tree <*T*>) . {} ) by Def4;

        now

          given r be FinSequence of NAT such that

           A7: r in ( dom T) and

           A8: q = ( <* 0 *> ^ r);

          reconsider r as Node of T by A7;

          q = (t2 ^ r) by A8;

          then

           A9: (D . q) = (T . r) by A2, TREES_3: 46;

          ( len <*T*>) = 1 & ( <*T*> . ( 0 + 1)) = T by FINSEQ_1: 40;

          then

           A10: ((x -tree <*T*>) | t2) = T by Def4;

          (W | t2) = ( dom T) by TREES_1: 33;

          hence (D . q) = ((x -tree <*T*>) . q) by A1, A8, A9, A10, TREES_2:def 10;

        end;

        hence (D . y) = ((x -tree <*T*>) . y) by A4, A5, A6;

      end;

      hence thesis by A1, A3;

    end;

    registration

      let D be non empty set, d be Element of D, p be FinSequence of D;

      cluster (d -flat_tree p) -> D -valued;

      coherence

      proof

        set T = (d -flat_tree p);

        ( rng T) c= D

        proof

          let x be object;

          assume x in ( rng T);

          then

          consider y be object such that

           A1: y in ( dom T) and

           A2: x = (T . y) by FUNCT_1:def 3;

          reconsider y as Node of T by A1;

          

           A3: ( dom T) = ( elementary_tree ( len p)) by Def3;

          

           A4: (T . {} ) = d by Def3;

          now

            assume y <> {} ;

            then

            consider n such that

             A5: n < ( len p) & y = <*n*> by A3, TREES_1: 30;

            

             A6: (T . y) = (p . (n + 1)) & (p . (n + 1)) in ( rng p) by A5, Def3, Lm2;

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

            hence thesis by A2, A6;

          end;

          hence thesis by A2, A4;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

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

      let d be Element of D, p be FinSequence of F;

      cluster (d -tree p) -> D -valued;

      coherence

      proof

        set T = (d -tree p);

        ( rng T) c= D

        proof

          let x be object;

          assume x in ( rng T);

          then

          consider y be object such that

           A1: y in ( dom T) and

           A2: x = (T . y) by FUNCT_1:def 3;

          reconsider y as Node of T by A1;

          

           A3: (( tree ( doms p)) -level 1) = { <*n*> : n < ( len ( doms p)) } by TREES_3: 49;

          

           A4: (T . {} ) = d by Def4;

          

           A5: ( tree ( doms p)) = ( dom T) & ( len ( doms p)) = ( len p) by Th10, TREES_3: 38;

          now

            assume y <> {} ;

            then

            consider q be FinSequence of NAT , n be Element of NAT such that

             A6: y = ( <*n*> ^ q) by FINSEQ_2: 130;

            

             A7: <*n*> in ( dom T) by A6, TREES_1: 21;

            

             A8: ( len <*n*>) = 1 by FINSEQ_1: 40;

            

             A9: q in (( dom T) | <*n*>) by A6, A7, TREES_1:def 6;

            

             A10: <*n*> in (( dom T) -level 1) by A7, A8;

            

             A11: ( dom (T | <*n*>)) = (( dom T) | <*n*>) by TREES_2:def 10;

            consider i such that

             A12: <*n*> = <*i*> & i < ( len p) by A3, A5, A10;

            

             A13: ( <*n*> . 1) = n & ( <*i*> . 1) = i by FINSEQ_1: 40;

            then

             A14: (T | <*n*>) = (p . (n + 1)) by A12, Def4;

            

             A15: (p . (n + 1)) in ( rng p) by A12, A13, Lm2;

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

            then

            reconsider t = (p . (n + 1)) as Element of F by A15;

            

             A16: (t . q) = x by A2, A6, A9, A14, TREES_2:def 10;

            

             A17: (t . q) in ( rng t) by A9, A11, A14, FUNCT_1:def 3;

            ( rng t) c= D by RELAT_1:def 19;

            hence thesis by A16, A17;

          end;

          hence thesis by A2, A4;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

      let D be non empty set, d be Element of D, T be DecoratedTree of D;

      cluster (d -tree T) -> D -valued;

      coherence

      proof

        reconsider T as Element of ( Trees D) by TREES_3:def 7;

        reconsider t = <*T*> as Element of (( Trees D) * ) by FINSEQ_1:def 11;

        (d -tree T) = (d -tree t);

        hence thesis;

      end;

    end

    registration

      let D be non empty set, d be Element of D, T1,T2 be DecoratedTree of D;

      cluster (d -tree (T1,T2)) -> D -valued;

      coherence

      proof

        reconsider T1, T2 as Element of ( Trees D) by TREES_3:def 7;

         <*T1, T2*> = ( <*T1 qua Element of ( Trees D) qua non empty set*> ^ <*T2 qua Element of ( Trees D) qua non empty set*>);

        then

        reconsider t = <*T1, T2*> as Element of (( Trees D) * ) by FINSEQ_1:def 11;

        (d -tree (T1,T2)) = (d -tree t);

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      let p be FinSequence of ( FinTrees D);

      :: original: doms

      redefine

      func doms p -> FinSequence of FinTrees ;

      coherence

      proof

        

         A1: ( dom ( doms p)) = ( dom p) by TREES_3: 37;

        

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

        thus ( doms p) is FinSequence of FinTrees

        proof

          let x be object;

          assume x in ( rng ( doms p));

          then

          consider y be object such that

           A3: y in ( dom p) and

           A4: x = (( doms p) . y) by A1, FUNCT_1:def 3;

          reconsider T = (p . y) as DecoratedTree by A3, TREES_3: 24;

          T in ( rng p) by A3, FUNCT_1:def 3;

          then ( dom T) in FinTrees by A2, TREES_3:def 2;

          hence thesis by A3, A4, FUNCT_6: 22;

        end;

      end;

    end

    definition

      let D be non empty set;

      let d be Element of D, p be FinSequence of ( FinTrees D);

      :: original: -tree

      redefine

      func d -tree p -> Element of ( FinTrees D) ;

      coherence

      proof

        ( dom (d -tree p)) = ( tree ( doms p)) by Th10;

        hence thesis by TREES_3:def 8;

      end;

    end

    definition

      let D be non empty set, x be Subset of D;

      :: original: FinSequence

      redefine

      mode FinSequence of x -> FinSequence of D ;

      coherence

      proof

        let p be FinSequence of x;

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

        hence ( rng p) c= D by XBOOLE_1: 1;

      end;

    end

    registration

      let D be non empty constituted-DTrees set;

      let X be Subset of D;

      cluster -> DTree-yielding for FinSequence of X;

      coherence ;

    end

    begin

    scheme :: TREES_4:sch1

    ExpandTree { T1() -> Tree , T2() -> Tree , P[ set] } :

ex T be Tree st for p holds p in T iff p in T1() or ex q be Element of T1(), r be Element of T2() st P[q] & p = (q ^ r);

      defpred X[ object] means $1 in T1() or ex q be Element of T1(), r be Element of T2() st P[q] & $1 = (q ^ r);

      consider T be set such that

       A1: for x be object holds x in T iff x in ( NAT * ) & X[x] from XBOOLE_0:sch 1;

      set t = the Element of T1();

      t in ( NAT * ) by FINSEQ_1:def 11;

      then

      reconsider T as non empty set by A1;

      T is Tree-like

      proof

        thus T c= ( NAT * ) by A1;

        thus for p be FinSequence of NAT st p in T holds ( ProperPrefixes p) c= T

        proof

          let p be FinSequence of NAT such that

           A2: p in T;

          let x be object;

          assume x in ( ProperPrefixes p);

          then

          consider q such that

           A3: x = q and

           A4: q is_a_proper_prefix_of p by TREES_1:def 2;

          assume

           A5: not thesis;

          q is_a_prefix_of p by A4, XBOOLE_0:def 8;

          then

          consider r such that

           A6: p = (q ^ r) by TREES_1: 1;

          reconsider q, r as FinSequence of NAT by A6, FINSEQ_1: 36;

          (q ^ r) in T1() & q in ( NAT * ) & ((q ^ r) in T1() implies q in T1()) or ex q be Element of T1(), r be Element of T2() st P[q] & p = (q ^ r) by A1, A2, A6, FINSEQ_1:def 11, TREES_1: 21;

          then

          consider q9 be Element of T1(), r9 be Element of T2() such that

           A7: P[q9] and

           A8: (q ^ r) = (q9 ^ r9) by A1, A3, A5, A6;

          now

            assume ( len q) <= ( len q9);

            then ex s be FinSequence st (q ^ s) = q9 by A8, FINSEQ_1: 47;

            then

             A9: q in T1() by TREES_1: 21;

            q in ( NAT * ) by FINSEQ_1:def 11;

            hence contradiction by A1, A3, A5, A9;

          end;

          then

          consider s be FinSequence such that

           A10: (q9 ^ s) = q by A8, FINSEQ_1: 47;

          reconsider s as FinSequence of NAT by A10, FINSEQ_1: 36;

          (q9 ^ r9) = (q9 ^ (s ^ r)) by A8, A10, FINSEQ_1: 32;

          then (s ^ r) = r9 by FINSEQ_1: 33;

          then q in ( NAT * ) & s is Element of T2() by FINSEQ_1:def 11, TREES_1: 21;

          hence thesis by A1, A3, A5, A7, A10;

        end;

        let p be FinSequence of NAT , k,n be Nat;

        assume that

         A11: (p ^ <*k*>) in T and

         A12: n <= k;

         A13:

        now

          assume (p ^ <*k*>) in T1();

          then

           A14: (p ^ <*n*>) in T1() by A12, TREES_1:def 3;

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

          (p ^ <*n*>) in ( NAT * ) by FINSEQ_1:def 11;

          hence thesis by A1, A14;

        end;

        now

          assume

           A15: not (p ^ <*k*>) in T1();

          then

          consider q be Element of T1(), r be Element of T2() such that

           A16: P[q] and

           A17: (p ^ <*k*>) = (q ^ r) by A1, A11;

          (q ^ {} ) = q by FINSEQ_1: 34;

          then r <> {} by A15, A17;

          then

          consider w be FinSequence, z such that

           A18: r = (w ^ <*z*>) by FINSEQ_1: 46;

          reconsider w as FinSequence of NAT by A18, FINSEQ_1: 36;

          

           A19: (p ^ <*k*>) = ((q ^ w) ^ <*z*>) by A17, A18, FINSEQ_1: 32;

          

           A20: ((p ^ <*k*>) . (( len p) + 1)) = k & (((q ^ w) ^ <*z*>) . (( len (q ^ w)) + 1)) = z by FINSEQ_1: 42;

          

           A21: ( len <*k*>) = 1 & ( len <*z*>) = 1 by FINSEQ_1: 40;

          

           A22: ( len (p ^ <*k*>)) = (( len p) + ( len <*k*>)) & ( len ((q ^ w) ^ <*z*>)) = (( len (q ^ w)) + ( len <*z*>)) by FINSEQ_1: 22;

          then

           A23: p = (q ^ w) by A19, A20, A21, FINSEQ_1: 33;

          

           A24: (w ^ <*n*>) in T2() by A12, A18, A19, A20, A21, A22, TREES_1:def 3;

          

           A25: (p ^ <*n*>) = (q ^ (w ^ <*n*>)) by A23, FINSEQ_1: 32;

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

          (p ^ <*n*>) in ( NAT * ) by FINSEQ_1:def 11;

          hence thesis by A1, A16, A24, A25;

        end;

        hence thesis by A13;

      end;

      then

      reconsider T as Tree;

      take T;

      let p;

      p is Element of T1() or (ex q be Element of T1(), r be Element of T2() st P[q] & p = (q ^ r)) implies p in ( NAT * ) by FINSEQ_1:def 11;

      hence thesis by A1;

    end;

    definition

      let T,T9 be DecoratedTree;

      let x be set;

      :: TREES_4:def7

      func (T,x) <- T9 -> DecoratedTree means

      : Def7: (for p holds p in ( dom it ) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r)) & (for p be Node of T st not p in ( Leaves ( dom T)) or (T . p) <> x holds (it . p) = (T . p)) & for p be Node of T, q be Node of T9 st p in ( Leaves ( dom T)) & (T . p) = x holds (it . (p ^ q)) = (T9 . q);

      existence

      proof

        defpred X[ set] means $1 in ( Leaves ( dom T)) & (T . $1) = x;

        consider W be Tree such that

         A1: p in W iff p in ( dom T) or ex q be Node of T, r be Node of T9 st X[q] & p = (q ^ r) from ExpandTree;

        defpred X[ object, object] means $1 is Node of T & ( not $1 in ( Leaves ( dom T)) or (T . $1) <> x) & $2 = (T . $1) or ex p be Node of T, q be Node of T9 st $1 = (p ^ q) & p in ( Leaves ( dom T)) & (T . p) = x & $2 = (T9 . q);

        

         A2: for z be object st z in W holds ex y be object st X[z, y]

        proof

          let z be object;

          assume z in W;

          then

          reconsider w = z as Element of W;

           A3:

          now

            given q be Node of T, r be Node of T9 such that

             A4: q in ( Leaves ( dom T)) & (T . q) = x & w = (q ^ r);

            take y = (T9 . r), q, r;

            thus z = (q ^ r) & q in ( Leaves ( dom T)) & (T . q) = x & y = (T9 . r) by A4;

          end;

          now

            assume

             A5: not ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & w = (q ^ r);

            take y = (T . z);

            thus z is Node of T by A1, A5;

            reconsider w as Node of T by A1, A5;

            reconsider e = {} as Node of T9 by TREES_1: 22;

            (w ^ e) = w by FINSEQ_1: 34;

            hence ( not z in ( Leaves ( dom T)) or (T . z) <> x) & y = (T . z) by A5;

          end;

          hence thesis by A3;

        end;

        consider f be Function such that

         A6: ( dom f) = W & for z be object st z in W holds X[z, (f . z)] from CLASSES1:sch 1( A2);

        reconsider f as DecoratedTree by A6, TREES_2:def 8;

        take f;

        thus p in ( dom f) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r) by A1, A6;

        thus for p be Node of T st not p in ( Leaves ( dom T)) or (T . p) <> x holds (f . p) = (T . p)

        proof

          let p be Node of T;

          assume

           A7: not p in ( Leaves ( dom T)) or (T . p) <> x;

          

           A8: p in W by A1;

          now

            given p9 be Node of T, q be Node of T9 such that

             A9: p = (p9 ^ q) and

             A10: p9 in ( Leaves ( dom T)) and

             A11: (T . p9) = x and (f . p) = (T9 . q);

            p9 is_a_prefix_of p & not p9 is_a_proper_prefix_of p by A9, A10, TREES_1: 1, TREES_1:def 5;

            hence contradiction by A7, A10, A11, XBOOLE_0:def 8;

          end;

          hence thesis by A6, A8;

        end;

        let p be Node of T, q be Node of T9;

        assume that

         A12: p in ( Leaves ( dom T)) and

         A13: (T . p) = x;

        

         A14: (p ^ q) in W by A1, A12, A13;

        now

          assume (p ^ q) is Node of T;

          then

           A15: not p is_a_proper_prefix_of (p ^ q) by A12, TREES_1:def 5;

          p is_a_prefix_of (p ^ q) by TREES_1: 1;

          hence p = (p ^ q) by A15, XBOOLE_0:def 8;

        end;

        then

        consider p9 be Node of T, q9 be Node of T9 such that

         A16: (p ^ q) = (p9 ^ q9) and

         A17: p9 in ( Leaves ( dom T)) and (T . p9) = x and

         A18: (f . (p ^ q)) = (T9 . q9) by A6, A12, A13, A14;

        now

          let p,p9,q,q9 be FinSequence of NAT , T be Tree;

          assume that

           A19: (p ^ q) = (p9 ^ q9) and

           A20: p in ( Leaves T) & p9 in ( Leaves T) and

           A21: p <> p9;

          now

            assume ( len p) <= ( len p9);

            then ex r st (p ^ r) = p9 by A19, FINSEQ_1: 47;

            then p is_a_prefix_of p9 by TREES_1: 1;

            then p is_a_proper_prefix_of p9 by A21, XBOOLE_0:def 8;

            hence contradiction by A20, TREES_1:def 5;

          end;

          then ex r st (p9 ^ r) = p by A19, FINSEQ_1: 47;

          then p9 is_a_prefix_of p by TREES_1: 1;

          then p9 is_a_proper_prefix_of p by A21, XBOOLE_0:def 8;

          hence contradiction by A20, TREES_1:def 5;

        end;

        then p = p9 by A12, A16, A17;

        hence thesis by A16, A18, FINSEQ_1: 33;

      end;

      uniqueness

      proof

        let T1,T2 be DecoratedTree such that

         A22: p in ( dom T1) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r) and

         A23: for p be Node of T st not p in ( Leaves ( dom T)) or (T . p) <> x holds (T1 . p) = (T . p) and

         A24: for p be Node of T, q be Node of T9 st p in ( Leaves ( dom T)) & (T . p) = x holds (T1 . (p ^ q)) = (T9 . q) and

         A25: p in ( dom T2) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r) and

         A26: for p be Node of T st not p in ( Leaves ( dom T)) or (T . p) <> x holds (T2 . p) = (T . p) and

         A27: for p be Node of T, q be Node of T9 st p in ( Leaves ( dom T)) & (T . p) = x holds (T2 . (p ^ q)) = (T9 . q);

        

         A28: ( dom T1) = ( dom T2)

        proof

          let p be FinSequence of NAT ;

          p in ( dom T1) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r) by A22;

          hence thesis by A25;

        end;

        reconsider p9 = {} as Node of T9 by TREES_1: 22;

        now

          let y be object;

          assume y in ( dom T1);

          then

          reconsider p = y as Node of T1;

          per cases by A22;

            suppose p in ( dom T);

            then

            reconsider p as Node of T;

            hereby

              per cases ;

                suppose

                 A29: p in ( Leaves ( dom T)) & (T . p) = x;

                then

                 A30: (T1 . (p ^ p9)) = (T9 . p9) by A24;

                (p ^ p9) = p by FINSEQ_1: 34;

                hence (T1 . y) = (T2 . y) by A27, A29, A30;

              end;

                suppose

                 A31: not p in ( Leaves ( dom T)) or (T . p) <> x;

                then (T1 . p) = (T . p) by A23;

                hence (T1 . y) = (T2 . y) by A26, A31;

              end;

            end;

          end;

            suppose ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r);

            then

            consider q be Node of T, r be Node of T9 such that

             A32: q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r);

            

            thus (T1 . y) = (T9 . r) by A24, A32

            .= (T2 . y) by A27, A32;

          end;

        end;

        hence thesis by A28;

      end;

    end

    registration

      let D be non empty set;

      let T,T9 be DecoratedTree of D;

      let x be set;

      cluster ((T,x) <- T9) -> D -valued;

      coherence

      proof

        ( rng ((T,x) <- T9)) c= D

        proof

          let y be object;

          assume y in ( rng ((T,x) <- T9));

          then

          consider z be object such that

           A1: z in ( dom ((T,x) <- T9)) and

           A2: y = (((T,x) <- T9) . z) by FUNCT_1:def 3;

          reconsider z as Node of ((T,x) <- T9) by A1;

          reconsider p9 = {} as Node of T9 by TREES_1: 22;

          per cases by Def7;

            suppose z in ( dom T);

            then

            reconsider p = z as Node of T;

            hereby

              per cases ;

                suppose p in ( Leaves ( dom T)) & (T . p) = x;

                then

                 A3: (((T,x) <- T9) . (p ^ p9)) = (T9 . p9) by Def7;

                (p ^ p9) = p by FINSEQ_1: 34;

                hence thesis by A2, A3;

              end;

                suppose not p in ( Leaves ( dom T)) or (T . p) <> x;

                then (((T,x) <- T9) . p) = (T . p) by Def7;

                hence thesis by A2;

              end;

            end;

          end;

            suppose ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & z = (q ^ r);

            then

            consider q be Node of T, r be Node of T9 such that

             A4: q in ( Leaves ( dom T)) & (T . q) = x & z = (q ^ r);

            (((T,x) <- T9) . z) = (T9 . r) by A4, Def7;

            hence thesis by A2;

          end;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    reserve T,T9 for DecoratedTree,

x,y for set;

    theorem :: TREES_4:23

     not x in ( rng T) or not x in ( Leaves T) implies ((T,x) <- T9) = T

    proof

      

       A1: ( Leaves T) c= ( rng T) by RELAT_1: 111;

      assume not x in ( rng T) or not x in ( Leaves T);

      then

       A2: not x in ( Leaves T) by A1;

      thus

       A3: ( dom ((T,x) <- T9)) = ( dom T)

      proof

        let p be FinSequence of NAT ;

        p in ( dom ((T,x) <- T9)) iff p in ( dom T) or ex q be Node of T, r be Node of T9 st q in ( Leaves ( dom T)) & (T . q) = x & p = (q ^ r) by Def7;

        hence thesis by A2, FUNCT_1:def 6;

      end;

      let p be Node of ((T,x) <- T9);

      reconsider p9 = p as Node of T by A3;

      p9 in ( Leaves ( dom T)) implies (T . p9) in ( Leaves T) by FUNCT_1:def 6;

      hence thesis by A2, Def7;

    end;

    begin

    reserve D1,D2 for non empty set,

T for DecoratedTree of D1, D2,

d1 for Element of D1,

d2 for Element of D2,

F for non empty DTree-set of D1, D2,

F1 for non empty DTree-set of D1,

F2 for non empty DTree-set of D2;

    theorem :: TREES_4:24

    

     Th24: for D1, D2, T holds ( dom (T `1 )) = ( dom T) & ( dom (T `2 )) = ( dom T)

    proof

      let D1, D2, T;

      

       A1: (T `1 ) = (( pr1 (D1,D2)) * T) & (T `2 ) = (( pr2 (D1,D2)) * T) by TREES_3:def 12, TREES_3:def 13;

      

       A2: ( rng T) c= [:D1, D2:] & ( dom ( pr1 (D1,D2))) = [:D1, D2:] by FUNCT_2:def 1, RELAT_1:def 19;

      ( dom ( pr2 (D1,D2))) = [:D1, D2:] by FUNCT_2:def 1;

      hence thesis by A1, A2, RELAT_1: 27;

    end;

    theorem :: TREES_4:25

    

     Th25: (( root-tree [d1, d2]) `1 ) = ( root-tree d1) & (( root-tree [d1, d2]) `2 ) = ( root-tree d2)

    proof

      reconsider r = {} as Node of ( root-tree [d1, d2]) by TREES_1: 22;

      

       A1: ( dom (( root-tree [d1, d2]) `1 )) = ( dom ( root-tree [d1, d2])) by Th24;

      

       A2: ( dom (( root-tree [d1, d2]) `2 )) = ( dom ( root-tree [d1, d2])) by Th24;

      

       A3: (( root-tree [d1, d2]) . r) = [d1, d2];

      

       A4: ( [d1, d2] `1 ) = d1;

      

       A5: ( [d1, d2] `2 ) = d2;

      

      thus (( root-tree [d1, d2]) `1 ) = ( root-tree ((( root-tree [d1, d2]) `1 ) . r)) by A1, Th5

      .= ( root-tree d1) by A3, A4, TREES_3: 39;

      

      thus (( root-tree [d1, d2]) `2 ) = ( root-tree ((( root-tree [d1, d2]) `2 ) . r)) by A2, Th5

      .= ( root-tree d2) by A3, A5, TREES_3: 39;

    end;

    theorem :: TREES_4:26

     <:( root-tree x), ( root-tree y):> = ( root-tree [x, y])

    proof

      reconsider x9 = x as Element of {x} by TARSKI:def 1;

      reconsider y9 = y as Element of {y} by TARSKI:def 1;

      (( root-tree [x9, y9]) `1 ) = ( root-tree x) & (( root-tree [x9, y9]) `2 ) = ( root-tree y) by Th25;

      hence thesis by TREES_3: 40;

    end;

    theorem :: TREES_4:27

    

     Th27: for D1, D2, d1, d2, F, F1 holds for p be FinSequence of F, p1 be FinSequence of F1 st ( dom p1) = ( dom p) & for i st i in ( dom p) holds for T st T = (p . i) holds (p1 . i) = (T `1 ) holds (( [d1, d2] -tree p) `1 ) = (d1 -tree p1)

    proof

      let D1, D2, d1, d2, F, F1;

      let p be FinSequence of F, p1 be FinSequence of F1 such that

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

       A2: for i st i in ( dom p) holds for T st T = (p . i) holds (p1 . i) = (T `1 );

      set W = ( [d1, d2] -tree p), W1 = (d1 -tree p1);

      

       A3: ( len ( doms p)) = ( len p) by TREES_3: 38;

      

       A4: ( len ( doms p1)) = ( len p1) by TREES_3: 38;

      

       A5: ( len p) = ( len p1) by A1, FINSEQ_3: 29;

      then

       A6: ( dom ( doms p)) = ( dom ( doms p1)) by A3, A4, FINSEQ_3: 29;

      

       A7: ( dom ( doms p)) = ( dom p) by A3, FINSEQ_3: 29;

      now

        let i be Nat;

        assume

         A8: i in ( dom p);

        then

        reconsider T = (p . i) as Element of F by Lm1;

        

         A9: (p1 . i) = (T `1 ) by A2, A8;

        

         A10: (( doms p) . i) = ( dom T) by A8, FUNCT_6: 22;

        (( doms p1) . i) = ( dom (T `1 )) by A1, A8, A9, FUNCT_6: 22;

        hence (( doms p) . i) = (( doms p1) . i) by A10, Th24;

      end;

      then

       A11: ( doms p) = ( doms p1) by A6, A7, FINSEQ_1: 13;

      ( dom (W `1 )) = ( dom W) by Th24

      .= ( tree ( doms p)) by Th10;

      hence ( dom (W `1 )) = ( dom W1) by A11, Th10;

      let x be Node of (W `1 );

      reconsider a = x as Node of W by Th24;

      

       A12: ((W `1 ) . x) = ((W . a) `1 ) by TREES_3: 39;

      per cases ;

        suppose x = {} ;

        then (W . x) = [d1, d2] & (W1 . x) = d1 by Def4;

        hence thesis by A12;

      end;

        suppose x <> {} ;

        then

        consider n be Nat, T be DecoratedTree, q be Node of T such that

         A13: n < ( len p) and

         A14: T = (p . (n + 1)) and

         A15: a = ( <*n*> ^ q) by Th11;

        reconsider T as Element of F by A13, A14, Lm3;

        reconsider q as Node of (T `1 ) by Th24;

        

         A16: (p1 . (n + 1)) = (T `1 ) by A2, A13, A14, Lm2;

        

         A17: (W . a) = (T . q) by A13, A14, A15, Th12;

        (W1 . a) = ((T `1 ) . q) by A5, A13, A15, A16, Th12;

        hence thesis by A12, A17, TREES_3: 39;

      end;

    end;

    theorem :: TREES_4:28

    

     Th28: for D1, D2, d1, d2, F, F2 holds for p be FinSequence of F, p2 be FinSequence of F2 st ( dom p2) = ( dom p) & for i st i in ( dom p) holds for T st T = (p . i) holds (p2 . i) = (T `2 ) holds (( [d1, d2] -tree p) `2 ) = (d2 -tree p2)

    proof

      let D1, D2, d1, d2, F, F2;

      let p be FinSequence of F, p2 be FinSequence of F2 such that

       A1: ( dom p2) = ( dom p) and

       A2: for i st i in ( dom p) holds for T st T = (p . i) holds (p2 . i) = (T `2 );

      set W = ( [d1, d2] -tree p), W2 = (d2 -tree p2);

      

       A3: ( len ( doms p)) = ( len p) by TREES_3: 38;

      

       A4: ( len ( doms p2)) = ( len p2) by TREES_3: 38;

      

       A5: ( len p) = ( len p2) by A1, FINSEQ_3: 29;

      then

       A6: ( dom ( doms p)) = ( dom ( doms p2)) by A3, A4, FINSEQ_3: 29;

      

       A7: ( dom ( doms p)) = ( dom p) by A3, FINSEQ_3: 29;

      now

        let i be Nat;

        assume

         A8: i in ( dom p);

        then

        reconsider T = (p . i) as Element of F by Lm1;

        

         A9: (p2 . i) = (T `2 ) by A2, A8;

        

         A10: (( doms p) . i) = ( dom T) by A8, FUNCT_6: 22;

        (( doms p2) . i) = ( dom (T `2 )) by A1, A8, A9, FUNCT_6: 22;

        hence (( doms p) . i) = (( doms p2) . i) by A10, Th24;

      end;

      then

       A11: ( doms p) = ( doms p2) by A6, A7, FINSEQ_1: 13;

      ( dom (W `2 )) = ( dom W) by Th24

      .= ( tree ( doms p)) by Th10;

      hence ( dom (W `2 )) = ( dom W2) by A11, Th10;

      let x be Node of (W `2 );

      reconsider a = x as Node of W by Th24;

      

       A12: ((W `2 ) . x) = ((W . a) `2 ) by TREES_3: 39;

      per cases ;

        suppose x = {} ;

        then (W . x) = [d1, d2] & (W2 . x) = d2 by Def4;

        hence thesis by A12;

      end;

        suppose x <> {} ;

        then

        consider n be Nat, T be DecoratedTree, q be Node of T such that

         A13: n < ( len p) and

         A14: T = (p . (n + 1)) and

         A15: a = ( <*n*> ^ q) by Th11;

        reconsider T as Element of F by A13, A14, Lm3;

        reconsider q as Node of (T `2 ) by Th24;

        

         A16: (p2 . (n + 1)) = (T `2 ) by A2, A13, A14, Lm2;

        

         A17: (W . a) = (T . q) by A13, A14, A15, Th12;

        (W2 . a) = ((T `2 ) . q) by A5, A13, A15, A16, Th12;

        hence thesis by A12, A17, TREES_3: 39;

      end;

    end;

    theorem :: TREES_4:29

    

     Th29: for D1, D2, d1, d2, F holds for p be FinSequence of F holds ex p1 be FinSequence of ( Trees D1) st ( dom p1) = ( dom p) & (for i st i in ( dom p) holds ex T be Element of F st T = (p . i) & (p1 . i) = (T `1 )) & (( [d1, d2] -tree p) `1 ) = (d1 -tree p1)

    proof

      let D1, D2, d1, d2, F;

      let p be FinSequence of F;

      

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

      defpred X[ set, set] means ex T be Element of F st T = (p . $1) & $2 = (T `1 );

      

       A2: for i be Nat st i in ( Seg ( len p)) holds ex x be Element of ( Trees D1) st X[i, x]

      proof

        let i be Nat;

        assume i in ( Seg ( len p));

        then

        reconsider T = (p . i) as Element of F by A1, Lm1;

        reconsider y = (T `1 ) as Element of ( Trees D1) by TREES_3:def 7;

        take y, T;

        thus thesis;

      end;

      consider p1 be FinSequence of ( Trees D1) such that

       A3: ( dom p1) = ( Seg ( len p)) & for i be Nat st i in ( Seg ( len p)) holds X[i, (p1 . i)] from FINSEQ_1:sch 5( A2);

      take p1;

      thus

       A4: ( dom p1) = ( dom p) by A3, FINSEQ_1:def 3;

      hence for i st i in ( dom p) holds ex T be Element of F st T = (p . i) & (p1 . i) = (T `1 ) by A3;

      now

        let i;

        assume i in ( dom p);

        then ex T be Element of F st T = (p . i) & (p1 . i) = (T `1 ) by A3, A4;

        hence for T st T = (p . i) holds (p1 . i) = (T `1 );

      end;

      hence thesis by A4, Th27;

    end;

    theorem :: TREES_4:30

    

     Th30: for D1, D2, d1, d2, F holds for p be FinSequence of F holds ex p2 be FinSequence of ( Trees D2) st ( dom p2) = ( dom p) & (for i st i in ( dom p) holds ex T be Element of F st T = (p . i) & (p2 . i) = (T `2 )) & (( [d1, d2] -tree p) `2 ) = (d2 -tree p2)

    proof

      let D1, D2, d1, d2, F;

      let p be FinSequence of F;

      

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

      defpred X[ Nat, set] means ex T be Element of F st T = (p . $1) & $2 = (T `2 );

      

       A2: for i be Nat st i in ( Seg ( len p)) holds ex x be Element of ( Trees D2) st X[i, x]

      proof

        let i be Nat;

        assume i in ( Seg ( len p));

        then

        reconsider T = (p . i) as Element of F by A1, Lm1;

        reconsider y = (T `2 ) as Element of ( Trees D2) by TREES_3:def 7;

        take y, T;

        thus thesis;

      end;

      consider p2 be FinSequence of ( Trees D2) such that

       A3: ( dom p2) = ( Seg ( len p)) & for i be Nat st i in ( Seg ( len p)) holds X[i, (p2 . i)] from FINSEQ_1:sch 5( A2);

      take p2;

      thus

       A4: ( dom p2) = ( dom p) by A3, FINSEQ_1:def 3;

      hence for i st i in ( dom p) holds ex T be Element of F st T = (p . i) & (p2 . i) = (T `2 ) by A3;

      now

        let i;

        assume i in ( dom p);

        then ex T be Element of F st T = (p . i) & (p2 . i) = (T `2 ) by A3, A4;

        hence for T st T = (p . i) holds (p2 . i) = (T `2 );

      end;

      hence thesis by A4, Th28;

    end;

    theorem :: TREES_4:31

    for D1, D2, d1, d2 holds for p be FinSequence of ( FinTrees [:D1, D2:]) holds ex p1 be FinSequence of ( FinTrees D1) st ( dom p1) = ( dom p) & (for i st i in ( dom p) holds ex T be Element of ( FinTrees [:D1, D2:]) st T = (p . i) & (p1 . i) = (T `1 )) & (( [d1, d2] -tree p) `1 ) = (d1 -tree p1)

    proof

      let D1, D2, d1, d2;

      let p be FinSequence of ( FinTrees [:D1, D2:]);

      consider p1 be FinSequence of ( Trees D1) such that

       A1: ( dom p1) = ( dom p) & for i st i in ( dom p) holds ex T be Element of ( FinTrees [:D1, D2:]) st T = (p . i) & (p1 . i) = (T `1 ) and

       A2: (( [d1, d2] -tree p) `1 ) = (d1 -tree p1) by Th29;

      ( rng p1) c= ( FinTrees D1)

      proof

        let x be object;

        assume x in ( rng p1);

        then

        consider y be object such that

         A3: y in ( dom p1) and

         A4: x = (p1 . y) by FUNCT_1:def 3;

        reconsider y as Nat by A3;

        consider T be Element of ( FinTrees [:D1, D2:]) such that T = (p . y) and

         A5: (p1 . y) = (T `1 ) by A1, A3;

        ( dom (T `1 )) = ( dom T) by Th24;

        hence thesis by A4, A5, TREES_3:def 8;

      end;

      then p1 is FinSequence of ( FinTrees D1) by FINSEQ_1:def 4;

      hence thesis by A1, A2;

    end;

    theorem :: TREES_4:32

    for D1, D2, d1, d2 holds for p be FinSequence of ( FinTrees [:D1, D2:]) holds ex p2 be FinSequence of ( FinTrees D2) st ( dom p2) = ( dom p) & (for i st i in ( dom p) holds ex T be Element of ( FinTrees [:D1, D2:]) st T = (p . i) & (p2 . i) = (T `2 )) & (( [d1, d2] -tree p) `2 ) = (d2 -tree p2)

    proof

      let D1, D2, d1, d2;

      let p be FinSequence of ( FinTrees [:D1, D2:]);

      consider p2 be FinSequence of ( Trees D2) such that

       A1: ( dom p2) = ( dom p) & for i st i in ( dom p) holds ex T be Element of ( FinTrees [:D1, D2:]) st T = (p . i) & (p2 . i) = (T `2 ) and

       A2: (( [d1, d2] -tree p) `2 ) = (d2 -tree p2) by Th30;

      ( rng p2) c= ( FinTrees D2)

      proof

        let x be object;

        assume x in ( rng p2);

        then

        consider y be object such that

         A3: y in ( dom p2) and

         A4: x = (p2 . y) by FUNCT_1:def 3;

        reconsider y as Nat by A3;

        consider T be Element of ( FinTrees [:D1, D2:]) such that T = (p . y) and

         A5: (p2 . y) = (T `2 ) by A1, A3;

        ( dom (T `2 )) = ( dom T) by Th24;

        hence thesis by A4, A5, TREES_3:def 8;

      end;

      then p2 is FinSequence of ( FinTrees D2) by FINSEQ_1:def 4;

      hence thesis by A1, A2;

    end;