trees_3.miz



    begin

    reserve x,y,z for object,

X,Y for set,

i,k,n for Nat,

p,q,r,s for FinSequence,

w for FinSequence of NAT ,

f for Function;

    

     Lm1: 1 <= n & n <= ( len p) implies ((p ^ q) . n) = (p . n)

    proof

      assume that

       A1: 1 <= n and

       A2: n <= ( len p);

      n in ( dom p) by A1, A2, FINSEQ_3: 25;

      hence thesis by FINSEQ_1:def 7;

    end;

    begin

    definition

      :: TREES_3:def1

      func Trees -> set means

      : Def1: x in it iff x is Tree;

      existence

      proof

        set X = { T where T be Subset of ( NAT * ) : T is Tree };

        take X;

        let x;

        thus x in X implies x is Tree

        proof

          assume x in X;

          then ex T be Subset of ( NAT * ) st x = T & T is Tree;

          hence thesis;

        end;

        assume x is Tree;

        then

        reconsider T = x as Tree;

        T is Subset of ( NAT * ) by TREES_1:def 3;

        hence thesis;

      end;

      uniqueness

      proof

        defpred X[ object] means $1 is Tree;

        let T1,T2 be set such that

         A1: x in T1 iff X[x] and

         A2: x in T2 iff X[x];

        thus thesis from XBOOLE_0:sch 2( A1, A2);

      end;

    end

    registration

      cluster Trees -> non empty;

      coherence

      proof

        set T = the Tree;

        T in Trees by Def1;

        hence thesis;

      end;

    end

    definition

      :: TREES_3:def2

      func FinTrees -> Subset of Trees means

      : Def2: x in it iff x is finite Tree;

      existence

      proof

        set X = { T where T be Element of Trees : T is finite Tree };

        X c= Trees

        proof

          let x be object;

          assume x in X;

          then ex T be Element of Trees st x = T & T is finite Tree;

          hence thesis;

        end;

        then

        reconsider X as Subset of Trees ;

        take X;

        let x;

        thus x in X implies x is finite Tree

        proof

          assume x in X;

          then ex T be Element of Trees st x = T & T is finite Tree;

          hence thesis;

        end;

        assume x is finite Tree;

        then

        reconsider T = x as finite Tree;

        T in Trees by Def1;

        hence thesis;

      end;

      uniqueness

      proof

        defpred X[ object] means $1 is finite Tree;

        let T1,T2 be Subset of Trees such that

         A1: x in T1 iff X[x] and

         A2: x in T2 iff X[x];

        thus thesis from XBOOLE_0:sch 2( A1, A2);

      end;

    end

    registration

      cluster FinTrees -> non empty;

      coherence

      proof

        set T = the finite Tree;

        T in FinTrees by Def2;

        hence thesis;

      end;

    end

    definition

      let IT be set;

      :: TREES_3:def3

      attr IT is constituted-Trees means

      : Def3: for x st x in IT holds x is Tree;

      :: TREES_3:def4

      attr IT is constituted-FinTrees means

      : Def4: for x st x in IT holds x is finite Tree;

      :: TREES_3:def5

      attr IT is constituted-DTrees means

      : Def5: for x st x in IT holds x is DecoratedTree;

    end

    theorem :: TREES_3:1

    X is constituted-Trees iff X c= Trees

    proof

      thus X is constituted-Trees implies X c= Trees

      proof

        assume

         A1: for x st x in X holds x is Tree;

        let x be object;

        assume x in X;

        then x is Tree by A1;

        hence thesis by Def1;

      end;

      assume

       A2: X c= Trees ;

      let x;

      assume x in X;

      hence thesis by A2, Def1;

    end;

    theorem :: TREES_3:2

    X is constituted-FinTrees iff X c= FinTrees

    proof

      thus X is constituted-FinTrees implies X c= FinTrees

      proof

        assume

         A1: for x st x in X holds x is finite Tree;

        let x be object;

        assume x in X;

        then x is finite Tree by A1;

        hence thesis by Def2;

      end;

      assume

       A2: X c= FinTrees ;

      let x;

      assume x in X;

      hence thesis by A2, Def2;

    end;

    theorem :: TREES_3:3

    

     Th3: X is constituted-Trees & Y is constituted-Trees iff (X \/ Y) is constituted-Trees

    proof

      thus X is constituted-Trees & Y is constituted-Trees implies (X \/ Y) is constituted-Trees

      proof

        assume that

         A1: for x st x in X holds x is Tree and

         A2: for x st x in Y holds x is Tree;

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis by A1, A2;

      end;

      assume

       A3: for x st x in (X \/ Y) holds x is Tree;

      thus X is constituted-Trees

      proof

        let x;

        assume x in X;

        then x in (X \/ Y) by XBOOLE_0:def 3;

        hence thesis by A3;

      end;

      let x;

      assume x in Y;

      then x in (X \/ Y) by XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: TREES_3:4

    X is constituted-Trees & Y is constituted-Trees implies (X \+\ Y) is constituted-Trees

    proof

      assume that

       A1: for x st x in X holds x is Tree and

       A2: for x st x in Y holds x is Tree;

      let x;

      assume x in (X \+\ Y);

      then not x in X iff x in Y by XBOOLE_0: 1;

      hence thesis by A1, A2;

    end;

    theorem :: TREES_3:5

    X is constituted-Trees implies (X /\ Y) is constituted-Trees & (Y /\ X) is constituted-Trees & (X \ Y) is constituted-Trees

    proof

      assume

       A1: for x st x in X holds x is Tree;

      thus (X /\ Y) is constituted-Trees

      proof

        let x;

        assume x in (X /\ Y);

        then x in X by XBOOLE_0:def 4;

        hence thesis by A1;

      end;

      hence (Y /\ X) is constituted-Trees;

      let x;

      assume x in (X \ Y);

      hence thesis by A1;

    end;

    theorem :: TREES_3:6

    

     Th6: X is constituted-FinTrees & Y is constituted-FinTrees iff (X \/ Y) is constituted-FinTrees

    proof

      thus X is constituted-FinTrees & Y is constituted-FinTrees implies (X \/ Y) is constituted-FinTrees

      proof

        assume that

         A1: for x st x in X holds x is finite Tree and

         A2: for x st x in Y holds x is finite Tree;

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis by A1, A2;

      end;

      assume

       A3: for x st x in (X \/ Y) holds x is finite Tree;

      thus X is constituted-FinTrees

      proof

        let x;

        assume x in X;

        then x in (X \/ Y) by XBOOLE_0:def 3;

        hence thesis by A3;

      end;

      let x;

      assume x in Y;

      then x in (X \/ Y) by XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: TREES_3:7

    X is constituted-FinTrees & Y is constituted-FinTrees implies (X \+\ Y) is constituted-FinTrees

    proof

      assume that

       A1: for x st x in X holds x is finite Tree and

       A2: for x st x in Y holds x is finite Tree;

      let x;

      assume x in (X \+\ Y);

      then not x in X iff x in Y by XBOOLE_0: 1;

      hence thesis by A1, A2;

    end;

    theorem :: TREES_3:8

    X is constituted-FinTrees implies (X /\ Y) is constituted-FinTrees & (Y /\ X) is constituted-FinTrees & (X \ Y) is constituted-FinTrees

    proof

      assume

       A1: for x st x in X holds x is finite Tree;

      thus (X /\ Y) is constituted-FinTrees

      proof

        let x;

        assume x in (X /\ Y);

        then x in X by XBOOLE_0:def 4;

        hence thesis by A1;

      end;

      hence (Y /\ X) is constituted-FinTrees;

      let x;

      assume x in (X \ Y);

      hence thesis by A1;

    end;

    theorem :: TREES_3:9

    

     Th9: X is constituted-DTrees & Y is constituted-DTrees iff (X \/ Y) is constituted-DTrees

    proof

      thus X is constituted-DTrees & Y is constituted-DTrees implies (X \/ Y) is constituted-DTrees

      proof

        assume that

         A1: for x st x in X holds x is DecoratedTree and

         A2: for x st x in Y holds x is DecoratedTree;

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis by A1, A2;

      end;

      assume

       A3: for x st x in (X \/ Y) holds x is DecoratedTree;

      thus X is constituted-DTrees

      proof

        let x;

        assume x in X;

        then x in (X \/ Y) by XBOOLE_0:def 3;

        hence thesis by A3;

      end;

      let x;

      assume x in Y;

      then x in (X \/ Y) by XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: TREES_3:10

    X is constituted-DTrees & Y is constituted-DTrees implies (X \+\ Y) is constituted-DTrees

    proof

      assume that

       A1: for x st x in X holds x is DecoratedTree and

       A2: for x st x in Y holds x is DecoratedTree;

      let x;

      assume x in (X \+\ Y);

      then not x in X iff x in Y by XBOOLE_0: 1;

      hence thesis by A1, A2;

    end;

    theorem :: TREES_3:11

    X is constituted-DTrees implies (X /\ Y) is constituted-DTrees & (Y /\ X) is constituted-DTrees & (X \ Y) is constituted-DTrees

    proof

      assume

       A1: for x st x in X holds x is DecoratedTree;

      thus (X /\ Y) is constituted-DTrees

      proof

        let x;

        assume x in (X /\ Y);

        then x in X by XBOOLE_0:def 4;

        hence thesis by A1;

      end;

      hence (Y /\ X) is constituted-DTrees;

      let x;

      assume x in (X \ Y);

      hence thesis by A1;

    end;

    registration

      cluster empty -> constituted-Trees constituted-FinTrees constituted-DTrees for set;

      coherence ;

    end

    theorem :: TREES_3:12

    

     Th12: {x} is constituted-Trees iff x is Tree

    proof

      thus {x} is constituted-Trees implies x is Tree

      proof

        assume

         A1: for y st y in {x} holds y is Tree;

        x in {x} by TARSKI:def 1;

        hence thesis by A1;

      end;

      assume

       A2: x is Tree;

      let y;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: TREES_3:13

    

     Th13: for x be object holds {x} is constituted-FinTrees iff x is finite Tree

    proof

      let x be object;

      thus {x} is constituted-FinTrees implies x is finite Tree

      proof

        assume

         A1: for y st y in {x} holds y is finite Tree;

        x in {x} by TARSKI:def 1;

        hence thesis by A1;

      end;

      assume

       A2: x is finite Tree;

      let y;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: TREES_3:14

    

     Th14: {x} is constituted-DTrees iff x is DecoratedTree

    proof

      thus {x} is constituted-DTrees implies x is DecoratedTree

      proof

        assume

         A1: for y st y in {x} holds y is DecoratedTree;

        x in {x} by TARSKI:def 1;

        hence thesis by A1;

      end;

      assume

       A2: x is DecoratedTree;

      let y;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: TREES_3:15

    

     Th15: {x, y} is constituted-Trees iff x is Tree & y is Tree

    proof

      thus {x, y} is constituted-Trees implies x is Tree & y is Tree

      proof

        assume

         A1: for z st z in {x, y} holds z is Tree;

        

         A2: x in {x, y} by TARSKI:def 2;

        y in {x, y} by TARSKI:def 2;

        hence thesis by A1, A2;

      end;

      assume that

       A3: x is Tree and

       A4: y is Tree;

      let z;

      thus thesis by A3, A4, TARSKI:def 2;

    end;

    theorem :: TREES_3:16

    

     Th16: {x, y} is constituted-FinTrees iff x is finite Tree & y is finite Tree

    proof

      thus {x, y} is constituted-FinTrees implies x is finite Tree & y is finite Tree

      proof

        assume

         A1: for z st z in {x, y} holds z is finite Tree;

        

         A2: x in {x, y} by TARSKI:def 2;

        y in {x, y} by TARSKI:def 2;

        hence thesis by A1, A2;

      end;

      assume that

       A3: x is finite Tree and

       A4: y is finite Tree;

      let z;

      thus thesis by A3, A4, TARSKI:def 2;

    end;

    theorem :: TREES_3:17

    

     Th17: {x, y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree

    proof

      thus {x, y} is constituted-DTrees implies x is DecoratedTree & y is DecoratedTree

      proof

        assume

         A1: for z st z in {x, y} holds z is DecoratedTree;

        

         A2: x in {x, y} by TARSKI:def 2;

        y in {x, y} by TARSKI:def 2;

        hence thesis by A1, A2;

      end;

      assume that

       A3: x is DecoratedTree and

       A4: y is DecoratedTree;

      let z;

      thus thesis by A3, A4, TARSKI:def 2;

    end;

    theorem :: TREES_3:18

    X is constituted-Trees & Y c= X implies Y is constituted-Trees;

    theorem :: TREES_3:19

    X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees;

    theorem :: TREES_3:20

    X is constituted-DTrees & Y c= X implies Y is constituted-DTrees;

    registration

      cluster finite constituted-Trees constituted-FinTrees non empty for set;

      existence

      proof

        set T = the finite Tree;

        take {T};

        thus thesis by Th12, Th13;

      end;

      cluster finite constituted-DTrees non empty for set;

      existence

      proof

        set T = the DecoratedTree;

        take {T};

        thus thesis by Th14;

      end;

    end

    registration

      cluster constituted-FinTrees -> constituted-Trees for set;

      coherence ;

    end

    registration

      let X be constituted-Trees set;

      cluster -> constituted-Trees for Subset of X;

      coherence by Def3;

    end

    registration

      let X be constituted-FinTrees set;

      cluster -> constituted-FinTrees for Subset of X;

      coherence by Def4;

    end

    registration

      let X be constituted-DTrees set;

      cluster -> constituted-DTrees for Subset of X;

      coherence by Def5;

    end

    registration

      let D be constituted-Trees non empty set;

      cluster -> non empty Tree-like for Element of D;

      coherence by Def3;

    end

    registration

      let D be constituted-FinTrees non empty set;

      cluster -> finite for Element of D;

      coherence by Def4;

    end

    registration

      cluster constituted-DTrees -> functional for set;

      coherence ;

    end

    registration

      let D be constituted-DTrees non empty set;

      cluster -> DecoratedTree-like for Element of D;

      coherence by Def5;

    end

    registration

      cluster Trees -> constituted-Trees;

      coherence by Def1;

    end

    registration

      cluster FinTrees -> constituted-FinTrees;

      coherence by Def2;

    end

    registration

      cluster constituted-FinTrees non empty for Subset of Trees ;

      existence

      proof

        take FinTrees ;

        thus thesis;

      end;

    end

    definition

      let D be non empty set;

      :: TREES_3:def6

      mode DTree-set of D -> non empty set means

      : Def6: for x st x in it holds x is DecoratedTree of D;

      existence

      proof

        take {(( elementary_tree 0 ) --> the Element of D)};

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let D be non empty set;

      cluster -> constituted-DTrees for DTree-set of D;

      coherence by Def6;

    end

    registration

      let D be non empty set;

      cluster finite non empty for DTree-set of D;

      existence

      proof

        set X = { the DecoratedTree of D};

        X is constituted-DTrees by TARSKI:def 1;

        then

        reconsider X as non empty constituted-DTrees set;

        X is DTree-set of D

        proof

          let x;

          thus thesis by TARSKI:def 1;

        end;

        then

        reconsider X as DTree-set of D;

        take X;

        thus thesis;

      end;

    end

    registration

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

      cluster -> D -valued for Element of E;

      coherence by Def6;

    end

    definition

      let T be Tree, D be non empty set;

      :: original: Funcs

      redefine

      func Funcs (T,D) -> non empty DTree-set of D ;

      coherence

      proof

        set F = ( Funcs (T,D));

        F is constituted-DTrees

        proof

          let x;

          assume x in F;

          then ex f be Function st (x = f) & (( dom f) = T) & (( rng f) c= D) by FUNCT_2:def 2;

          hence thesis by TREES_2:def 8;

        end;

        then

        reconsider F as non empty constituted-DTrees set;

        F is DTree-set of D

        proof

          let x;

          assume x in F;

          then ex f be Function st (x = f) & (( dom f) = T) & (( rng f) c= D) by FUNCT_2:def 2;

          hence thesis by RELAT_1:def 19, TREES_2:def 8;

        end;

        then

        reconsider F as DTree-set of D;

        set d = the Function of T, D;

        

         A1: ( dom d) = T by FUNCT_2:def 1;

        ( rng d) c= D;

        then d in F by A1, FUNCT_2:def 2;

        hence thesis;

      end;

    end

    registration

      let T be Tree, D be non empty set;

      cluster -> DecoratedTree-like for Function of T, D;

      coherence by FUNCT_2:def 1;

    end

    definition

      let D be non empty set;

      :: TREES_3:def7

      func Trees (D) -> DTree-set of D means

      : Def7: for T be DecoratedTree of D holds T in it ;

      existence

      proof

        set A = the set of all ( Funcs (T,D)) where T be Element of Trees ;

        set TT = ( union A);

        set f = ( the Element of Trees --> the Element of D);

        

         A1: f in ( Funcs ( the Element of Trees ,D)) by FUNCT_2: 8;

        

         A2: ( Funcs ( the Element of Trees ,D)) in A;

        TT is constituted-DTrees

        proof

          let x;

          assume x in TT;

          then

          consider X such that

           A3: x in X and

           A4: X in the set of all ( Funcs (T,D)) where T be Element of Trees by TARSKI:def 4;

          ex T be Element of Trees st (X = ( Funcs (T,D))) by A4;

          hence thesis by A3;

        end;

        then

        reconsider TT as non empty constituted-DTrees set by A2, A1, TARSKI:def 4;

        TT is DTree-set of D

        proof

          let x;

          assume x in TT;

          then

          consider X such that

           A5: x in X and

           A6: X in the set of all ( Funcs (T,D)) where T be Element of Trees by TARSKI:def 4;

          ex T be Element of Trees st (X = ( Funcs (T,D))) by A6;

          hence thesis by A5;

        end;

        then

        reconsider TT as DTree-set of D;

        take TT;

        let T be DecoratedTree of D;

        reconsider t = ( dom T) as Element of Trees by Def1;

        ( rng T) c= D;

        then

         A7: T in ( Funcs (t,D)) by FUNCT_2:def 2;

        ( Funcs (t,D)) in the set of all ( Funcs (W,D)) where W be Element of Trees ;

        hence thesis by A7, TARSKI:def 4;

      end;

      uniqueness

      proof

        let T1,T2 be DTree-set of D such that

         A8: for T be DecoratedTree of D holds T in T1 and

         A9: for T be DecoratedTree of D holds T in T2;

        thus T1 c= T2 by A9;

        let x be object;

        thus thesis by A8;

      end;

    end

    registration

      let D be non empty set;

      cluster ( Trees D) -> non empty;

      coherence ;

    end

    definition

      let D be non empty set;

      :: TREES_3:def8

      func FinTrees (D) -> DTree-set of D means

      : Def8: for T be DecoratedTree of D holds ( dom T) is finite iff T in it ;

      existence

      proof

        defpred X[ object] means ex T be DecoratedTree of D st $1 = T & ( dom T) is finite;

        consider X such that

         A1: x in X iff x in ( Trees D) & X[x] from XBOOLE_0:sch 1;

        set T = the finite DecoratedTree of D;

        

         A2: ( dom T) is finite;

        T in ( Trees D) by Def7;

        then

         A3: X is non empty by A1, A2;

        now

          let x;

          assume x in X;

          then x in ( Trees D) by A1;

          hence x is DecoratedTree of D;

        end;

        then

        reconsider X as DTree-set of D by A3, Def6;

        take X;

        let T be DecoratedTree of D;

        T in ( Trees D) by Def7;

        hence ( dom T) is finite implies T in X by A1;

        assume T in X;

        then ex t be DecoratedTree of D st T = t & ( dom t) is finite by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let T1,T2 be DTree-set of D such that

         A4: for T be DecoratedTree of D holds ( dom T) is finite iff T in T1 and

         A5: for T be DecoratedTree of D holds ( dom T) is finite iff T in T2;

        thus T1 c= T2

        proof

          let x be object;

          assume

           A6: x in T1;

          then

          reconsider T = x as DecoratedTree of D;

          ( dom T) is finite by A4, A6;

          hence thesis by A5;

        end;

        let x be object;

        assume

         A7: x in T2;

        then

        reconsider T = x as DecoratedTree of D;

        ( dom T) is finite by A5, A7;

        hence thesis by A4;

      end;

    end

    theorem :: TREES_3:21

    for D be non empty set holds ( FinTrees D) c= ( Trees D) by Def7;

    begin

    definition

      let IT be Function;

      :: TREES_3:def9

      attr IT is Tree-yielding means

      : Def9: ( rng IT) is constituted-Trees;

      :: TREES_3:def10

      attr IT is FinTree-yielding means

      : Def10: ( rng IT) is constituted-FinTrees;

      :: TREES_3:def11

      attr IT is DTree-yielding means ( rng IT) is constituted-DTrees;

    end

    registration

      cluster empty -> Tree-yielding FinTree-yielding DTree-yielding for Function;

      coherence ;

    end

    theorem :: TREES_3:22

    

     Th22: f is Tree-yielding iff for x st x in ( dom f) holds (f . x) is Tree

    proof

      thus f is Tree-yielding implies for x st x in ( dom f) holds (f . x) is Tree

      proof

        assume

         A1: for x st x in ( rng f) holds x is Tree;

        let x;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      assume

       A2: for x st x in ( dom f) holds (f . x) is Tree;

      let x;

      assume x in ( rng f);

      then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: TREES_3:23

    f is FinTree-yielding iff for x st x in ( dom f) holds (f . x) is finite Tree

    proof

      thus f is FinTree-yielding implies for x st x in ( dom f) holds (f . x) is finite Tree

      proof

        assume

         A1: for x st x in ( rng f) holds x is finite Tree;

        let x;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      assume

       A2: for x st x in ( dom f) holds (f . x) is finite Tree;

      let x;

      assume x in ( rng f);

      then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: TREES_3:24

    

     Th24: f is DTree-yielding iff for x st x in ( dom f) holds (f . x) is DecoratedTree

    proof

      thus f is DTree-yielding implies for x st x in ( dom f) holds (f . x) is DecoratedTree

      proof

        assume

         A1: for x st x in ( rng f) holds x is DecoratedTree;

        let x;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      assume

       A2: for x st x in ( dom f) holds (f . x) is DecoratedTree;

      let x;

      assume x in ( rng f);

      then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: TREES_3:25

    

     Th25: p is Tree-yielding & q is Tree-yielding iff (p ^ q) is Tree-yielding

    proof

      

       A1: ( rng (p ^ q)) = (( rng p) \/ ( rng q)) by FINSEQ_1: 31;

      thus p is Tree-yielding & q is Tree-yielding implies (p ^ q) is Tree-yielding by A1, Th3;

      assume

       A2: ( rng (p ^ q)) is constituted-Trees;

      hence ( rng p) is constituted-Trees by A1, Th3;

      thus ( rng q) is constituted-Trees by A1, A2, Th3;

    end;

    theorem :: TREES_3:26

    

     Th26: p is FinTree-yielding & q is FinTree-yielding iff (p ^ q) is FinTree-yielding

    proof

      

       A1: ( rng (p ^ q)) = (( rng p) \/ ( rng q)) by FINSEQ_1: 31;

      thus p is FinTree-yielding & q is FinTree-yielding implies (p ^ q) is FinTree-yielding by A1, Th6;

      assume

       A2: ( rng (p ^ q)) is constituted-FinTrees;

      hence ( rng p) is constituted-FinTrees by A1, Th6;

      thus ( rng q) is constituted-FinTrees by A1, A2, Th6;

    end;

    theorem :: TREES_3:27

    

     Th27: p is DTree-yielding & q is DTree-yielding iff (p ^ q) is DTree-yielding

    proof

      

       A1: ( rng (p ^ q)) = (( rng p) \/ ( rng q)) by FINSEQ_1: 31;

      thus p is DTree-yielding & q is DTree-yielding implies (p ^ q) is DTree-yielding by A1, Th9;

      assume

       A2: ( rng (p ^ q)) is constituted-DTrees;

      hence ( rng p) is constituted-DTrees by A1, Th9;

      thus ( rng q) is constituted-DTrees by A1, A2, Th9;

    end;

    theorem :: TREES_3:28

    

     Th28: <*x*> is Tree-yielding iff x is Tree

    proof

      

       A1: x is Tree iff {x} is constituted-Trees by Th12;

      ( rng <*x*>) = {x} by FINSEQ_1: 39;

      hence thesis by A1;

    end;

    theorem :: TREES_3:29

    

     Th29: for x be object holds <*x*> is FinTree-yielding iff x is finite Tree

    proof

      let x be object;

      

       A1: x is finite Tree iff {x} is constituted-FinTrees by Th13;

      ( rng <*x*>) = {x} by FINSEQ_1: 39;

      hence thesis by A1;

    end;

    theorem :: TREES_3:30

    

     Th30: <*x*> is DTree-yielding iff x is DecoratedTree

    proof

      

       A1: x is DecoratedTree iff {x} is constituted-DTrees by Th14;

      ( rng <*x*>) = {x} by FINSEQ_1: 39;

      hence thesis by A1;

    end;

    theorem :: TREES_3:31

    

     Th31: <*x, y*> is Tree-yielding iff x is Tree & y is Tree

    proof

      

       A1: x is Tree & y is Tree iff {x, y} is constituted-Trees by Th15;

      ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      hence thesis by A1;

    end;

    theorem :: TREES_3:32

    

     Th32: <*x, y*> is FinTree-yielding iff x is finite Tree & y is finite Tree

    proof

      

       A1: x is finite Tree & y is finite Tree iff {x, y} is constituted-FinTrees by Th16;

      ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      hence thesis by A1;

    end;

    theorem :: TREES_3:33

    

     Th33: <*x, y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree

    proof

      

       A1: x is DecoratedTree & y is DecoratedTree iff {x, y} is constituted-DTrees by Th17;

      ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      hence thesis by A1;

    end;

    theorem :: TREES_3:34

    

     Th34: i <> 0 implies ((i |-> x) is Tree-yielding iff x is Tree)

    proof

      assume

       A1: i <> 0 ;

      (i |-> x) = (( Seg i) --> x) by FINSEQ_2:def 2;

      then ( rng (i |-> x)) = {x} by A1, FUNCOP_1: 8;

      then x is Tree iff ( rng (i |-> x)) is constituted-Trees by Th12;

      hence thesis;

    end;

    theorem :: TREES_3:35

    

     Th35: i <> 0 implies ((i |-> x) is FinTree-yielding iff x is finite Tree)

    proof

      assume

       A1: i <> 0 ;

      (i |-> x) = (( Seg i) --> x) by FINSEQ_2:def 2;

      then ( rng (i |-> x)) = {x} by A1, FUNCOP_1: 8;

      then x is finite Tree iff ( rng (i |-> x)) is constituted-FinTrees by Th13;

      hence thesis;

    end;

    theorem :: TREES_3:36

    

     Th36: i <> 0 implies ((i |-> x) is DTree-yielding iff x is DecoratedTree)

    proof

      assume

       A1: i <> 0 ;

      (i |-> x) = (( Seg i) --> x) by FINSEQ_2:def 2;

      then ( rng (i |-> x)) = {x} by A1, FUNCOP_1: 8;

      then x is DecoratedTree iff ( rng (i |-> x)) is constituted-DTrees by Th14;

      hence thesis;

    end;

    registration

      cluster Tree-yielding FinTree-yielding non empty for FinSequence;

      existence

      proof

        set T = the finite Tree;

        take <*T*>;

        thus thesis by Th28, Th29;

      end;

      cluster DTree-yielding non empty for FinSequence;

      existence

      proof

        set T = the DecoratedTree;

        take <*T*>;

        thus thesis by Th30;

      end;

    end

    registration

      cluster Tree-yielding FinTree-yielding non empty for Function;

      existence

      proof

        set p = the Tree-yielding FinTree-yielding non empty FinSequence;

        take p;

        thus thesis;

      end;

      cluster DTree-yielding non empty for Function;

      existence

      proof

        set p = the DTree-yielding non empty FinSequence;

        take p;

        thus thesis;

      end;

    end

    registration

      cluster FinTree-yielding -> Tree-yielding for Function;

      coherence ;

    end

    registration

      let D be constituted-Trees non empty set;

      cluster -> Tree-yielding for FinSequence of D;

      coherence

      proof

        let p be FinSequence of D;

        let x;

        ( rng p) c= D;

        hence thesis;

      end;

    end

    registration

      let p,q be Tree-yielding FinSequence;

      cluster (p ^ q) -> Tree-yielding;

      coherence by Th25;

    end

    registration

      let D be constituted-FinTrees non empty set;

      cluster -> FinTree-yielding for FinSequence of D;

      coherence

      proof

        let p be FinSequence of D;

        let x;

        ( rng p) c= D;

        hence thesis;

      end;

    end

    registration

      let p,q be FinTree-yielding FinSequence;

      cluster (p ^ q) -> FinTree-yielding;

      coherence by Th26;

    end

    registration

      let D be constituted-DTrees non empty set;

      cluster -> DTree-yielding for FinSequence of D;

      coherence

      proof

        let p be FinSequence of D;

        let x;

        ( rng p) c= D;

        hence thesis;

      end;

    end

    registration

      let p,q be DTree-yielding FinSequence;

      cluster (p ^ q) -> DTree-yielding;

      coherence by Th27;

    end

    registration

      let T be Tree;

      cluster <*T*> -> Tree-yielding non empty;

      coherence by Th28;

      let S be Tree;

      cluster <*T, S*> -> Tree-yielding non empty;

      coherence by Th31;

    end

    registration

      let n be Nat, T be Tree;

      cluster (n |-> T) -> Tree-yielding;

      coherence

      proof

        ( 0 |-> T) = {} ;

        hence thesis by Th34;

      end;

    end

    registration

      let T be finite Tree;

      cluster <*T*> -> FinTree-yielding;

      coherence by Th29;

      let S be finite Tree;

      cluster <*T, S*> -> FinTree-yielding;

      coherence by Th32;

    end

    registration

      let n be Nat, T be finite Tree;

      cluster (n |-> T) -> FinTree-yielding;

      coherence

      proof

        ( 0 |-> T) = {} ;

        hence thesis by Th35;

      end;

    end

    registration

      let T be DecoratedTree;

      cluster <*T*> -> DTree-yielding non empty;

      coherence by Th30;

      let S be DecoratedTree;

      cluster <*T, S*> -> DTree-yielding non empty;

      coherence by Th33;

    end

    registration

      let n be Nat, T be DecoratedTree;

      cluster (n |-> T) -> DTree-yielding;

      coherence

      proof

        ( 0 |-> T) = {} ;

        hence thesis by Th36;

      end;

    end

    registration

      cluster DTree-yielding -> Function-yielding for Function;

      coherence

      proof

        let f be Function;

        assume

         A1: ( rng f) is constituted-DTrees;

        let x be object;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1: 3;

        then (f . x) is DecoratedTree by A1;

        hence (f . x) is Function;

      end;

    end

    theorem :: TREES_3:37

    

     Th37: for f be DTree-yielding Function holds ( dom ( doms f)) = ( dom f) & ( doms f) is Tree-yielding

    proof

      let f be DTree-yielding Function;

      

       A1: ( dom ( doms f)) = ( dom f) by FUNCT_6:def 2;

      hence ( dom ( doms f)) c= ( dom f);

      thus ( dom f) c= ( dom ( doms f)) by A1;

      now

        let x;

        assume x in ( dom ( doms f));

        then

         A2: x in ( dom f) by A1;

        then

        reconsider g = (f . x) as DecoratedTree by Th24;

        (( doms f) . x) = ( dom g) by A2, FUNCT_6: 22;

        hence (( doms f) . x) is Tree;

      end;

      hence thesis by Th22;

    end;

    registration

      let p be DTree-yielding FinSequence;

      cluster ( doms p) -> Tree-yielding FinSequence-like;

      coherence

      proof

        

         A1: ( dom ( doms p)) = ( dom p) by Th37;

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

        hence thesis by A1, Th37, FINSEQ_1:def 2;

      end;

    end

    theorem :: TREES_3:38

    for p be DTree-yielding FinSequence holds ( len ( doms p)) = ( len p)

    proof

      let p be DTree-yielding FinSequence;

      

       A1: ( dom p) = ( dom ( doms p)) by Th37;

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

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    

     Lm2: for D be non empty set, T be DecoratedTree of D holds T is Function of ( dom T), D

    proof

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

      ( rng T) c= D;

      hence thesis by FUNCT_2:def 1, RELSET_1: 4;

    end;

    begin

    definition

      let D,E be non empty set;

      mode DecoratedTree of D,E is DecoratedTree of [:D, E:];

      mode DTree-set of D,E is DTree-set of [:D, E:];

    end

    registration

      let T1,T2 be DecoratedTree;

      cluster <:T1, T2:> -> DecoratedTree-like;

      coherence

      proof

        ( dom <:T1, T2:>) = (( dom T1) /\ ( dom T2)) by FUNCT_3:def 7;

        hence thesis;

      end;

    end

    registration

      let D1,D2 be non empty set;

      let T1 be DecoratedTree of D1;

      let T2 be DecoratedTree of D2;

      cluster <:T1, T2:> -> [:D1, D2:] -valued;

      coherence

      proof

        

         A1: ( rng <:T1, T2:>) c= [:( rng T1), ( rng T2):] by FUNCT_3: 51;

         [:( rng T1), ( rng T2):] c= [:D1, D2:] by ZFMISC_1: 96;

        then ( rng <:T1, T2:>) c= [:D1, D2:] by A1;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

      let D,E be non empty set;

      let T be DecoratedTree of D;

      let f be Function of D, E;

      cluster (f * T) -> DecoratedTree-like;

      coherence

      proof

        reconsider g = T as Function of ( dom T), D by Lm2;

        reconsider fg = (f * g) as Function of ( dom T), E;

        ( rng fg) c= E;

        hence thesis;

      end;

    end

    definition

      let D1,D2 be non empty set;

      :: original: pr1

      redefine

      func pr1 (D1,D2) -> Function of [:D1, D2:], D1 ;

      coherence

      proof

        thus ( pr1 (D1,D2)) is Function of [:D1, D2:], D1;

      end;

      :: original: pr2

      redefine

      func pr2 (D1,D2) -> Function of [:D1, D2:], D2 ;

      coherence

      proof

        thus ( pr2 (D1,D2)) is Function of [:D1, D2:], D2;

      end;

    end

    definition

      let D1,D2 be non empty set, T be DecoratedTree of D1, D2;

      :: TREES_3:def12

      func T `1 -> DecoratedTree of D1 equals (( pr1 (D1,D2)) * T);

      correctness ;

      :: TREES_3:def13

      func T `2 -> DecoratedTree of D2 equals (( pr2 (D1,D2)) * T);

      correctness ;

    end

    theorem :: TREES_3:39

    

     Th39: for D1,D2 be non empty set, T be DecoratedTree of D1, D2, t be Element of ( dom T) holds ((T . t) `1 ) = ((T `1 ) . t) & ((T `2 ) . t) = ((T . t) `2 )

    proof

      let D1,D2 be non empty set, T be DecoratedTree of D1, D2;

      let t be Element of ( dom T);

      

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

      

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

      

       A3: ( rng T) c= [:D1, D2:];

      then

       A4: ( dom (T `1 )) = ( dom T) by A1, RELAT_1: 27;

      

       A5: ( dom (T `2 )) = ( dom T) by A2, A3, RELAT_1: 27;

      

       A6: (T . t) = [((T . t) `1 ), ((T . t) `2 )] by MCART_1: 21;

      then

       A7: ((T `1 ) . t) = (( pr1 (D1,D2)) . (((T . t) `1 ),((T . t) `2 ))) by A4, FUNCT_1: 12;

      ((T `2 ) . t) = (( pr2 (D1,D2)) . (((T . t) `1 ),((T . t) `2 ))) by A5, A6, FUNCT_1: 12;

      hence thesis by A7, FUNCT_3:def 4, FUNCT_3:def 5;

    end;

    theorem :: TREES_3:40

    for D1,D2 be non empty set, T be DecoratedTree of D1, D2 holds <:(T `1 ), (T `2 ):> = T

    proof

      let D1,D2 be non empty set, T be DecoratedTree of D1, D2;

      

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

      

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

      

       A3: ( rng T) c= [:D1, D2:];

      then

       A4: ( dom (T `1 )) = ( dom T) by A1, RELAT_1: 27;

      

       A5: ( dom (T `2 )) = ( dom T) by A2, A3, RELAT_1: 27;

      then

       A6: ( dom <:(T `1 ), (T `2 ):>) = ( dom T) by A4, FUNCT_3: 50;

      now

        let x be object;

        assume x in ( dom T);

        then

        reconsider t = x as Element of ( dom T);

        

        thus ( <:(T `1 ), (T `2 ):> . x) = [((T `1 ) . t), ((T `2 ) . t)] by A4, A5, FUNCT_3: 49

        .= [((T . t) `1 ), ((T `2 ) . t)] by Th39

        .= [((T . t) `1 ), ((T . t) `2 )] by Th39

        .= (T . x) by MCART_1: 21;

      end;

      hence thesis by A6;

    end;

    registration

      let T be finite Tree;

      cluster ( Leaves T) -> finite non empty;

      coherence

      proof

        

         A1: T <> {} ;

        defpred X[ object, object] means ex t1,t2 be Element of T st $1 = t1 & $2 = t2 & t2 is_a_prefix_of t1;

        

         A2: for x, y st X[x, y] & X[y, x] holds x = y by XBOOLE_0:def 10;

        

         A3: for x, y, z st X[x, y] & X[y, z] holds X[x, z] by XBOOLE_1: 1;

        consider x such that

         A4: x in T & for y st y in T & y <> x holds not X[y, x] from CARD_2:sch 1( A1, A2, A3);

        reconsider x as Element of T by A4;

        now

          let p be FinSequence of NAT ;

          assume p in T;

          then

          reconsider t1 = p as Element of T;

          thus not x is_a_proper_prefix_of p

          proof

            assume x is_a_prefix_of p;

            then x = t1 by A4;

            hence thesis;

          end;

        end;

        hence thesis by TREES_1:def 5;

      end;

    end

    definition

      let T be Tree, S be non empty Subset of T;

      :: original: Element

      redefine

      mode Element of S -> Element of T ;

      coherence

      proof

        let t be Element of S;

        thus thesis;

      end;

    end

    definition

      let T be finite Tree;

      :: original: Leaf

      redefine

      mode Leaf of T -> Element of ( Leaves T) ;

      coherence by TREES_1:def 7;

    end

    definition

      let T be finite Tree;

      :: TREES_3:def14

      mode T-Substitution of T -> Tree means

      : Def14: for t be Element of it holds t in T or ex l be Leaf of T st l is_a_proper_prefix_of t;

      existence

      proof

        take T;

        thus thesis;

      end;

    end

    definition

      let T be finite Tree, t be Leaf of T, S be Tree;

      :: original: with-replacement

      redefine

      func T with-replacement (t,S) -> T-Substitution of T ;

      coherence

      proof

        let s be Element of (T with-replacement (t,S));

        assume

         A1: not s in T;

        then

        consider t1 be FinSequence of NAT such that t1 in S and

         A2: s = (t ^ t1) by TREES_1:def 9;

        take t;

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

        then t1 <> {} by A1, A2;

        hence thesis by A2, TREES_1: 10;

      end;

    end

    registration

      let T be finite Tree;

      cluster finite for T-Substitution of T;

      existence

      proof

        for t be Element of T holds t in T or ex l be Leaf of T st l is_a_proper_prefix_of t;

        then T is T-Substitution of T by Def14;

        hence thesis;

      end;

    end

    definition

      let n;

      mode T-Substitution of n is T-Substitution of ( elementary_tree n);

    end

    theorem :: TREES_3:41

    for T be Tree holds T is T-Substitution of 0

    proof

      let T be Tree;

      let t be Element of T;

      assume

       A1: not t in ( elementary_tree 0 );

      set l = the Leaf of ( elementary_tree 0 );

      take l;

      

       A2: l = {} by TARSKI:def 1, TREES_1: 29;

      

       A3: t <> {} by A1, TARSKI:def 1, TREES_1: 29;

       {} is_a_prefix_of t;

      hence thesis by A2, A3;

    end;

    theorem :: TREES_3:42

    for T1,T2 be Tree st (T1 -level 1) c= (T2 -level 1) & for n be Element of NAT st <*n*> in T1 holds (T1 | <*n*>) = (T2 | <*n*>) holds T1 c= T2

    proof

      let T1,T2 be Tree;

      assume that

       A1: (T1 -level 1) c= (T2 -level 1) and

       A2: for n be Element of NAT st <*n*> in T1 holds (T1 | <*n*>) = (T2 | <*n*>);

      let x be object;

      assume x in T1;

      then

      reconsider t = x as Element of T1;

      now

        assume t <> {} ;

        then

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

         A3: t = ( <*n*> ^ p) by FINSEQ_2: 130;

        

         A4: ( len <*n*>) = 1 by FINSEQ_1: 39;

        reconsider n as Element of NAT ;

        reconsider q = <*n*> as Element of T1 by A3, TREES_1: 21;

        

         A5: q in (T1 -level 1) by A4;

        then

         A6: q in (T2 -level 1) by A1;

        

         A7: p in (T1 | q) by A3, TREES_1:def 6;

        (T1 | <*n*>) = (T2 | <*n*>) by A2, A5;

        hence t in T2 by A3, A6, A7, TREES_1:def 6;

      end;

      hence thesis by TREES_1: 22;

    end;

    

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

    proof

      assume

       A1: n < ( len p);

      

       A2: (n + 1) >= ( 0 + 1) by NAT_1: 13;

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

    begin

    theorem :: TREES_3:43

    for T,T9 be Tree, p be FinSequence of NAT st p in ( Leaves T) holds T c= (T with-replacement (p,T9))

    proof

      let T,T9 be Tree, p be FinSequence of NAT such that

       A1: p in ( Leaves T);

      let x be object;

      assume x in T;

      then

      reconsider t = x as Element of T;

       not p is_a_proper_prefix_of t by A1, TREES_1:def 5;

      hence thesis by A1, TREES_1:def 9;

    end;

    theorem :: TREES_3:44

    for T,T9 be DecoratedTree, p be Element of ( dom T) holds ((T with-replacement (p,T9)) . p) = (T9 . {} )

    proof

      let T,T9 be DecoratedTree, p be Element of ( dom T);

      p in (( dom T) with-replacement (p,( dom T9))) by TREES_1:def 9;

      then

       A1: ex r be FinSequence of NAT st (r in ( dom T9)) & (p = (p ^ r)) & (((T with-replacement (p,T9)) . p) = (T9 . r)) by TREES_2:def 11;

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

      hence thesis by A1, FINSEQ_1: 33;

    end;

    theorem :: TREES_3:45

    for T,T9 be DecoratedTree, p,q be Element of ( dom T) st not p is_a_prefix_of q holds ((T with-replacement (p,T9)) . q) = (T . q)

    proof

      let T,T9 be DecoratedTree, p,q be Element of ( dom T);

      assume

       A1: not p is_a_prefix_of q;

      then

       A2: q in (( dom T) with-replacement (p,( dom T9))) by TREES_2: 7;

       not ex r be FinSequence of NAT st r in ( dom T9) & q = (p ^ r) & ((T with-replacement (p,T9)) . q) = (T9 . r) by A1, TREES_1: 1;

      hence thesis by A2, TREES_2:def 11;

    end;

    theorem :: TREES_3:46

    for T,T9 be DecoratedTree, p be Element of ( dom T), q be Element of ( dom T9) holds ((T with-replacement (p,T9)) . (p ^ q)) = (T9 . q)

    proof

      let T,T9 be DecoratedTree;

      let p be Element of ( dom T), q be Element of ( dom T9);

      

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

      (p ^ q) in (( dom T) with-replacement (p,( dom T9))) by TREES_1:def 9;

      then ex r be FinSequence of NAT st (r in ( dom T9)) & ((p ^ q) = (p ^ r)) & (((T with-replacement (p,T9)) . (p ^ q)) = (T9 . r)) by A1, TREES_2:def 11;

      hence thesis by FINSEQ_1: 33;

    end;

    registration

      let T1,T2 be Tree;

      cluster (T1 \/ T2) -> non empty Tree-like;

      coherence ;

    end

    theorem :: TREES_3:47

    

     Th47: for T1,T2 be Tree, p be Element of (T1 \/ T2) holds (p in T1 & p in T2 implies ((T1 \/ T2) | p) = ((T1 | p) \/ (T2 | p))) & ( not p in T1 implies ((T1 \/ T2) | p) = (T2 | p)) & ( not p in T2 implies ((T1 \/ T2) | p) = (T1 | p))

    proof

      let T1,T2 be Tree, p be Element of (T1 \/ T2);

      thus p in T1 & p in T2 implies ((T1 \/ T2) | p) = ((T1 | p) \/ (T2 | p))

      proof

        assume that

         A1: p in T1 and

         A2: p in T2;

        let q be FinSequence of NAT ;

        thus q in ((T1 \/ T2) | p) implies q in ((T1 | p) \/ (T2 | p))

        proof

          assume q in ((T1 \/ T2) | p);

          then (p ^ q) in (T1 \/ T2) by TREES_1:def 6;

          then (p ^ q) in T1 or (p ^ q) in T2 by XBOOLE_0:def 3;

          then q in (T1 | p) or q in (T2 | p) by A1, A2, TREES_1:def 6;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume q in ((T1 | p) \/ (T2 | p));

        then q in (T1 | p) or q in (T2 | p) by XBOOLE_0:def 3;

        then (p ^ q) in T1 or (p ^ q) in T2 by A1, A2, TREES_1:def 6;

        then (p ^ q) in (T1 \/ T2) by XBOOLE_0:def 3;

        hence thesis by TREES_1:def 6;

      end;

      for T1,T2 be Tree, p be Element of (T1 \/ T2) st not p in T1 holds ((T1 \/ T2) | p) = (T2 | p)

      proof

        let T1,T2 be Tree;

        let p be Element of (T1 \/ T2);

        assume

         A3: not p in T1;

        then

         A4: p in T2 by XBOOLE_0:def 3;

        let q be FinSequence of NAT ;

        thus q in ((T1 \/ T2) | p) implies q in (T2 | p)

        proof

          assume q in ((T1 \/ T2) | p);

          then (p ^ q) in (T1 \/ T2) by TREES_1:def 6;

          then (p ^ q) in T1 or (p ^ q) in T2 by XBOOLE_0:def 3;

          hence thesis by A3, A4, TREES_1: 21, TREES_1:def 6;

        end;

        assume q in (T2 | p);

        then (p ^ q) in T2 by A4, TREES_1:def 6;

        then (p ^ q) in (T1 \/ T2) by XBOOLE_0:def 3;

        hence thesis by TREES_1:def 6;

      end;

      hence thesis;

    end;

    definition

      let p;

      :: TREES_3:def15

      func tree p -> Tree means

      : Def15: x in it iff x = {} or ex n, q st n < ( len p) & q in (p . (n + 1)) & x = ( <*n*> ^ q);

      existence

      proof

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

        consider T be set such that

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

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

        then

        reconsider T as non empty set by A2;

        

         A3: ( rng p) is constituted-Trees by A1;

        then

         A4: for n st n < ( len p) holds (p . (n + 1)) is Tree by Lm3;

        T is Tree-like

        proof

          thus T c= ( NAT * ) by A2;

          thus w in T implies ( ProperPrefixes w) c= T

          proof

            assume

             A5: w in T;

            now

              assume w <> {} ;

              then

              consider n, q such that

               A6: n < ( len p) and

               A7: q in (p . (n + 1)) and

               A8: w = ( <*n*> ^ q) by A2, A5;

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

              thus thesis

              proof

                let x be object;

                assume x in ( ProperPrefixes w);

                then

                consider r such that

                 A9: x = r and

                 A10: r is_a_proper_prefix_of w by TREES_1:def 2;

                r is_a_prefix_of w by A10;

                then

                consider k such that

                 A11: r = (w | ( Seg k));

                ( rng r) = (w .: ( Seg k)) by A11, RELAT_1: 115;

                then

                reconsider r as FinSequence of NAT by FINSEQ_1:def 4;

                

                 A12: r in ( NAT * ) by FINSEQ_1:def 11;

                now

                  assume r <> {} ;

                  then

                  consider r1 be FinSequence of NAT , i be Element of NAT such that

                   A13: r = ( <*i*> ^ r1) by FINSEQ_2: 130;

                  

                   A14: ( dom <*i*>) = ( Seg 1) by FINSEQ_1: 38;

                  

                   A15: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

                  

                   A16: ( Seg 1) c= ( dom r) by A13, A14, FINSEQ_1: 26;

                  

                   A17: (r . 1) = i by A13, FINSEQ_1: 41;

                  

                   A18: (w . 1) = n by A8, FINSEQ_1: 41;

                  

                   A19: (r . 1) = (w . 1) by A11, A15, A16, FUNCT_1: 47;

                  then

                   A20: r1 is_a_proper_prefix_of q by A8, A10, A13, A17, A18, TREES_1: 49;

                  

                   A21: (p . (n + 1)) is Tree by A4, A6;

                  r1 is_a_prefix_of q by A20;

                  then r1 in (p . (n + 1)) by A7, A21, TREES_1: 20;

                  hence thesis by A2, A6, A9, A12, A13, A17, A18, A19;

                end;

                hence thesis by A2, A9, A12;

              end;

            end;

            hence thesis by TREES_1: 15;

          end;

          let w, k, n such that

           A22: (w ^ <*k*>) in T and

           A23: n <= k;

           A24:

          now

            assume

             A25: w = {} ;

            then <*k*> in T by A22, FINSEQ_1: 34;

            then

            consider m be Nat, q such that

             A26: m < ( len p) and q in (p . (m + 1)) and

             A27: <*k*> = ( <*m*> ^ q) by A2;

            

             A28: ( <*k*> . 1) = k by FINSEQ_1:def 8;

            (( <*m*> ^ q) . 1) = m by FINSEQ_1: 41;

            then

             A29: n < ( len p) by A23, A26, A27, A28, XXREAL_0: 2;

            then (p . (n + 1)) in ( rng p) by Lm3;

            then

             A30: {} in (p . (n + 1)) by A3, TREES_1: 22;

            

             A31: ( <*n*> ^ {} ) = <*n*> by FINSEQ_1: 34;

            

             A32: ( {} ^ <*n*>) = <*n*> by FINSEQ_1: 34;

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

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

            hence thesis by A2, A25, A29, A30, A31, A32;

          end;

          now

            assume w <> {} ;

            then

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

             A33: w = ( <*m*> ^ q) by FINSEQ_2: 130;

            consider m9 be Nat, r such that

             A34: m9 < ( len p) and

             A35: r in (p . (m9 + 1)) and

             A36: (w ^ <*k*>) = ( <*m9*> ^ r) by A2, A22;

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

            

             A37: (w ^ <*k*>) = ( <*m*> ^ (q ^ <*k*>)) by A33, FINSEQ_1: 32;

            

             A38: (w ^ <*n*>) = ( <*m*> ^ (q ^ <*n*>)) by A33, FINSEQ_1: 32;

            

             A39: ((w ^ <*k*>) . 1) = m by A37, FINSEQ_1: 41;

            

             A40: ((w ^ <*k*>) . 1) = m9 by A36, FINSEQ_1: 41;

            

             A41: ( <*m*> ^ (q ^ <*n*>)) in ( NAT * ) by FINSEQ_1:def 11;

            

             A42: r = (q ^ <*k*>) by A36, A37, A39, A40, FINSEQ_1: 33;

            (p . (m + 1)) in ( rng p) by A34, A39, A40, Lm3;

            then (q ^ <*n*>) in (p . (m + 1)) by A3, A23, A35, A39, A40, A42, TREES_1:def 3;

            hence thesis by A2, A34, A38, A39, A40, A41;

          end;

          hence thesis by A24;

        end;

        then

        reconsider T as Tree;

        take T;

        let x;

        thus x in T implies x = {} or ex n, q st n < ( len p) & q in (p . (n + 1)) & x = ( <*n*> ^ q) by A2;

        assume

         A43: x = {} or ex n, q st n < ( len p) & q in (p . (n + 1)) & x = ( <*n*> ^ q);

         A44:

        now

          given n, q such that

           A45: n < ( len p) and

           A46: q in (p . (n + 1)) and

           A47: x = ( <*n*> ^ q);

          reconsider T1 = (p . (n + 1)) as Tree by A4, A45;

          reconsider q as Element of T1 by A46;

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

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

          hence x in ( NAT * ) by A47;

        end;

         {} in ( NAT * ) by FINSEQ_1: 49;

        hence thesis by A2, A43, A44;

      end;

      uniqueness

      proof

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

        let T1,T2 be Tree such that

         A48: x in T1 iff X[x] and

         A49: x in T2 iff X[x];

        thus thesis from XBOOLE_0:sch 2( A48, A49);

      end;

    end

    definition

      let T be Tree;

      :: TREES_3:def16

      func ^ T -> Tree equals ( tree <*T*>);

      correctness ;

    end

    definition

      let T1,T2 be Tree;

      :: TREES_3:def17

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

      correctness ;

    end

    theorem :: TREES_3:48

    p is Tree-yielding implies (( <*n*> ^ q) in ( tree p) iff n < ( len p) & q in (p . (n + 1)))

    proof

      assume

       A1: p is Tree-yielding;

      thus ( <*n*> ^ q) in ( tree p) implies n < ( len p) & q in (p . (n + 1))

      proof

        assume ( <*n*> ^ q) in ( tree p);

        then

        consider k, r such that

         A2: k < ( len p) and

         A3: r in (p . (k + 1)) and

         A4: ( <*n*> ^ q) = ( <*k*> ^ r) by A1, Def15;

        

         A5: (( <*n*> ^ q) . 1) = n by FINSEQ_1: 41;

        (( <*k*> ^ r) . 1) = k by FINSEQ_1: 41;

        hence thesis by A2, A3, A4, A5, FINSEQ_1: 33;

      end;

      thus thesis by A1, Def15;

    end;

    theorem :: TREES_3:49

    

     Th49: p is Tree-yielding implies (( tree p) -level 1) = { <*n*> : n < ( len p) } & for n be Element of NAT st n < ( len p) holds (( tree p) | <*n*>) = (p . (n + 1))

    proof

      set T = ( tree p);

      assume

       A1: p is Tree-yielding;

      then

       A2: ( rng p) is constituted-Trees;

      thus (T -level 1) = { <*n*> : n < ( len p) }

      proof

        thus (T -level 1) c= { <*n*> : n < ( len p) }

        proof

          let x be object;

          assume x in (T -level 1);

          then

          consider t be Element of T such that

           A3: x = t and

           A4: ( len t) = 1;

          

           A5: t = <*(t . 1)*> by A4, FINSEQ_1: 40;

          then

          consider n, q such that

           A6: n < ( len p) and q in (p . (n + 1)) and

           A7: t = ( <*n*> ^ q) by A1, Def15;

          t = <*n*> by A5, A7, FINSEQ_1: 88;

          hence thesis by A3, A6;

        end;

        let x be object;

        assume x in { <*n*> : n < ( len p) };

        then

        consider n such that

         A8: x = <*n*> and

         A9: n < ( len p);

        (p . (n + 1)) in ( rng p) by A9, Lm3;

        then

         A10: {} in (p . (n + 1)) by A2, TREES_1: 22;

        ( <*n*> ^ {} ) = <*n*> by FINSEQ_1: 34;

        then

        reconsider t = <*n*> as Element of T by A1, A9, A10, Def15;

        ( len t) = 1 by FINSEQ_1: 39;

        hence thesis by A8;

      end;

      let n be Element of NAT ;

      assume

       A11: n < ( len p);

      then (p . (n + 1)) in ( rng p) by Lm3;

      then

      reconsider S = (p . (n + 1)) as Tree by A2;

      

       A12: {} in S by TREES_1: 22;

      ( <*n*> ^ {} ) = <*n*> by FINSEQ_1: 34;

      then

       A13: <*n*> in T by A1, A11, A12, Def15;

      (T | <*n*>) = S

      proof

        let r be FinSequence of NAT ;

        thus r in (T | <*n*>) implies r in S

        proof

          assume r in (T | <*n*>);

          then ( <*n*> ^ r) in T by A13, TREES_1:def 6;

          then

          consider m be Nat, q such that m < ( len p) and

           A14: q in (p . (m + 1)) and

           A15: ( <*n*> ^ r) = ( <*m*> ^ q) by A1, Def15;

          

           A16: (( <*n*> ^ r) . 1) = n by FINSEQ_1: 41;

          (( <*m*> ^ q) . 1) = m by FINSEQ_1: 41;

          hence thesis by A14, A15, A16, FINSEQ_1: 33;

        end;

        assume r in S;

        then

         A17: ( <*n*> ^ r) in T by A1, A11, Def15;

        then <*n*> in T by TREES_1: 21;

        hence thesis by A17, TREES_1:def 6;

      end;

      hence thesis;

    end;

    theorem :: TREES_3:50

    for p,q be Tree-yielding FinSequence st ( tree p) = ( tree q) holds p = q

    proof

      let p,q be Tree-yielding FinSequence such that

       A1: ( tree p) = ( tree q);

      

       A2: (( tree p) -level 1) = { <*n*> : n < ( len p) } by Th49;

      

       A3: (( tree q) -level 1) = { <*k*> : k < ( len q) } by Th49;

       A4:

      now

        let n1,n2 be Element of NAT ;

        assume { <*i*> : i < n1 } = { <*k*> : k < n2 } & n1 < n2;

        then <*n1*> in { <*i*> : i < n1 };

        then

         A5: ex i st ( <*n1*> = <*i*>) & (i < n1);

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

        hence contradiction by A5, FINSEQ_1: 40;

      end;

      then

       A6: not ( len p) < ( len q) by A1, A2, A3;

      

       A7: not ( len p) > ( len q) by A1, A2, A3, A4;

      then

       A8: ( len p) = ( len q) by A6, XXREAL_0: 1;

      now

        let i be Nat;

        assume that

         A9: i >= 1 and

         A10: i <= ( len p);

        consider k be Nat such that

         A11: i = (1 + k) by A9, NAT_1: 10;

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

        

         A12: k < ( len p) by A10, A11, NAT_1: 13;

        then (p . i) = (( tree p) | <*k*>) by A11, Th49;

        hence (p . i) = (q . i) by A1, A8, A11, A12, Th49;

      end;

      hence thesis by A6, A7, FINSEQ_1: 14, XXREAL_0: 1;

    end;

    theorem :: TREES_3:51

    

     Th51: for p1,p2 be Tree-yielding FinSequence, T be Tree holds p in T iff ( <*( len p1)*> ^ p) in ( tree ((p1 ^ <*T*>) ^ p2))

    proof

      let p1,p2 be Tree-yielding FinSequence, T be Tree;

      

       A1: ( len ((p1 ^ <*T*>) ^ p2)) = (( len (p1 ^ <*T*>)) + ( len p2)) by FINSEQ_1: 22;

      

       A2: ( len (p1 ^ <*T*>)) = (( len p1) + ( len <*T*>)) by FINSEQ_1: 22;

      

       A3: ( len <*T*>) = 1 by FINSEQ_1: 40;

      

       A4: ((( len p1) + 1) + ( len p2)) = ((( len p1) + ( len p2)) + 1);

      ( len p1) <= (( len p1) + ( len p2)) by NAT_1: 11;

      then

       A5: ( len p1) < ( len ((p1 ^ <*T*>) ^ p2)) by A1, A2, A3, A4, NAT_1: 13;

      (( len p1) + 1) >= 1 by NAT_1: 11;

      then (( len p1) + 1) in ( dom (p1 ^ <*T*>)) by A2, A3, FINSEQ_3: 25;

      

      then

       A6: (((p1 ^ <*T*>) ^ p2) . (( len p1) + 1)) = ((p1 ^ <*T*>) . (( len p1) + 1)) by FINSEQ_1:def 7

      .= T by FINSEQ_1: 42;

      hence p in T implies ( <*( len p1)*> ^ p) in ( tree ((p1 ^ <*T*>) ^ p2)) by A5, Def15;

      assume ( <*( len p1)*> ^ p) in ( tree ((p1 ^ <*T*>) ^ p2));

      then

      consider n, q such that n < ( len ((p1 ^ <*T*>) ^ p2)) and

       A7: q in (((p1 ^ <*T*>) ^ p2) . (n + 1)) and

       A8: ( <*( len p1)*> ^ p) = ( <*n*> ^ q) by Def15;

      

       A9: (( <*( len p1)*> ^ p) . 1) = ( len p1) by FINSEQ_1: 41;

      (( <*n*> ^ q) . 1) = n by FINSEQ_1: 41;

      hence thesis by A6, A7, A8, A9, FINSEQ_1: 33;

    end;

    theorem :: TREES_3:52

    

     Th52: ( tree {} ) = ( elementary_tree 0 )

    proof

      let p be FinSequence of NAT ;

      thus p in ( tree {} ) implies p in ( elementary_tree 0 )

      proof

        assume p in ( tree {} );

        then

         A1: p = {} or ex n, q st n < ( len {} ) & q in ( {} . (n + 1)) & p = ( <*n*> ^ q) by Def15;

        assume not thesis;

        hence contradiction by A1, TARSKI:def 1, TREES_1: 29;

      end;

      assume p in ( elementary_tree 0 );

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

      hence thesis by Def15;

    end;

    theorem :: TREES_3:53

    

     Th53: p is Tree-yielding implies ( elementary_tree ( len p)) c= ( tree p)

    proof

      assume

       A1: p is Tree-yielding;

      then

       A2: ( rng p) is constituted-Trees;

      let q be object;

      assume q in ( elementary_tree ( len p));

      then q in { <*n*> : n < ( len p) } or q in { {} } by XBOOLE_0:def 3;

      then

       A3: (ex n st q = <*n*> & n < ( len p)) or q = {} by TARSKI:def 1;

      assume

       A4: not thesis;

      then

      consider n such that

       A5: q = <*n*> and

       A6: n < ( len p) by A3, TREES_1: 22;

      (p . (n + 1)) in ( rng p) by A6, Lm3;

      then

      reconsider t = (p . (n + 1)) as Tree by A2;

      

       A7: {} in t by TREES_1: 22;

      ( <*n*> ^ {} ) = q by A5, FINSEQ_1: 34;

      hence thesis by A1, A4, A6, A7, Def15;

    end;

    theorem :: TREES_3:54

    

     Th54: ( elementary_tree i) = ( tree (i |-> ( elementary_tree 0 )))

    proof

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

      let q be FinSequence of NAT ;

      

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

      then ( elementary_tree i) c= ( tree p) by Th53;

      hence q in ( elementary_tree i) implies q in ( tree p);

      assume q in ( tree p);

      then

       A2: q = {} or ex n, r st n < ( len p) & r in (p . (n + 1)) & q = ( <*n*> ^ r) by Def15;

      now

        given n, r such that

         A3: n < ( len p) and

         A4: r in (p . (n + 1)) and

         A5: q = ( <*n*> ^ r);

        p = (( Seg i) --> ( elementary_tree 0 )) by FINSEQ_2:def 2;

        then

         A6: ( rng p) c= {( elementary_tree 0 )} by FUNCOP_1: 13;

        (p . (n + 1)) in ( rng p) by A3, Lm3;

        then (p . (n + 1)) = ( elementary_tree 0 ) by A6, TARSKI:def 1;

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

        then q = <*n*> by A5, FINSEQ_1: 34;

        hence thesis by A1, A3, TREES_1: 28;

      end;

      hence thesis by A2, TREES_1: 22;

    end;

    theorem :: TREES_3:55

    

     Th55: for T be Tree, p be Tree-yielding FinSequence holds ( tree (p ^ <*T*>)) = ((( tree p) \/ ( elementary_tree (( len p) + 1))) with-replacement ( <*( len p)*>,T))

    proof

      let T be Tree, p be Tree-yielding FinSequence;

      set W1 = ( elementary_tree (( len p) + 1)), W2 = (( tree p) \/ W1), W = (W2 with-replacement ( <*( len p)*>,T));

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

      then

       A1: ( len (p ^ <*T*>)) = (( len p) + 1) by FINSEQ_1: 22;

      ( len p) < (( len p) + 1) by NAT_1: 13;

      then <*( len p)*> in W1 by TREES_1: 28;

      then

       A2: <*( len p)*> in W2 by XBOOLE_0:def 3;

      let q be FinSequence of NAT ;

      thus q in ( tree (p ^ <*T*>)) implies q in W

      proof

        assume q in ( tree (p ^ <*T*>));

        then

         A3: q = {} or ex n, r st n < ( len (p ^ <*T*>)) & r in ((p ^ <*T*>) . (n + 1)) & q = ( <*n*> ^ r) by Def15;

        now

          given n, r such that

           A4: n < ( len (p ^ <*T*>)) and

           A5: r in ((p ^ <*T*>) . (n + 1)) and

           A6: q = ( <*n*> ^ r);

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

          

           A7: n <= ( len p) by A1, A4, NAT_1: 13;

           A8:

          now

            assume

             A9: n < ( len p);

            then (n + 1) in ( dom p) by Lm3;

            then ((p ^ <*T*>) . (n + 1)) = (p . (n + 1)) by FINSEQ_1:def 7;

            then q in ( tree p) by A5, A6, A9, Def15;

            then

             A10: q in W2 by XBOOLE_0:def 3;

             not <*( len p)*> is_a_prefix_of ( <*n*> ^ r) by A9, TREES_1: 50;

            then not <*( len p)*> is_a_proper_prefix_of ( <*n*> ^ r);

            hence thesis by A2, A6, A10, TREES_1:def 9;

          end;

          now

            assume

             A11: n = ( len p);

            then

             A12: ((p ^ <*T*>) . (n + 1)) = T by FINSEQ_1: 42;

            r = r;

            hence thesis by A2, A5, A6, A11, A12, TREES_1:def 9;

          end;

          hence thesis by A7, A8, XXREAL_0: 1;

        end;

        hence thesis by A3, TREES_1: 22;

      end;

      assume

       A13: q in W;

      assume

       A14: not thesis;

       A15:

      now

        given r be FinSequence of NAT such that

         A16: r in T and

         A17: q = ( <*( len p)*> ^ r);

        

         A18: ( len p) < (( len p) + 1) by NAT_1: 13;

        ((p ^ <*T*>) . (( len p) + 1)) = T by FINSEQ_1: 42;

        hence thesis by A1, A14, A16, A17, A18, Def15;

      end;

      now

        assume q in W2;

        then

         A19: q in ( tree p) or q in W1 by XBOOLE_0:def 3;

         A20:

        now

          assume q in ( tree p);

          then q = {} & {} in ( tree (p ^ <*T*>)) or ex n, r st n < ( len p) & r in (p . (n + 1)) & q = ( <*n*> ^ r) by Def15;

          then

          consider n, r such that

           A21: n < ( len p) and

           A22: r in (p . (n + 1)) and

           A23: q = ( <*n*> ^ r) by A14;

          (n + 1) in ( dom p) by A21, Lm3;

          then

           A24: (p . (n + 1)) = ((p ^ <*T*>) . (n + 1)) by FINSEQ_1:def 7;

          n < ( len (p ^ <*T*>)) by A1, A21, NAT_1: 13;

          hence thesis by A14, A22, A23, A24, Def15;

        end;

        now

          assume

           A25: not q in ( tree p);

          then q = {} or ex n st n < (( len p) + 1) & q = <*n*> by A19, TREES_1: 30;

          then

          consider n such that

           A26: n < (( len p) + 1) and

           A27: q = <*n*> by A14, TREES_1: 22;

           A28:

          now

            assume n < ( len p);

            then

             A29: (p . (n + 1)) in ( rng p) by Lm3;

            ( rng p) is constituted-Trees by Def9;

            hence {} in (p . (n + 1)) by A29, TREES_1: 22;

          end;

          

           A30: q = ( <*n*> ^ {} ) by A27, FINSEQ_1: 34;

          then

           A31: n >= ( len p) by A25, A28, Def15;

          n <= ( len p) by A26, NAT_1: 13;

          then

           A32: ( len p) = n by A31, XXREAL_0: 1;

          

           A33: n < (n + 1) by NAT_1: 13;

          

           A34: ((p ^ <*T*>) . (( len p) + 1)) = T by FINSEQ_1: 42;

           {} in T by TREES_1: 22;

          hence thesis by A1, A14, A30, A32, A33, A34, Def15;

        end;

        hence thesis by A20;

      end;

      hence thesis by A2, A13, A15, TREES_1:def 9;

    end;

    theorem :: TREES_3:56

    for p be Tree-yielding FinSequence holds ( tree (p ^ <*( elementary_tree 0 )*>)) = (( tree p) \/ ( elementary_tree (( len p) + 1)))

    proof

      let p be Tree-yielding FinSequence;

      ( len p) < (( len p) + 1) by NAT_1: 13;

      then

       A1: <*( len p)*> in ( elementary_tree (( len p) + 1)) by TREES_1: 28;

      then

       A2: <*( len p)*> in (( tree p) \/ ( elementary_tree (( len p) + 1))) by XBOOLE_0:def 3;

       {} in (( elementary_tree (( len p) + 1)) | <*( len p)*>) by TREES_1: 22;

      then

       A3: ( elementary_tree 0 ) c= (( elementary_tree (( len p) + 1)) | <*( len p)*>) by TREES_1: 29, ZFMISC_1: 31;

      

       A4: (( elementary_tree (( len p) + 1)) | <*( len p)*>) c= ( elementary_tree 0 )

      proof

        let x be object;

        assume x in (( elementary_tree (( len p) + 1)) | <*( len p)*>);

        then

        reconsider q = x as Element of (( elementary_tree (( len p) + 1)) | <*( len p)*>);

        ( <*( len p)*> ^ q) in ( elementary_tree (( len p) + 1)) by A1, TREES_1:def 6;

        then

        consider n such that n < (( len p) + 1) and

         A5: ( <*( len p)*> ^ q) = <*n*> by TREES_1: 30;

        

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

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

        then (1 + ( len q)) = (1 + 0 ) by A5, A6, FINSEQ_1: 22;

        then x = {} ;

        hence thesis by TREES_1: 22;

      end;

      now

        let n, r;

        assume <*( len p)*> = ( <*n*> ^ r);

        

        then n = ( <*( len p)*> . 1) by FINSEQ_1: 41

        .= ( len p) by FINSEQ_1: 40;

        hence not n < ( len p);

      end;

      then not ex n, q st n < ( len p) & q in (p . (n + 1)) & <*( len p)*> = ( <*n*> ^ q);

      then not <*( len p)*> in ( tree p) by Def15;

      

      then

       A7: ((( tree p) \/ ( elementary_tree (( len p) + 1))) | <*( len p)*>) = (( elementary_tree (( len p) + 1)) | <*( len p)*>) by A2, Th47

      .= ( elementary_tree 0 ) by A3, A4;

      

      thus ( tree (p ^ <*( elementary_tree 0 )*>)) = ((( tree p) \/ ( elementary_tree (( len p) + 1))) with-replacement ( <*( len p)*>,( elementary_tree 0 ))) by Th55

      .= (( tree p) \/ ( elementary_tree (( len p) + 1))) by A2, A7, TREES_2: 6;

    end;

    theorem :: TREES_3:57

    

     Th57: for p,q be Tree-yielding FinSequence holds for T1,T2 be Tree holds ( tree ((p ^ <*T1*>) ^ q)) = (( tree ((p ^ <*T2*>) ^ q)) with-replacement ( <*( len p)*>,T1))

    proof

      let p,q be Tree-yielding FinSequence, T1,T2 be Tree;

      set w1 = ((p ^ <*T1*>) ^ q), W1 = ( tree w1), w2 = ((p ^ <*T2*>) ^ q), W2 = ( tree w2), W = (W2 with-replacement ( <*( len p)*>,T1));

      

       A1: ( len <*T1*>) = 1 by FINSEQ_1: 40;

      

       A2: ( len <*T2*>) = 1 by FINSEQ_1: 40;

      

       A3: ( len (p ^ <*T1*>)) = (( len p) + 1) by A1, FINSEQ_1: 22;

      

       A4: ( len w1) = (( len (p ^ <*T1*>)) + ( len q)) by FINSEQ_1: 22;

      

       A5: ( len (p ^ <*T2*>)) = (( len p) + 1) by A2, FINSEQ_1: 22;

      

       A6: ( len w2) = (( len (p ^ <*T2*>)) + ( len q)) by FINSEQ_1: 22;

      (( len p) + 1) <= ((( len p) + 1) + ( len q)) by NAT_1: 11;

      then

       A7: ( len p) < ((( len p) + 1) + ( len q)) by NAT_1: 13;

      then

       A8: (w2 . (( len p) + 1)) in ( rng w2) by A5, A6, Lm3;

      ( rng w2) is constituted-Trees by Def9;

      then

       A9: {} in (w2 . (( len p) + 1)) by A8, TREES_1: 22;

      ( <*( len p)*> ^ {} ) = <*( len p)*> by FINSEQ_1: 34;

      then

       A10: <*( len p)*> in W2 by A5, A6, A7, A9, Def15;

      let r be FinSequence of NAT ;

      thus r in W1 implies r in W

      proof

        assume r in W1;

        then

         A11: r = {} or ex n, s st n < ( len w1) & s in (w1 . (n + 1)) & r = ( <*n*> ^ s) by Def15;

        now

          given n, s such that

           A12: n < ( len w1) and

           A13: s in (w1 . (n + 1)) and

           A14: r = ( <*n*> ^ s);

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

          

           A15: n <= ( len p) or n >= (( len p) + 1) by NAT_1: 13;

           A16:

          now

            assume

             A17: n < ( len p);

            then

             A18: (n + 1) in ( dom p) by Lm3;

            

             A19: ( dom p) c= ( dom (p ^ <*T2*>)) by FINSEQ_1: 26;

            

             A20: ( dom p) c= ( dom (p ^ <*T1*>)) by FINSEQ_1: 26;

            

             A21: ((p ^ <*T2*>) . (n + 1)) = (p . (n + 1)) by A18, FINSEQ_1:def 7;

            

             A22: ((p ^ <*T1*>) . (n + 1)) = (p . (n + 1)) by A18, FINSEQ_1:def 7;

            

             A23: (w2 . (n + 1)) = (p . (n + 1)) by A18, A19, A21, FINSEQ_1:def 7;

            (w1 . (n + 1)) = (p . (n + 1)) by A18, A20, A22, FINSEQ_1:def 7;

            then

             A24: r in W2 by A3, A4, A5, A6, A12, A13, A14, A23, Def15;

             not <*( len p)*> is_a_prefix_of ( <*n*> ^ s) by A17, TREES_1: 50;

            then not <*( len p)*> is_a_proper_prefix_of ( <*n*> ^ s);

            hence thesis by A10, A14, A24, TREES_1:def 9;

          end;

           A25:

          now

            assume

             A26: n = ( len p);

            then

             A27: ((p ^ <*T1*>) . (n + 1)) = T1 by FINSEQ_1: 42;

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

            then (n + 1) in ( dom (p ^ <*T1*>)) by A3, Lm3;

            then

             A28: (w1 . (n + 1)) = T1 by A27, FINSEQ_1:def 7;

            s = s;

            hence thesis by A10, A13, A14, A26, A28, TREES_1:def 9;

          end;

          now

            assume that

             A29: n >= (( len p) + 1) and

             A30: n < ((( len p) + 1) + ( len q));

            

             A31: (n + 1) >= ((( len p) + 1) + 1) by A29, XREAL_1: 7;

            

             A32: (n + 1) <= ((( len p) + 1) + ( len q)) by A30, NAT_1: 13;

            then

             A33: (w1 . (n + 1)) = (q . ((n + 1) - (( len p) + 1))) by A3, A31, FINSEQ_1: 23;

            (w2 . (n + 1)) = (q . ((n + 1) - (( len p) + 1))) by A5, A31, A32, FINSEQ_1: 23;

            then

             A34: r in W2 by A3, A4, A5, A6, A12, A13, A14, A33, Def15;

            ( len p) <> n by A29, NAT_1: 13;

            then not <*( len p)*> is_a_prefix_of ( <*n*> ^ s) by TREES_1: 50;

            then not <*( len p)*> is_a_proper_prefix_of ( <*n*> ^ s);

            hence thesis by A10, A14, A34, TREES_1:def 9;

          end;

          hence thesis by A3, A12, A15, A16, A25, FINSEQ_1: 22, XXREAL_0: 1;

        end;

        hence thesis by A11, TREES_1: 22;

      end;

      assume r in W;

      then

       A35: r in W2 & not <*( len p)*> is_a_proper_prefix_of r or ex s be FinSequence of NAT st s in T1 & r = ( <*( len p)*> ^ s) by A10, TREES_1:def 9;

      assume

       A36: not r in W1;

      then

       A37: r <> {} by Def15;

      

       A38: ((p ^ <*T1*>) . (( len p) + 1)) = T1 by FINSEQ_1: 42;

      

       A39: ( len p) < (( len p) + 1) by NAT_1: 13;

      (( len p) + 1) <= ((( len p) + 1) + ( len q)) by NAT_1: 11;

      then

       A40: ( len p) < ( len w2) by A5, A6, NAT_1: 13;

      (( len p) + 1) in ( dom (p ^ <*T1*>)) by A3, A39, Lm3;

      then

       A41: (w1 . (( len p) + 1)) = T1 by A38, FINSEQ_1:def 7;

      then

      consider n, s such that

       A42: n < ( len w2) and

       A43: s in (w2 . (n + 1)) and

       A44: r = ( <*n*> ^ s) by A3, A4, A5, A6, A35, A36, A37, A40, Def15;

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

      

       A45: n = ( len p) implies s = {} by A3, A4, A5, A6, A35, A36, A41, A42, A44, Def15, TREES_1: 10;

       {} in T1 by TREES_1: 22;

      then n <> ( len p) by A3, A4, A5, A6, A36, A41, A42, A44, A45, Def15;

      then n < ( len p) or n > ( len p) & 1 <= 1 by XXREAL_0: 1;

      then 1 <= (1 + n) & (1 + n) = (n + 1) & (n + 1) <= ( len p) & w1 = (p ^ ( <*T1*> ^ q)) & w2 = (p ^ ( <*T2*> ^ q)) or (( len p) + 1) < (n + 1) & (n + 1) <= ( len w1) by A3, A4, A5, A6, A42, FINSEQ_1: 32, NAT_1: 11, NAT_1: 13, XREAL_1: 6;

      then (w1 . (n + 1)) = (p . (n + 1)) & (w2 . (n + 1)) = (p . (n + 1)) or (w1 . (n + 1)) = (q . ((n + 1) - (( len p) + 1))) & (w2 . (n + 1)) = (q . ((n + 1) - (( len p) + 1))) by A3, A4, A5, A6, Lm1, FINSEQ_1: 24;

      hence contradiction by A3, A4, A5, A6, A36, A42, A43, A44, Def15;

    end;

    definition

      let n be Nat;

      :: original: <*

      redefine

      func <*n*> -> FinSequence of NAT ;

      coherence

      proof

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

         <*n*> is FinSequence of NAT ;

        hence thesis;

      end;

    end

    theorem :: TREES_3:58

    for T be Tree holds ( ^ T) = (( elementary_tree 1) with-replacement ( <* 0 *>,T))

    proof

      let T be Tree;

      let p be FinSequence of NAT ;

      

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

      

       A2: ( len <*T*>) = 1 by FINSEQ_1: 40;

      

       A3: ( 0 + 1) = 1;

      

       A4: {} in T by TREES_1: 22;

      

       A5: <* 0 *> in ( elementary_tree 1) by TARSKI:def 2, TREES_1: 51;

      thus p in ( ^ T) implies p in (( elementary_tree 1) with-replacement ( <* 0 *>,T))

      proof

        assume

         A6: p in ( ^ T);

        now

          assume p <> {} ;

          then

          consider n, q such that

           A7: n < ( len <*T*>) and

           A8: q in ( <*T*> . (n + 1)) and

           A9: p = ( <*n*> ^ q) by A6, Def15;

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

          

           A10: n = 0 by A2, A3, A7, NAT_1: 13;

          p = ( <*n*> ^ q) by A9;

          hence thesis by A1, A5, A8, A10, TREES_1:def 9;

        end;

        hence thesis by TREES_1: 22;

      end;

      assume p in (( elementary_tree 1) with-replacement ( <* 0 *>,T));

      then

       A11: p in ( elementary_tree 1) & not <* 0 *> is_a_proper_prefix_of p or ex r be FinSequence of NAT st r in T & p = ( <* 0 *> ^ r) by A5, TREES_1:def 9;

      now

        assume p in ( elementary_tree 1);

        then p = {} or p = <* 0 *> & (p ^ {} ) = p by FINSEQ_1: 34, TARSKI:def 2, TREES_1: 51;

        hence thesis by A1, A2, A3, A4, Def15;

      end;

      hence thesis by A1, A2, A3, A11, Def15;

    end;

    theorem :: TREES_3:59

    for T1,T2 be Tree holds ( tree (T1,T2)) = ((( elementary_tree 2) with-replacement ( <* 0 *>,T1)) with-replacement ( <*1*>,T2))

    proof

      let T1,T2 be Tree;

      let p be FinSequence of NAT ;

      

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

      

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

      

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

      

       A4: (1 + 1) = 2;

      

       A5: ( 0 + 1) = 1;

      

       A6: {} in T1 by TREES_1: 22;

      

       A7: {} in T2 by TREES_1: 22;

      

       A8: <* 0 *> in ( elementary_tree 2) by ENUMSET1:def 1, TREES_1: 53;

      

       A9: <*1*> in ( elementary_tree 2) by ENUMSET1:def 1, TREES_1: 53;

       not <* 0 *> is_a_proper_prefix_of <*1*> by TREES_1: 52;

      then

       A10: <*1*> in (( elementary_tree 2) with-replacement ( <* 0 *>,T1)) by A8, A9, TREES_1:def 9;

      thus p in ( tree (T1,T2)) implies p in ((( elementary_tree 2) with-replacement ( <* 0 *>,T1)) with-replacement ( <*1*>,T2))

      proof

        assume

         A11: p in ( tree (T1,T2));

        now

          assume p <> {} ;

          then

          consider n, q such that

           A12: n < ( len <*T1, T2*>) and

           A13: q in ( <*T1, T2*> . (n + 1)) and

           A14: p = ( <*n*> ^ q) by A11, Def15;

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

          

           A15: not <*1*> is_a_prefix_of ( <* 0 *> ^ q) by TREES_1: 50;

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

           A16:

          now

            assume

             A17: n = 0 ;

            then

             A18: not <*1*> is_a_proper_prefix_of ( <*n*> ^ q) by A15;

            ( <*n*> ^ q) in (( elementary_tree 2) with-replacement ( <* 0 *>,T1)) by A1, A8, A13, A17, TREES_1:def 9;

            hence thesis by A10, A14, A18, TREES_1:def 9;

          end;

          n <= ( 0 + 1) by A3, A4, A12, NAT_1: 13;

          then n = 1 & (n = 1 implies ( <*n*> ^ q) in ((( elementary_tree 2) with-replacement ( <* 0 *>,T1)) with-replacement ( <*1*>,T2))) or n >= 0 & n <= 0 by A2, A10, A13, NAT_1: 8, TREES_1:def 9;

          hence thesis by A14, A16;

        end;

        hence thesis by TREES_1: 22;

      end;

      assume p in ((( elementary_tree 2) with-replacement ( <* 0 *>,T1)) with-replacement ( <*1*>,T2));

      then

       A19: p in (( elementary_tree 2) with-replacement ( <* 0 *>,T1)) & not <*1*> is_a_proper_prefix_of p or ex r be FinSequence of NAT st r in T2 & p = ( <*1*> ^ r) by A10, TREES_1:def 9;

      now

        assume p in (( elementary_tree 2) with-replacement ( <* 0 *>,T1));

        then

         A20: p in ( elementary_tree 2) & not <* 0 *> is_a_proper_prefix_of p or ex r be FinSequence of NAT st r in T1 & p = ( <* 0 *> ^ r) by A8, TREES_1:def 9;

        now

          assume p in ( elementary_tree 2);

          then

           A21: p = {} or p = <* 0 *> or p = <*1*> by ENUMSET1:def 1, TREES_1: 53;

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

          hence thesis by A1, A2, A3, A4, A5, A6, A7, A21, Def15;

        end;

        hence thesis by A1, A3, A5, A20, Def15;

      end;

      hence thesis by A2, A3, A4, A19, Def15;

    end;

    registration

      let p be FinTree-yielding FinSequence;

      cluster ( tree p) -> finite;

      coherence

      proof

        defpred X[ set] means for p be FinTree-yielding FinSequence st ( len p) = $1 holds ( tree p) is finite Tree;

        

         A1: X[ 0 ]

        proof

          let p be FinTree-yielding FinSequence;

          assume ( len p) = 0 ;

          then p = {} ;

          hence thesis by Th52;

        end;

        

         A2: X[n] implies X[(n + 1)]

        proof

          assume

           A3: for p be FinTree-yielding FinSequence st ( len p) = n holds ( tree p) is finite Tree;

          let p be FinTree-yielding FinSequence such that

           A4: ( len p) = (n + 1);

          p <> {} by A4;

          then

          consider q be FinSequence, x be object such that

           A5: p = (q ^ <*x*>) by FINSEQ_1: 46;

          reconsider q as FinTree-yielding FinSequence by A5, Th26;

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

          then

           A6: ( len p) = (( len q) + 1) by A5, FINSEQ_1: 22;

          then ( tree q) is finite by A3, A4;

          then

          reconsider W = (( tree q) \/ ( elementary_tree (n + 1))) as finite Tree;

           <*x*> is FinTree-yielding by A5, Th26;

          then

          reconsider x as finite Tree by Th29;

          n < (n + 1) by NAT_1: 13;

          then <*n*> in ( elementary_tree (n + 1)) by TREES_1: 28;

          then

          reconsider r = <*n*> as Element of W by XBOOLE_0:def 3;

          ( tree p) = (W with-replacement (r,x)) by A4, A5, A6, Th55;

          hence thesis;

        end;

         X[n] from NAT_1:sch 2( A1, A2);

        then ( len p) = ( len p) implies thesis;

        hence thesis;

      end;

    end

    registration

      let T be finite Tree;

      cluster ( ^ T) -> finite;

      coherence ;

    end

    registration

      let T1,T2 be finite Tree;

      cluster ( tree (T1,T2)) -> finite;

      coherence ;

    end

    theorem :: TREES_3:60

    

     Th60: for T be Tree, x be object holds x in ( ^ T) iff x = {} or ex p st p in T & x = ( <* 0 *> ^ p)

    proof

      let T be Tree;

      let x;

      set p = <*T*>;

      

       A1: ( len p) = 1 by FINSEQ_1: 40;

      

       A2: (p . 1) = T by FINSEQ_1: 40;

      thus x in ( ^ T) & x <> {} implies ex p st p in T & x = ( <* 0 *> ^ p)

      proof

        assume that

         A3: x in ( ^ T) and

         A4: x <> {} ;

        consider n, q such that

         A5: n < ( len p) and

         A6: q in (p . (n + 1)) and

         A7: x = ( <*n*> ^ q) by A3, A4, Def15;

        ( 0 + 1) = 1;

        then n = 0 by A1, A5, NAT_1: 13;

        hence thesis by A2, A6, A7;

      end;

       0 < ( 0 + 1);

      hence thesis by A1, A2, Def15;

    end;

    theorem :: TREES_3:61

    

     Th61: for T be Tree, p be FinSequence holds p in T iff ( <* 0 *> ^ p) in ( ^ T)

    proof

      let T be Tree, p be FinSequence;

      thus p in T implies ( <* 0 *> ^ p) in ( ^ T) by Th60;

      assume ( <* 0 *> ^ p) in ( ^ T);

      then

      consider n, q such that n < ( len <*T*>) and

       A1: q in ( <*T*> . (n + 1)) and

       A2: ( <* 0 *> ^ p) = ( <*n*> ^ q) by Def15;

      

       A3: (( <* 0 *> ^ p) . 1) = 0 by FINSEQ_1: 41;

      

       A4: (( <*n*> ^ q) . 1) = n by FINSEQ_1: 41;

      then p = q by A2, A3, FINSEQ_1: 33;

      hence thesis by A1, A2, A3, A4, FINSEQ_1: 40;

    end;

    theorem :: TREES_3:62

    for T be Tree holds ( elementary_tree 1) c= ( ^ T)

    proof

      let T be Tree;

      let x be object;

      assume x in ( elementary_tree 1);

      then

      reconsider p = x as Element of ( elementary_tree 1);

      p = {} or p = <* 0 *> & {} in T & ( <* 0 *> ^ {} ) = <* 0 *> by FINSEQ_1: 34, TARSKI:def 2, TREES_1: 22, TREES_1: 51;

      hence thesis by Th60;

    end;

    theorem :: TREES_3:63

    for T1,T2 be Tree st T1 c= T2 holds ( ^ T1) c= ( ^ T2)

    proof

      let T1,T2 be Tree such that

       A1: T1 c= T2;

      let x be object;

      assume x in ( ^ T1);

      then

      reconsider p = x as Element of ( ^ T1);

      p = {} or ex q st q in T1 & p = ( <* 0 *> ^ q) by Th60;

      hence thesis by A1, Th60;

    end;

    theorem :: TREES_3:64

    for T1,T2 be Tree st ( ^ T1) = ( ^ T2) holds T1 = T2

    proof

      let T1,T2 be Tree such that

       A1: ( ^ T1) = ( ^ T2);

      let p be FinSequence of NAT ;

      p in T1 iff ( <* 0 *> ^ p) in ( ^ T1) by Th61;

      hence thesis by A1, Th61;

    end;

    theorem :: TREES_3:65

    for T be Tree holds (( ^ T) | <* 0 *>) = T

    proof

      let T be Tree;

      set p = <*T*>;

      

       A1: ( len p) = 1 by FINSEQ_1: 40;

      

       A2: (p . 1) = T by FINSEQ_1: 40;

      ( 0 + 1) = 1;

      hence thesis by A1, A2, Th49;

    end;

    theorem :: TREES_3:66

    for T1,T2 be Tree holds (( ^ T1) with-replacement ( <* 0 *>,T2)) = ( ^ T2)

    proof

      let T1,T2 be Tree;

      

       A1: ( len {} ) = 0 ;

      

       A2: <*T1*> = ( {} ^ <*T1*>) by FINSEQ_1: 34;

      

       A3: <*T2*> = ( {} ^ <*T2*>) by FINSEQ_1: 34;

      

       A4: <*T1*> = ( <*T1*> ^ {} ) by FINSEQ_1: 34;

       <*T2*> = ( <*T2*> ^ {} ) by FINSEQ_1: 34;

      hence thesis by A1, A2, A3, A4, Th57;

    end;

    theorem :: TREES_3:67

    ( ^ ( elementary_tree 0 )) = ( elementary_tree 1)

    proof

      set T = ( elementary_tree 0 );

      

      thus ( ^ T) = ( tree (1 |-> T)) by FINSEQ_2: 59

      .= ( elementary_tree 1) by Th54;

    end;

    theorem :: TREES_3:68

    

     Th68: for T1,T2 be Tree, x be object holds x in ( tree (T1,T2)) iff x = {} or ex p st p in T1 & x = ( <* 0 *> ^ p) or p in T2 & x = ( <*1*> ^ p)

    proof

      let T1,T2 be Tree;

      let x;

      set p = <*T1, T2*>;

      

       A1: ( len p) = 2 by FINSEQ_1: 44;

      

       A2: (p . 1) = T1 by FINSEQ_1: 44;

      

       A3: (p . 2) = T2 by FINSEQ_1: 44;

      thus x in ( tree (T1,T2)) & x <> {} implies ex p st p in T1 & x = ( <* 0 *> ^ p) or p in T2 & x = ( <*1*> ^ p)

      proof

        assume that

         A4: x in ( tree (T1,T2)) and

         A5: x <> {} ;

        consider n, q such that

         A6: n < ( len p) and

         A7: q in (p . (n + 1)) and

         A8: x = ( <*n*> ^ q) by A4, A5, Def15;

        (1 + 1) = 2;

        then n <= 1 by A1, A6, NAT_1: 13;

        then n = 1 or n < ( 0 + 1) by XXREAL_0: 1;

        then n = 1 or n = 0 by NAT_1: 13;

        hence thesis by A2, A3, A7, A8;

      end;

      now

        given q such that

         A9: q in T1 & x = ( <* 0 *> ^ q) or q in T2 & x = ( <*1*> ^ q);

        x = ( <* 0 *> ^ q) or x <> ( <* 0 *> ^ q);

        then

        consider n such that

         A10: n = 0 & x = ( <* 0 *> ^ q) or n = 1 & x <> ( <* 0 *> ^ q);

        take n, q;

        thus n < ( len p) by A1, A10;

        (( <* 0 *> ^ q) . 1) = 0 by FINSEQ_1: 41;

        hence q in (p . (n + 1)) & x = ( <*n*> ^ q) by A9, A10, FINSEQ_1: 41, FINSEQ_1: 44;

      end;

      hence thesis by Def15;

    end;

    theorem :: TREES_3:69

    

     Th69: for T1,T2 be Tree, p be FinSequence holds p in T1 iff ( <* 0 *> ^ p) in ( tree (T1,T2))

    proof

      let T1,T2 be Tree;

      

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

      

       A2: <*T1*> = ( {} ^ <*T1*>) by FINSEQ_1: 34;

      ( len {} ) = 0 ;

      hence thesis by A1, A2, Th51;

    end;

    theorem :: TREES_3:70

    

     Th70: for T1,T2 be Tree, p be FinSequence holds p in T2 iff ( <*1*> ^ p) in ( tree (T1,T2))

    proof

      let T1,T2 be Tree;

      

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

      

       A2: ( len <*T1*>) = 1 by FINSEQ_1: 40;

       <*T1, T2*> = ( <*T1, T2*> ^ {} ) by FINSEQ_1: 34;

      hence thesis by A1, A2, Th51;

    end;

    theorem :: TREES_3:71

    for T1,T2 be Tree holds ( elementary_tree 2) c= ( tree (T1,T2))

    proof

      let T1,T2 be Tree;

      let x be object;

      assume x in ( elementary_tree 2);

      then

      reconsider p = x as Element of ( elementary_tree 2);

      p = {} or p = <* 0 *> & {} in T1 & ( <* 0 *> ^ {} ) = <* 0 *> or p = <*1*> & {} in T2 & ( <*1*> ^ {} ) = <*1*> by ENUMSET1:def 1, FINSEQ_1: 34, TREES_1: 22, TREES_1: 53;

      hence thesis by Th68;

    end;

    theorem :: TREES_3:72

    for T1,T2,W1,W2 be Tree st T1 c= W1 & T2 c= W2 holds ( tree (T1,T2)) c= ( tree (W1,W2))

    proof

      let T1,T2,W1,W2 be Tree such that

       A1: T1 c= W1 and

       A2: T2 c= W2;

      let x be object;

      assume x in ( tree (T1,T2));

      then

      reconsider p = x as Element of ( tree (T1,T2));

      p = {} or ex q st q in T1 & p = ( <* 0 *> ^ q) or q in T2 & p = ( <*1*> ^ q) by Th68;

      hence thesis by A1, A2, Th68;

    end;

    theorem :: TREES_3:73

    for T1,T2,W1,W2 be Tree st ( tree (T1,T2)) = ( tree (W1,W2)) holds T1 = W1 & T2 = W2

    proof

      let T1,T2,W1,W2 be Tree such that

       A1: ( tree (T1,T2)) = ( tree (W1,W2));

      now

        let p;

        p in T1 iff ( <* 0 *> ^ p) in ( tree (T1,T2)) by Th69;

        hence p in T1 iff p in W1 by A1, Th69;

      end;

      hence for p be FinSequence of NAT holds p in T1 iff p in W1;

      let p be FinSequence of NAT ;

      p in T2 iff ( <*1*> ^ p) in ( tree (T1,T2)) by Th70;

      hence thesis by A1, Th70;

    end;

    theorem :: TREES_3:74

    for T1,T2 be Tree holds (( tree (T1,T2)) | <* 0 *>) = T1 & (( tree (T1,T2)) | <*1*>) = T2

    proof

      let T1,T2 be Tree;

      set p = <*T1, T2*>;

      

       A1: ( len p) = 2 by FINSEQ_1: 44;

      

       A2: (p . 1) = T1 by FINSEQ_1: 44;

      

       A3: (p . 2) = T2 by FINSEQ_1: 44;

      

       A4: ( 0 + 1) = 1;

      (1 + 1) = 2;

      hence thesis by A1, A2, A3, A4, Th49;

    end;

    theorem :: TREES_3:75

    for T,T1,T2 be Tree holds (( tree (T1,T2)) with-replacement ( <* 0 *>,T)) = ( tree (T,T2)) & (( tree (T1,T2)) with-replacement ( <*1*>,T)) = ( tree (T1,T))

    proof

      let T,T1,T2 be Tree;

      

       A1: ( len {} ) = 0 ;

      

       A2: <*T1*> = ( {} ^ <*T1*>) by FINSEQ_1: 34;

      

       A3: <*T*> = ( {} ^ <*T*>) by FINSEQ_1: 34;

      

       A4: ( <*T1, T2*> ^ {} ) = <*T1, T2*> by FINSEQ_1: 34;

      

       A5: ( <*T1, T*> ^ {} ) = <*T1, T*> by FINSEQ_1: 34;

      

       A6: ( len <*T1*>) = 1 by FINSEQ_1: 40;

      

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

      

       A8: <*T1, T*> = ( <*T1*> ^ <*T*>) by FINSEQ_1:def 9;

       <*T, T2*> = ( <*T*> ^ <*T2*>) by FINSEQ_1:def 9;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, Th57;

    end;

    theorem :: TREES_3:76

    ( tree (( elementary_tree 0 ),( elementary_tree 0 ))) = ( elementary_tree 2)

    proof

      set T = ( elementary_tree 0 );

      

      thus ( tree (T,T)) = ( tree (2 |-> T)) by FINSEQ_2: 61

      .= ( elementary_tree 2) by Th54;

    end;

    reserve w for FinTree-yielding FinSequence;

    theorem :: TREES_3:77

    

     Th77: for w st for t be finite Tree st t in ( rng w) holds ( height t) <= n holds ( height ( tree w)) <= (n + 1)

    proof

      let w such that

       A1: for t be finite Tree st t in ( rng w) holds ( height t) <= n;

      consider p be FinSequence of NAT such that

       A2: p in ( tree w) and

       A3: ( len p) = ( height ( tree w)) by TREES_1:def 12;

      

       A4: p = {} & ( len {} ) = 0 or ex n, q st n < ( len w) & q in (w . (n + 1)) & p = ( <*n*> ^ q) by A2, Def15;

      now

        given k, q such that

         A5: k < ( len w) and

         A6: q in (w . (k + 1)) and

         A7: p = ( <*k*> ^ q);

        

         A8: (w . (k + 1)) in ( rng w) by A5, Lm3;

        ( rng w) is constituted-FinTrees by Def10;

        then

        reconsider t = (w . (k + 1)) as finite Tree by A8;

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

        

         A9: ( len q) <= ( height t) by A6, TREES_1:def 12;

        

         A10: ( height t) <= n by A1, A5, Lm3;

        

         A11: ( len <*k*>) = 1 by FINSEQ_1: 40;

        

         A12: ( len q) <= n by A9, A10, XXREAL_0: 2;

        ( len p) = (1 + ( len q)) by A7, A11, FINSEQ_1: 22;

        hence thesis by A3, A12, XREAL_1: 7;

      end;

      hence thesis by A3, A4;

    end;

    theorem :: TREES_3:78

    

     Th78: for t be finite Tree st t in ( rng w) holds ( height ( tree w)) > ( height t)

    proof

      let t be finite Tree;

      assume t in ( rng w);

      then

      consider x be object such that

       A1: x in ( dom w) and

       A2: t = (w . x) by FUNCT_1:def 3;

      reconsider x as Element of NAT by A1;

      

       A3: 1 <= x by A1, FINSEQ_3: 25;

      

       A4: ( len w) >= x by A1, FINSEQ_3: 25;

      consider n be Nat such that

       A5: x = (1 + n) by A3, NAT_1: 10;

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

      

       A6: n < ( len w) by A4, A5, NAT_1: 13;

      

       A7: {} in t by TREES_1: 22;

      

       A8: ( <*n*> ^ {} ) = <*n*> by FINSEQ_1: 34;

      

       A9: t = (( tree w) | <*n*>) by A2, A5, A6, Th49;

       <*n*> in ( tree w) by A2, A5, A6, A7, A8, Def15;

      hence thesis by A9, TREES_1: 48;

    end;

    theorem :: TREES_3:79

    

     Th79: for t be finite Tree st t in ( rng w) & for t9 be finite Tree st t9 in ( rng w) holds ( height t9) <= ( height t) holds ( height ( tree w)) = (( height t) + 1)

    proof

      let t be finite Tree such that

       A1: t in ( rng w) and

       A2: for t9 be finite Tree st t9 in ( rng w) holds ( height t9) <= ( height t);

      

       A3: ( height ( tree w)) > ( height t) by A1, Th78;

      

       A4: ( height ( tree w)) <= (( height t) + 1) by A2, Th77;

      ( height ( tree w)) >= (( height t) + 1) by A3, NAT_1: 13;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: TREES_3:80

    for T be finite Tree holds ( height ( ^ T)) = (( height T) + 1)

    proof

      let T be finite Tree;

      set m = ( height T);

      

       A1: ( rng <*T*>) = {T} by FINSEQ_1: 38;

      

       A2: T in {T} by TARSKI:def 1;

      for t be finite Tree st t in ( rng <*T*>) holds ( height t) <= m by A1, TARSKI:def 1;

      hence thesis by A1, A2, Th79;

    end;

    theorem :: TREES_3:81

    for T1,T2 be finite Tree holds ( height ( tree (T1,T2))) = (( max (( height T1),( height T2))) + 1)

    proof

      let T1,T2 be finite Tree;

      set m = ( max (( height T1),( height T2)));

      

       A1: ( rng <*T1, T2*>) = {T1, T2} by FINSEQ_2: 127;

      

       A2: T1 in {T1, T2} by TARSKI:def 2;

      

       A3: T2 in {T1, T2} by TARSKI:def 2;

      

       A4: m = ( height T1) or m = ( height T2) by XXREAL_0:def 10;

      now

        let t be finite Tree;

        assume t in ( rng <*T1, T2*>);

        then t = T1 or t = T2 by A1, TARSKI:def 2;

        hence ( height t) <= m by XXREAL_0: 25;

      end;

      hence thesis by A1, A2, A3, A4, Th79;

    end;

    begin

    registration

      let D be non empty set, t be Element of ( FinTrees D);

      cluster ( dom t) -> finite;

      coherence by Def8;

    end

    definition

      let p be FinSequence;

      defpred P[ Nat, object] means ex T be DecoratedTree st T = (p . $1) & $2 = (T . {} );

      :: TREES_3:def18

      func roots p -> FinSequence means ( dom it ) = ( dom p) & for i be Element of NAT st i in ( dom p) holds ex T be DecoratedTree st T = (p . i) & (it . i) = (T . {} );

      existence

      proof

        

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

        

         A3: for k be Nat st k in ( Seg ( len p)) holds ex x be object st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len p));

          then

           A4: (p . k) in ( rng p) by A2, FUNCT_1:def 3;

          ( rng p) is constituted-DTrees by A1;

          then

          reconsider T = (p . k) as DecoratedTree by A4;

          take (T . {} ), T;

          thus thesis;

        end;

        consider q be FinSequence such that

         A5: ( dom q) = ( Seg ( len p)) & for k be Nat st k in ( Seg ( len p)) holds P[k, (q . k)] from FINSEQ_1:sch 1( A3);

        take q;

        thus ( dom q) = ( dom p) by A5, FINSEQ_1:def 3;

        thus thesis by A2, A5;

      end;

      uniqueness

      proof

        let x1,x2 be FinSequence such that

         A6: ( dom x1) = ( dom p) and

         A7: for i be Element of NAT st i in ( dom p) holds P[i, (x1 . i)] and

         A8: ( dom x2) = ( dom p) and

         A9: for i be Element of NAT st i in ( dom p) holds P[i, (x2 . i)];

        now

          let k be Nat;

          assume

           A10: k in ( dom p);

          then

           A11: P[k, (x1 . k)] by A7;

           P[k, (x2 . k)] by A9, A10;

          hence (x1 . k) = (x2 . k) by A11;

        end;

        hence thesis by A6, A8;

      end;

    end