trees_9.miz



    begin

    definition

      let D be non empty set;

      let F be non empty DTree-set of D;

      let Tset be non empty Subset of F;

      :: original: Element

      redefine

      mode Element of Tset -> Element of F ;

      coherence

      proof

        let x be Element of Tset;

        thus thesis;

      end;

    end

    registration

      cluster finite -> finite-order for Tree;

      coherence

      proof

        let t be Tree;

        assume t is finite;

        then

        reconsider s = t as finite Tree;

        take n = (( card s) + 1);

        let x be Element of t;

        deffunc U( Nat) = (x ^ <*($1 - 1)*>);

        consider f be FinSequence such that

         A1: ( len f) = n & for i be Nat st i in ( dom f) holds (f . i) = U(i) from FINSEQ_1:sch 2;

        

         A2: ( dom f) = ( Seg n) by A1, FINSEQ_1:def 3;

        assume

         A3: (x ^ <*n*>) in t;

        

         A4: ( rng f) c= ( succ x)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider i be object such that

           A5: i in ( dom f) and

           A6: y = (f . i) by FUNCT_1:def 3;

          reconsider i as Nat by A5;

          i >= 1 by A2, A5, FINSEQ_1: 1;

          then

          consider j be Nat such that

           A7: i = (1 + j) by NAT_1: 10;

          reconsider j as Nat;

          

           A8: j <= i by A7, NAT_1: 11;

          i <= n by A2, A5, FINSEQ_1: 1;

          then j <= n by A8, XXREAL_0: 2;

          then

           A9: (x ^ <*j*>) in t by A3, TREES_1:def 3;

          (i - 1) = j by A7;

          then y = (x ^ <*j*>) by A1, A5, A6;

          hence thesis by A9;

        end;

        

         A10: ( card ( succ x)) c= ( card t) by CARD_1: 11;

        f is one-to-one

        proof

          let z,y be object;

          assume that

           A11: z in ( dom f) & y in ( dom f) and

           A12: (f . z) = (f . y);

          reconsider i1 = z, i2 = y as Nat by A11;

          (f . z) = (x ^ <*(i1 - 1)*>) & (f . y) = (x ^ <*(i2 - 1)*>) by A1, A11;

          then <*(i1 - 1)*> = <*(i2 - 1)*> by A12, FINSEQ_1: 33;

          

          then (i1 - 1) = ( <*(i2 - 1)*> . 1) by FINSEQ_1: 40

          .= (i2 - 1) by FINSEQ_1: 40;

          hence thesis;

        end;

        then ( card ( dom f)) c= ( card ( succ x)) by A4, CARD_1: 10;

        then

         A13: ( Segm ( card ( dom f))) c= ( Segm ( card s)) by A10;

        

         A14: ( card s) <= n by NAT_1: 11;

        ( card ( Seg n)) = n by FINSEQ_1: 57;

        then n <= ( card s) by A2, A13, NAT_1: 39;

        then n = (( card s) + 0 ) by A14, XXREAL_0: 1;

        hence contradiction;

      end;

    end

    

     Lm1: for n be set, p be FinSequence st n in ( dom p) holds ex k be Nat st n = (k + 1) & k < ( len p)

    proof

      let n be set, p be FinSequence;

      assume

       A1: n in ( dom p);

      then

      reconsider n as Nat;

      n >= 1 by A1, FINSEQ_3: 25;

      then

      consider k be Nat such that

       A2: n = (1 + k) by NAT_1: 10;

      reconsider k as Nat;

      take k;

      n <= ( len p) by A1, FINSEQ_3: 25;

      hence thesis by A2, NAT_1: 13;

    end;

     Lm2:

    now

      let p,q be FinSequence such that

       A1: ( len p) = ( len q) and

       A2: for i be Nat st i < ( len p) holds (p . (i + 1)) = (q . (i + 1));

       A3:

      now

        let i be Nat;

        assume i in ( dom p);

        then ex k be Nat st i = (k + 1) & k < ( len p) by Lm1;

        hence (p . i) = (q . i) by A2;

      end;

      ( dom p) = ( dom q) by A1, FINSEQ_3: 29;

      hence p = q by A3;

    end;

    

     Lm3: for n be Nat, p be FinSequence holds n < ( len p) implies (n + 1) in ( dom p) & (p . (n + 1)) in ( rng p)

    proof

      let n be Nat, p be FinSequence;

      

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

      assume n < ( len p);

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

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

      hence thesis by FUNCT_1:def 3;

    end;

     Lm4:

    now

      let p be FinSequence;

      let x be set;

      assume x in ( rng p);

      then

      consider y be object such that

       A1: y in ( dom p) and

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

      ex k be Nat st y = (k + 1) & k < ( len p) by A1, Lm1;

      hence ex k be Nat st k < ( len p) & x = (p . (k + 1)) by A2;

    end;

    theorem :: TREES_9:1

    

     Th1: for t be DecoratedTree holds (t | ( <*> NAT )) = t

    proof

      let t be DecoratedTree;

      

       A1: ( dom (t | ( <*> NAT ))) = (( dom t) | ( <*> NAT )) by TREES_2:def 10;

      now

        let p be FinSequence of NAT ;

        assume p in ( dom (t | ( <*> NAT )));

        

        hence ((t | ( <*> NAT )) . p) = (t . ( {} ^ p)) by A1, TREES_2:def 10

        .= (t . p) by FINSEQ_1: 34;

      end;

      hence thesis by A1, TREES_1: 31;

    end;

    theorem :: TREES_9:2

    

     Th2: for t be Tree, p,q be FinSequence of NAT st (p ^ q) in t holds (t | (p ^ q)) = ((t | p) | q)

    proof

      let t be Tree, p,q be FinSequence of NAT ;

      assume

       A1: (p ^ q) in t;

      let r be FinSequence of NAT ;

      

       A2: p in t by A1, TREES_1: 21;

      then q in (t | p) by A1, TREES_1:def 6;

      then

       A3: r in ((t | p) | q) iff (q ^ r) in (t | p) by TREES_1:def 6;

      

       A4: ((p ^ q) ^ r) = (p ^ (q ^ r)) by FINSEQ_1: 32;

      r in (t | (p ^ q)) iff ((p ^ q) ^ r) in t by A1, TREES_1:def 6;

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

    end;

    theorem :: TREES_9:3

    

     Th3: for t be DecoratedTree, p,q be FinSequence of NAT st (p ^ q) in ( dom t) holds (t | (p ^ q)) = ((t | p) | q)

    proof

      let t be DecoratedTree, p,q be FinSequence of NAT ;

      

       A1: ( dom (t | p)) = (( dom t) | p) by TREES_2:def 10;

      

       A2: ( dom (t | (p ^ q))) = (( dom t) | (p ^ q)) by TREES_2:def 10;

      assume

       A3: (p ^ q) in ( dom t);

      then

       A4: p in ( dom t) by TREES_1: 21;

      then

       A5: q in (( dom t) | p) by A3, TREES_1:def 6;

       A6:

      now

        let a be FinSequence of NAT ;

        

         A7: ((p ^ q) ^ a) = (p ^ (q ^ a)) by FINSEQ_1: 32;

        assume

         A8: a in ( dom (t | (p ^ q)));

        then ((p ^ q) ^ a) in ( dom t) by A3, A2, TREES_1:def 6;

        then

         A9: (q ^ a) in (( dom t) | p) by A4, A7, TREES_1:def 6;

        then

         A10: a in ((( dom t) | p) | q) by A5, TREES_1:def 6;

        

        thus ((t | (p ^ q)) . a) = (t . ((p ^ q) ^ a)) by A2, A8, TREES_2:def 10

        .= ((t | p) . (q ^ a)) by A7, A9, TREES_2:def 10

        .= (((t | p) | q) . a) by A1, A10, TREES_2:def 10;

      end;

      ( dom ((t | p) | q)) = (( dom (t | p)) | q) by TREES_2:def 10;

      hence thesis by A3, A1, A2, A6, Th2;

    end;

    notation

      let IT be DecoratedTree;

      synonym IT is root for IT is trivial;

    end

    definition

      let IT be DecoratedTree;

      :: original: root

      redefine

      :: TREES_9:def1

      attr IT is root means ( dom IT) = ( elementary_tree 0 );

      compatibility

      proof

        thus IT is root implies ( dom IT) = ( elementary_tree 0 )

        proof

           not ( dom IT) is empty;

          then

           A1: not IT is empty;

          assume IT is root;

          then

          consider x be object such that

           A2: IT = {x} by A1, ZFMISC_1: 131;

          x in IT by A2, TARSKI:def 1;

          then

          consider x1,x2 be object such that

           A3: x = [x1, x2] by RELAT_1:def 1;

           {} in ( dom IT) & ( dom IT) = {x1} by A2, A3, RELAT_1: 9, TREES_1: 22;

          hence ( dom IT) = ( elementary_tree 0 ) by TARSKI:def 1, TREES_1: 29;

        end;

        thus thesis by TREES_1: 29;

      end;

    end

    theorem :: TREES_9:4

    

     Th4: for t be DecoratedTree holds t is root iff {} in ( Leaves ( dom t))

    proof

      let t be DecoratedTree;

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

      hereby

        assume t is root;

        then ( dom t) = ( elementary_tree 0 );

        then not (e ^ <* 0 *>) in ( dom t) by TARSKI:def 1, TREES_1: 29;

        hence {} in ( Leaves ( dom t)) by TREES_1: 54;

      end;

      assume

       A1: {} in ( Leaves ( dom t));

      let p be FinSequence of NAT ;

      hereby

        assume that

         A2: p in ( dom t) and

         A3: not p in ( elementary_tree 0 );

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

        then

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

         A4: p = ( <*n*> ^ q) by FINSEQ_2: 130;

        

         A5: (e ^ <*n*>) = <*n*> by FINSEQ_1: 34;

         <*n*> in ( dom t) by A2, A4, TREES_1: 21;

        hence contradiction by A1, A5, TREES_1: 55;

      end;

      assume p in ( elementary_tree 0 );

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

      hence thesis by TREES_1: 22;

    end;

    theorem :: TREES_9:5

    

     Th5: for t be Tree, p be Element of t holds (t | p) = ( elementary_tree 0 ) iff p in ( Leaves t)

    proof

      let t be Tree, p be Element of t;

      

       A1: not <* 0 *> in ( elementary_tree 0 ) by TARSKI:def 1, TREES_1: 29;

      hereby

        assume (t | p) = ( elementary_tree 0 );

        then not (p ^ <* 0 *>) in t by A1, TREES_1:def 6;

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

      end;

      assume

       A2: p in ( Leaves t);

      let q be FinSequence of NAT ;

      hereby

        assume q in (t | p);

        then (p ^ q) in t by TREES_1:def 6;

        then

         A3: not p is_a_proper_prefix_of (p ^ q) by A2, TREES_1:def 5;

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

        

        then (p ^ q) = p by A3

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

        then q = {} by FINSEQ_1: 33;

        hence q in ( elementary_tree 0 ) by TREES_1: 22;

      end;

      assume q in ( elementary_tree 0 );

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

      hence thesis by TREES_1: 22;

    end;

    theorem :: TREES_9:6

    for t be DecoratedTree, p be Node of t holds (t | p) is root iff p in ( Leaves ( dom t))

    proof

      let t be DecoratedTree, p be Node of t;

      

       A1: ( dom (t | p)) = (( dom t) | p) by TREES_2:def 10;

      thus thesis by A1, Th5;

    end;

    registration

      cluster root for DecoratedTree;

      existence

      proof

        take t = ( root-tree 0 );

        thus ( dom t) = ( elementary_tree 0 ) by TREES_4: 3;

      end;

      cluster finite non root for DecoratedTree;

      existence

      proof

        take t = ( 0 -tree ( root-tree 0 ));

        ( dom t) = ( ^ ( dom ( root-tree 0 ))) by TREES_4: 13

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

        hence t is finite by FINSET_1: 10;

        assume ( dom t) = ( elementary_tree 0 );

        

        then ( root-tree (t . {} )) = t by TREES_4: 5

        .= ( 0 -tree <*( root-tree 0 )*>);

        hence contradiction by TREES_4: 17;

      end;

    end

    registration

      let x be object;

      cluster ( root-tree x) -> finite root;

      coherence by TREES_4: 3;

    end

    definition

      let IT be Tree;

      :: TREES_9:def2

      attr IT is finite-branching means

      : Def2: for x be Element of IT holds ( succ x) is finite;

    end

    registration

      cluster finite-order -> finite-branching for Tree;

      coherence ;

    end

    definition

      let IT be DecoratedTree;

      :: TREES_9:def3

      attr IT is finite-order means

      : Def3: ( dom IT) is finite-order;

      :: TREES_9:def4

      attr IT is finite-branching means

      : Def4: ( dom IT) is finite-branching;

    end

    registration

      cluster finite -> finite-order for DecoratedTree;

      coherence ;

      cluster finite-order -> finite-branching for DecoratedTree;

      coherence ;

    end

    registration

      let t be finite-order DecoratedTree;

      cluster ( dom t) -> finite-order;

      coherence by Def3;

    end

    registration

      let t be finite-branching DecoratedTree;

      cluster ( dom t) -> finite-branching;

      coherence by Def4;

    end

    registration

      let t be finite-branching Tree;

      let p be Element of t;

      cluster ( succ p) -> finite;

      coherence by Def2;

    end

    scheme :: TREES_9:sch1

    FinOrdSet { f( object) -> set , X() -> finite set } :

for n be Nat holds f(n) in X() iff n < ( card X())

      provided

       A1: for x be set st x in X() holds ex n be Nat st x = f(n)

       and

       A2: for i,j be Nat st i < j & f(j) in X() holds f(i) in X()

       and

       A3: for i,j be Nat st f(i) = f(j) holds i = j;

      consider f be Function such that

       A4: ( dom f) = ( card X()) & for x be object st x in ( card X()) holds (f . x) = f(x) from FUNCT_1:sch 3;

      defpred X[ Nat] means $1 < ( card X()) implies f($1) in X();

      

       A5: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat such that

         A6: n < ( card X()) implies f(n) in X() and

         A7: (n + 1) < ( card X()) and

         A8: not f(+) in X();

        consider f be Function such that

         A9: ( dom f) = (n + 1) & for x be object st x in (n + 1) holds (f . x) = f(x) from FUNCT_1:sch 3;

        

         A10: (n + 1) = { k where k be Nat : k < (n + 1) } by AXIOMS: 4;

        

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

        

         A12: ( rng f) = X()

        proof

          hereby

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A13: y in (n + 1) and

             A14: x = (f . y) by A9, FUNCT_1:def 3;

            consider k be Nat such that

             A15: y = k and

             A16: k < (n + 1) by A10, A13;

            reconsider k as Nat;

            k <= n by A16, NAT_1: 13;

            then k = n or k < n by XXREAL_0: 1;

            then f(k) in X() by A2, A6, A7, A11, XXREAL_0: 2;

            hence x in X() by A9, A13, A14, A15;

          end;

          let x be object;

          assume

           A17: x in X();

          then

          consider k be Nat such that

           A18: x = f(k) by A1;

          now

            assume k >= (n + 1);

            then k = (n + 1) or k > (n + 1) by XXREAL_0: 1;

            hence contradiction by A2, A8, A17, A18;

          end;

          then

           A19: k in (n + 1) by A10;

          then x = (f . k) by A9, A18;

          hence thesis by A9, A19, FUNCT_1:def 3;

        end;

        f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A20: x1 in ( dom f) and

           A21: x2 in ( dom f) and

           A22: (f . x1) = (f . x2);

          (ex k be Nat st x1 = k & k < (n + 1)) & ex k be Nat st x2 = k & k < (n + 1) by A9, A10, A20, A21;

          then

           A23: f(x1) = f(x2) implies x1 = x2 by A3;

          f(x1) = (f . x1) by A9, A20;

          hence thesis by A9, A21, A22, A23;

        end;

        then ((n + 1),X()) are_equipotent by A9, A12, WELLORD2:def 4;

        hence thesis by A7, CARD_1:def 2;

      end;

      

       A24: ( card X()) = { n where n be Nat : n < ( card X()) } by AXIOMS: 4;

      f is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A25: x1 in ( dom f) and

         A26: x2 in ( dom f);

        (ex k be Nat st x1 = k & k < ( card X())) & ex k be Nat st x2 = k & k < ( card X()) by A4, A24, A25, A26;

        then

         A27: f(x1) = f(x2) implies x1 = x2 by A3;

        f(x1) = (f . x1) by A4, A25;

        hence thesis by A4, A26, A27;

      end;

      then

       A28: (( dom f),( rng f)) are_equipotent by WELLORD2:def 4;

      then

      reconsider Y = ( rng f) as finite set by A4, CARD_1: 38;

      

       A29: ( card ( rng f)) = ( card ( card X())) by A4, A28, CARD_1: 5

      .= ( card X());

       A30:

      now

        given i be Nat such that

         A31: i >= ( card X()) and

         A32: f(i) in X();

        ( card X()) < i or ( card X()) = i by A31, XXREAL_0: 1;

        then

         A33: f(card) in X() by A2, A32;

        ( rng f) c= (X() \ {f(card)})

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A34: y in ( card X()) and

           A35: x = (f . y) by A4, FUNCT_1:def 3;

          consider k be Nat such that

           A36: y = k and

           A37: k < ( card X()) by A24, A34;

          

           A38: f(k) = x by A4, A34, A35, A36;

           A39:

          now

            assume x in {f(card)};

            then f(k) = f(card) by A38, TARSKI:def 1;

            hence contradiction by A3, A37;

          end;

          f(k) in X() by A2, A33, A37;

          hence thesis by A38, A39, XBOOLE_0:def 5;

        end;

        then

         A40: ( card Y) <= ( card (X() \ {f(card)})) by NAT_1: 43;

         {f(card)} c= X() by A33, ZFMISC_1: 31;

        then ( card Y) <= (( card X()) - ( card {f(card)})) by A40, CARD_2: 44;

        then ( card Y) <= (( card Y) - 1) by A29, CARD_2: 42;

        then (( card Y) + 1) <= ((( card Y) - 1) + 1) by XREAL_1: 7;

        hence contradiction by NAT_1: 13;

      end;

      

       A41: X[ 0 ]

      proof

        assume 0 < ( card X());

        then

        reconsider X = X() as non empty set;

        set x = the Element of X;

        consider n be Nat such that

         A42: x = f(n) by A1;

        n = 0 or n > 0 ;

        hence thesis by A2, A42;

      end;

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

      hence thesis by A30;

    end;

    theorem :: TREES_9:7

    

     Th7: for t be finite-branching Tree, p be Element of t holds for n be Nat holds (p ^ <*n*>) in ( succ p) iff n < ( card ( succ p))

    proof

      let t be finite-branching Tree, p be Element of t;

      deffunc U( Nat) = (p ^ <*$1*>);

      

       A1: for x be set st x in ( succ p) holds ex n be Nat st x = U(n)

      proof

        let x be set;

        assume x in ( succ p);

        then ex n be Nat st x = U(n) & U(n) in t;

        hence thesis;

      end;

      

       A2: for i,j be Nat st i < j & U(j) in ( succ p) holds U(i) in ( succ p)

      proof

        let i,j be Nat;

        assume

         A3: i < j & (p ^ <*j*>) in ( succ p);

        reconsider i, j as Nat;

        (p ^ <*i*>) in t by A3, TREES_1:def 3;

        hence thesis;

      end;

      

       A4: for i,j be Nat st U(i) = U(j) holds i = j

      proof

        let i,j be Nat;

        assume (p ^ <*i*>) = (p ^ <*j*>);

        

        hence i = ((p ^ <*j*>) . (( len p) + 1)) by FINSEQ_1: 42

        .= j by FINSEQ_1: 42;

      end;

      thus for n be Nat holds U(n) in ( succ p) iff n < ( card ( succ p)) from FinOrdSet( A1, A2, A4);

    end;

    definition

      let t be finite-branching Tree;

      let p be Element of t;

      :: TREES_9:def5

      func p succ -> one-to-one FinSequence of t means

      : Def5: ( len it ) = ( card ( succ p)) & ( rng it ) = ( succ p) & for i be Nat st i < ( len it ) holds (it . (i + 1)) = (p ^ <*i*>);

      existence

      proof

        deffunc U( Nat) = (p ^ <*($1 - 1)*>);

        consider q be FinSequence such that

         A1: ( len q) = ( card ( succ p)) & for i be Nat st i in ( dom q) holds (q . i) = U(i) from FINSEQ_1:sch 2;

        

         A2: q is one-to-one

        proof

          let x1,x2 be object;

          assume

           A3: x1 in ( dom q) & x2 in ( dom q);

          then

          reconsider i1 = x1, i2 = x2 as Nat;

          

           A4: ((p ^ <*(i1 - 1)*>) . (( len p) + 1)) = (i1 - 1) & ((p ^ <*(i2 - 1)*>) . (( len p) + 1)) = (i2 - 1) by FINSEQ_1: 42;

          (q . x1) = (p ^ <*(i1 - 1)*>) & (q . x2) = (p ^ <*(i2 - 1)*>) by A1, A3;

          hence thesis by A4;

        end;

        

         A5: for i be Nat st i < ( len q) holds (q . (i + 1)) = (p ^ <*i*>)

        proof

          let i be Nat;

          assume i < ( len q);

          then (q . (i + 1)) = (p ^ <*((i + 1) - 1)*>) by A1, Lm3;

          hence thesis;

        end;

        

         A6: ( rng q) c= ( succ p)

        proof

          let x be object;

          assume x in ( rng q);

          then

          consider k be Nat such that

           A7: k < ( len q) and

           A8: x = (q . (k + 1)) by Lm4;

          x = (p ^ <*k*>) by A5, A7, A8;

          hence thesis by A1, A7, Th7;

        end;

        then

        reconsider q as one-to-one FinSequence of ( succ p) by A2, FINSEQ_1:def 4;

        take q;

        thus ( len q) = ( card ( succ p)) & ( rng q) c= ( succ p) by A1, A6;

        thus ( succ p) c= ( rng q)

        proof

          let x be object;

          assume

           A9: x in ( succ p);

          then

          consider n be Nat such that

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

          

           A11: n < ( card ( succ p)) by A9, A10, Th7;

          then (q . (n + 1)) = x by A1, A5, A10;

          hence thesis by A1, A11, Lm3;

        end;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let q1,q2 be one-to-one FinSequence of t such that

         A12: ( len q1) = ( card ( succ p)) and ( rng q1) = ( succ p) and

         A13: for i be Nat st i < ( len q1) holds (q1 . (i + 1)) = (p ^ <*i*>) and

         A14: ( len q2) = ( card ( succ p)) and ( rng q2) = ( succ p) and

         A15: for i be Nat st i < ( len q2) holds (q2 . (i + 1)) = (p ^ <*i*>);

        

         A16: ( dom q1) = ( Seg ( card ( succ p))) by A12, FINSEQ_1:def 3;

         A17:

        now

          let k be Nat;

          assume k in ( Seg ( card ( succ p)));

          then

          consider n be Nat such that

           A18: k = (n + 1) & n < ( len q1) by A16, Lm1;

          

          thus (q1 . k) = (p ^ <*n*>) by A13, A18

          .= (q2 . k) by A12, A14, A15, A18;

        end;

        ( dom q2) = ( Seg ( card ( succ p))) by A14, FINSEQ_1:def 3;

        hence thesis by A16, A17;

      end;

    end

    definition

      let t be finite-branching DecoratedTree;

      let p be FinSequence;

      :: TREES_9:def6

      func succ (t,p) -> FinSequence means

      : Def6: ex q be Element of ( dom t) st q = p & it = (t * (q succ ));

      existence

      proof

        reconsider q = p as Element of ( dom t) by A1;

        ( rng (q succ )) c= ( dom t);

        

        then ( dom (t * (q succ ))) = ( dom (q succ )) by RELAT_1: 27

        .= ( Seg ( len (q succ ))) by FINSEQ_1:def 3;

        then (t * (q succ )) is FinSequence by FINSEQ_1:def 2;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: TREES_9:8

    

     Th8: for t be finite-branching DecoratedTree holds ex x be set, p be DTree-yielding FinSequence st t = (x -tree p)

    proof

      let t be finite-branching DecoratedTree;

      take (t . {} );

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

      defpred X[ object, object] means ex n be Element of NAT st (n + 1) = $1 & $2 = (t | <*n*>);

      (( dom t) -level 1) = ( succ e) by TREES_2: 13;

      then

      reconsider A = (( dom t) -level 1) as finite set;

      reconsider e = {} as Element of ( dom t) by TREES_1: 22;

      

       A1: for z be object st z in ( Seg ( card A)) holds ex u be object st X[z, u]

      proof

        let z be object;

        assume

         A2: z in ( Seg ( card A));

        then

        reconsider m = z as Nat;

        m >= 1 by A2, FINSEQ_1: 1;

        then

        consider n be Nat such that

         A3: m = (1 + n) by NAT_1: 10;

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

        reconsider y = (t | <*n*>) as set;

        take y, n;

        thus thesis by A3;

      end;

      consider p be Function such that

       A4: ( dom p) = ( Seg ( card A)) and

       A5: for z be object st z in ( Seg ( card A)) holds X[z, (p . z)] from CLASSES1:sch 1( A1);

      reconsider p as FinSequence by A4, FINSEQ_1:def 2;

      

       A6: ( len p) = ( card A) by A4, FINSEQ_1:def 3;

       A7:

      now

        let x be object;

        assume x in ( dom p);

        then ex n be Element of NAT st (n + 1) = x & (p . x) = (t | <*n*>) by A4, A5;

        hence (p . x) is DecoratedTree;

      end;

       A8:

      now

        let n be Nat;

        thus (e ^ <*n*>) = <*n*> & ( succ e) = A by FINSEQ_1: 34, TREES_2: 13;

        hence <*n*> in A iff n < ( card A) by Th7;

      end;

      reconsider p as DTree-yielding FinSequence by A7, TREES_3: 24;

      

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

      now

        let x be object;

        hereby

          assume that

           A10: x in ( dom t) and

           A11: x <> {} ;

          reconsider r = x as Node of t by A10;

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

           A12: r = ( <*n*> ^ q) by A11, FINSEQ_2: 130;

          

           A13: <*n*> in ( dom t) by A12, TREES_1: 21;

          reconsider q as FinSequence;

          reconsider nn = n as Nat;

          take nn, q;

          (e ^ <*n*>) = <*n*> by A8;

          then <*n*> in A by A8, A13;

          hence nn < ( len ( doms p)) by A6, A8, A9;

          then (n + 1) in ( dom p) & ex k be Element of NAT st (k + 1) = (n + 1) & (p . (n + 1)) = (t | <*k*>) by A4, A5, A9, Lm3;

          

          then (( doms p) . (n + 1)) = ( dom (t | <*n*>)) by FUNCT_6: 22

          .= (( dom t) | <*n*>) by TREES_2:def 10;

          hence q in (( doms p) . (nn + 1)) & x = ( <*nn*> ^ q) by A12, A13, TREES_1:def 6;

        end;

        assume

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

        assume

         A15: not x in ( dom t);

        then

        consider n be Nat, q be FinSequence such that

         A16: n < ( len ( doms p)) and

         A17: q in (( doms p) . (n + 1)) and

         A18: x = ( <*n*> ^ q) by A14, TREES_1: 22;

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

        (n + 1) in ( dom p) & ex k be Element of NAT st (k + 1) = (n + 1) & (p . (n + 1)) = (t | <*k*>) by A4, A5, A9, A16, Lm3;

        

        then (( doms p) . (n + 1)) = ( dom (t | <*n*>)) by FUNCT_6: 22

        .= (( dom t) | <*n*>) by TREES_2:def 10;

        then

        reconsider q as Element of (( dom t) | <*n*>) by A17;

         <*n*> in A by A6, A8, A9, A16;

        then ( <*n*> ^ q) in ( dom t) by TREES_1:def 6;

        hence contradiction by A15, A18;

      end;

      then

       A19: ( dom t) = ( tree ( doms p)) by TREES_3:def 15;

      take p;

      now

        let n be Nat;

        assume n < ( len p);

        then ex m be Element of NAT st (m + 1) = (n + 1) & (p . (n + 1)) = (t | <*m*>) by A4, A5, Lm3;

        hence (t | <*n*>) = (p . (n + 1));

      end;

      hence thesis by A19, TREES_4:def 4;

    end;

    registration

      let t be finite DecoratedTree;

      let p be Node of t;

      cluster (t | p) -> finite;

      coherence ;

    end

    theorem :: TREES_9:9

    

     Th9: for t be finite Tree, p be Element of t st t = (t | p) holds p = {}

    proof

      let t be finite Tree, p be Element of t;

      p <> {} implies ( height t) > ( height (t | p)) by TREES_1: 48;

      hence thesis;

    end;

    registration

      let D be non empty set;

      let S be non empty Subset of ( FinTrees D);

      cluster -> finite for Element of S;

      coherence ;

    end

    begin

    definition

      let t be DecoratedTree;

      :: TREES_9:def7

      func Subtrees t -> set equals the set of all (t | p) where p be Node of t;

      coherence ;

    end

    registration

      let t be DecoratedTree;

      cluster ( Subtrees t) -> constituted-DTrees non empty;

      coherence

      proof

        set p0 = the Node of t;

        set S = the set of all (t | p) where p be Node of t;

        (t | p0) in S;

        then

        reconsider S as non empty set;

        S is constituted-DTrees

        proof

          let x be object;

          assume x in S;

          then ex p be Node of t st x = (t | p);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      let t be DecoratedTree of D;

      :: original: Subtrees

      redefine

      func Subtrees t -> non empty Subset of ( Trees D) ;

      coherence

      proof

        ( Subtrees t) c= ( Trees D)

        proof

          let x be object;

          assume x in ( Subtrees t);

          then ex p be Node of t st x = (t | p);

          hence thesis by TREES_3:def 7;

        end;

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      let t be finite DecoratedTree of D;

      :: original: Subtrees

      redefine

      func Subtrees t -> non empty Subset of ( FinTrees D) ;

      coherence

      proof

        ( Subtrees t) c= ( FinTrees D)

        proof

          let x be object;

          assume x in ( Subtrees t);

          then ex p be Node of t st x = (t qua DecoratedTree of D | p);

          then

          reconsider x as finite DecoratedTree of D;

          ( dom x) is finite;

          hence thesis by TREES_3:def 8;

        end;

        hence thesis;

      end;

    end

    registration

      let t be finite DecoratedTree;

      cluster -> finite for Element of ( Subtrees t);

      coherence

      proof

        let x be Element of ( Subtrees t);

        x in the set of all (t | p) where p be Node of t;

        then ex p be Node of t st x = (t | p);

        hence thesis;

      end;

    end

    reserve x for set,

t,t1,t2 for DecoratedTree;

    theorem :: TREES_9:10

    

     Th10: x in ( Subtrees t) iff ex n be Node of t st x = (t | n);

    theorem :: TREES_9:11

    

     Th11: t in ( Subtrees t)

    proof

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

      (t | e) = t by Th1;

      hence thesis;

    end;

    theorem :: TREES_9:12

    t1 is finite & ( Subtrees t1) = ( Subtrees t2) implies t1 = t2

    proof

      assume that

       A1: t1 is finite and

       A2: ( Subtrees t1) = ( Subtrees t2);

      reconsider t = t1 as finite DecoratedTree by A1;

      t1 in ( Subtrees t2) by A2, Th11;

      then

      consider n be Node of t2 such that

       A3: t1 = (t2 | n);

      t2 in ( Subtrees t1) by A2, Th11;

      then

      consider m be Node of t1 such that

       A4: t2 = (t1 | m);

      ( dom (t1 | m)) = (( dom t1) | m) by TREES_2:def 10;

      then

      reconsider p = (m ^ n) as Element of ( dom t) by A4, TREES_1:def 6;

      t = (t | p) by A3, A4, Th3;

      then ( dom t) = (( dom t) | p) by TREES_2:def 10;

      then n = {} by Th9;

      hence thesis by A3, Th1;

    end;

    theorem :: TREES_9:13

    for n be Node of t holds ( Subtrees (t | n)) c= ( Subtrees t)

    proof

      let n be Node of t;

      let x be object;

      assume x in ( Subtrees (t | n));

      then

      consider p be Node of (t | n) such that

       A1: x = ((t | n) | p);

      ( dom (t | n)) = (( dom t) | n) by TREES_2:def 10;

      then

      reconsider q = (n ^ p) as Node of t by TREES_1:def 6;

      x = (t | q) by A1, Th3;

      hence thesis;

    end;

    definition

      let t be DecoratedTree;

      :: TREES_9:def8

      func FixedSubtrees t -> Subset of [:( dom t), ( Subtrees t):] equals the set of all [p, (t | p)] where p be Node of t;

      coherence

      proof

        set S = the set of all [p, (t | p)] where p be Node of t;

        S c= [:( dom t), ( Subtrees t):]

        proof

          let x be object;

          assume x in S;

          then

          consider p be Node of t such that

           A1: x = [p, (t | p)];

          (t | p) in ( Subtrees t);

          hence thesis by A1, ZFMISC_1: 87;

        end;

        hence thesis;

      end;

    end

    registration

      let t be DecoratedTree;

      cluster ( FixedSubtrees t) -> non empty;

      coherence

      proof

        set p0 = the Node of t;

        set S = the set of all [p, (t | p)] where p be Node of t;

         [p0, (t | p0)] in S;

        hence thesis;

      end;

    end

    theorem :: TREES_9:14

    x in ( FixedSubtrees t) iff ex n be Node of t st x = [n, (t | n)];

    theorem :: TREES_9:15

    

     Th15: [ {} , t] in ( FixedSubtrees t)

    proof

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

      (t | e) = t by Th1;

      hence thesis;

    end;

    theorem :: TREES_9:16

    ( FixedSubtrees t1) = ( FixedSubtrees t2) implies t1 = t2

    proof

      assume ( FixedSubtrees t1) = ( FixedSubtrees t2);

      then [ {} , t1] in ( FixedSubtrees t2) by Th15;

      then

      consider n be Node of t2 such that

       A1: [ {} , t1] = [n, (t2 | n)];

       {} = n & t1 = (t2 | n) by A1, XTUPLE_0: 1;

      hence thesis by Th1;

    end;

    definition

      let t be DecoratedTree;

      let C be set;

      :: TREES_9:def9

      func C -Subtrees t -> Subset of ( Subtrees t) equals { (t | p) where p be Node of t : not p in ( Leaves ( dom t)) or (t . p) in C };

      coherence

      proof

        set W = { (t | p) where p be Node of t : not p in ( Leaves ( dom t)) or (t . p) in C };

        W c= ( Subtrees t)

        proof

          let x be object;

          assume x in W;

          then ex p be Node of t st x = (t | p) & ( not p in ( Leaves ( dom t)) or (t . p) in C);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    reserve C for set;

    theorem :: TREES_9:17

    

     Th17: x in (C -Subtrees t) iff ex n be Node of t st x = (t | n) & ( not n in ( Leaves ( dom t)) or (t . n) in C);

    theorem :: TREES_9:18

    (C -Subtrees t) is empty iff t is root & not (t . {} ) in C

    proof

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

      hereby

        assume (C -Subtrees t) is empty;

        then

         A1: not (t | e) in (C -Subtrees t);

        then e in ( Leaves ( dom t));

        hence t is root & not (t . {} ) in C by A1, Th4;

      end;

      assume that

       A2: t is root and

       A3: not (t . {} ) in C;

      assume not (C -Subtrees t) is empty;

      then

      reconsider S = (C -Subtrees t) as non empty Subset of ( Subtrees t);

      set s = the Element of S;

      consider n be Node of t such that s = (t | n) and

       A4: not n in ( Leaves ( dom t)) or (t . n) in C by Th17;

      

       A5: ( dom t) = { {} } by A2, TREES_1: 29;

      then n = {} by TARSKI:def 1;

      then (e ^ <* 0 *>) in ( dom t) by A3, A4, TREES_1: 54;

      hence contradiction by A5, TARSKI:def 1;

    end;

    definition

      let t be finite DecoratedTree;

      let C be set;

      :: TREES_9:def10

      func C -ImmediateSubtrees t -> Function of (C -Subtrees t), (( Subtrees t) * ) means for d be DecoratedTree st d in (C -Subtrees t) holds for p be FinSequence of ( Subtrees t) st p = (it . d) holds d = ((d . {} ) -tree p);

      existence

      proof

        defpred X[ object, object] means ex d be DecoratedTree, p be FinSequence of ( Subtrees t) st p = $2 & d = $1 & d = ((d . {} ) -tree p);

        

         A1: for x be object st x in (C -Subtrees t) holds ex y be object st y in (( Subtrees t) * ) & X[x, y]

        proof

          let x be object;

          assume x in (C -Subtrees t);

          then

          reconsider s = x as Element of ( Subtrees t);

          reconsider d = s as DecoratedTree;

          consider sp be Node of t such that

           A2: s = (t | sp) by Th10;

          consider z be set, p be DTree-yielding FinSequence such that

           A3: s = (z -tree p) by Th8;

          ( rng p) c= ( Subtrees t)

          proof

            let x be object;

            

             A4: ( dom (t | sp)) = (( dom t) | sp) by TREES_2:def 10;

            assume x in ( rng p);

            then

            consider k be Nat such that

             A5: k < ( len p) & x = (p . (k + 1)) by Lm4;

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

            reconsider e = {} as Node of (s | <*k*>) by TREES_1: 22;

            

             A6: x = (s | <*k*>) by A3, A5, TREES_4:def 4;

            ( <*k*> ^ e) = <*k*> by FINSEQ_1: 34;

            then <*k*> in ( dom s) by A3, A5, A6, TREES_4: 11;

            then

            reconsider q = (sp ^ <*k*>) as Node of t by A2, A4, TREES_1:def 6;

            x = (t | q) by A2, A6, Th3;

            hence thesis;

          end;

          then

          reconsider p as FinSequence of ( Subtrees t) by FINSEQ_1:def 4;

          reconsider y = p as set;

          take y;

          thus y in (( Subtrees t) * ) by FINSEQ_1:def 11;

          take d, p;

          thus thesis by A3, TREES_4:def 4;

        end;

        consider f be Function such that

         A7: ( dom f) = (C -Subtrees t) & ( rng f) c= (( Subtrees t) * ) & for x be object st x in (C -Subtrees t) holds X[x, (f . x)] from FUNCT_1:sch 6( A1);

        reconsider f as Function of (C -Subtrees t), (( Subtrees t) * ) by A7, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        let d be DecoratedTree;

        assume d in (C -Subtrees t);

        then ex d9 be DecoratedTree, p be FinSequence of ( Subtrees t) st p = (f . d) & d9 = d & d9 = ((d9 . {} ) -tree p) by A7;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of (C -Subtrees t), (( Subtrees t) * ) such that

         A8: (for d be DecoratedTree st d in (C -Subtrees t) holds for p be FinSequence of ( Subtrees t) st p = (f1 . d) holds d = ((d . {} ) -tree p)) & for d be DecoratedTree st d in (C -Subtrees t) holds for p be FinSequence of ( Subtrees t) st p = (f2 . d) holds d = ((d . {} ) -tree p);

        now

          let x be object;

          assume

           A9: x in (C -Subtrees t);

          then

          reconsider s = x as Element of ( Subtrees t);

          reconsider p1 = (f1 . s), p2 = (f2 . s) as Element of (( Subtrees t) * ) by A9, FUNCT_2: 5;

          s = ((s . {} ) -tree p1) & s = ((s . {} ) -tree p2) by A8, A9;

          hence (f1 . x) = (f2 . x) by TREES_4: 15;

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    begin

    definition

      let X be constituted-DTrees non empty set;

      :: TREES_9:def11

      func Subtrees X -> set equals the set of all (t | p) where t be Element of X, p be Node of t;

      coherence ;

    end

    registration

      let X be constituted-DTrees non empty set;

      cluster ( Subtrees X) -> constituted-DTrees non empty;

      coherence

      proof

        set S = the set of all (t | p) where t be Element of X, p be Node of t;

        set t = the Element of X, p0 = the Node of t;

        (t | p0) in S;

        then

        reconsider S as non empty set;

        S is constituted-DTrees

        proof

          let x be object;

          assume x in S;

          then ex t be Element of X, p be Node of t st x = (t | p);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      let X be non empty Subset of ( Trees D);

      :: original: Subtrees

      redefine

      func Subtrees X -> non empty Subset of ( Trees D) ;

      coherence

      proof

        ( Subtrees X) c= ( Trees D)

        proof

          let x be object;

          assume x in ( Subtrees X);

          then ex t be Element of X, p be Node of t st x = (t qua Element of ( Trees D) | p);

          hence thesis by TREES_3:def 7;

        end;

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      let X be non empty Subset of ( FinTrees D);

      :: original: Subtrees

      redefine

      func Subtrees X -> non empty Subset of ( FinTrees D) ;

      coherence

      proof

        ( Subtrees X) c= ( FinTrees D)

        proof

          let x be object;

          assume x in ( Subtrees X);

          then ex t be Element of X, p be Node of t st x = (t qua Element of ( FinTrees D) qua DecoratedTree of D | p);

          then

          reconsider x as finite DecoratedTree of D;

          ( dom x) is finite;

          hence thesis by TREES_3:def 8;

        end;

        hence thesis;

      end;

    end

    reserve X,Y for non empty constituted-DTrees set;

    theorem :: TREES_9:19

    

     Th19: x in ( Subtrees X) iff ex t be Element of X, n be Node of t st x = (t | n);

    theorem :: TREES_9:20

    t in X implies t in ( Subtrees X)

    proof

      assume t in X;

      then

      reconsider t as Element of X;

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

      (t | e) = t by Th1;

      hence thesis;

    end;

    theorem :: TREES_9:21

    X c= Y implies ( Subtrees X) c= ( Subtrees Y)

    proof

      assume

       A1: for x be object holds x in X implies x in Y;

      let x be object;

      assume x in ( Subtrees X);

      then

      consider t be Element of X, p be Node of t such that

       A2: x = (t | p);

      reconsider t as Element of Y by A1;

      reconsider p as Node of t;

      x = (t | p) by A2;

      hence thesis;

    end;

    registration

      let t be DecoratedTree;

      cluster {t} -> constituted-DTrees;

      coherence by TREES_3: 14;

    end

    theorem :: TREES_9:22

    ( Subtrees {t}) = ( Subtrees t)

    proof

      hereby

        let x be object;

        assume x in ( Subtrees {t});

        then

        consider u be Element of {t}, p be Node of u such that

         A1: x = (u | p);

        u = t by TARSKI:def 1;

        hence x in ( Subtrees t) by A1;

      end;

      let x be object;

      assume x in ( Subtrees t);

      then t in {t} & ex p be Node of t st x = (t | p) by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: TREES_9:23

    ( Subtrees X) = ( union the set of all ( Subtrees t) where t be Element of X)

    proof

      hereby

        let x be object;

        assume x in ( Subtrees X);

        then

        consider t be Element of X such that

         A1: ex p be Node of t st x = (t | p);

        ( Subtrees t) in the set of all ( Subtrees s) where s be Element of X & x in ( Subtrees t) by A1;

        hence x in ( union the set of all ( Subtrees s) where s be Element of X) by TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union the set of all ( Subtrees s) where s be Element of X);

      then

      consider Y be set such that

       A2: x in Y and

       A3: Y in the set of all ( Subtrees s) where s be Element of X by TARSKI:def 4;

      consider t be Element of X such that

       A4: Y = ( Subtrees t) by A3;

      ex p be Node of t st x = (t | p) by A2, A4;

      hence thesis;

    end;

    definition

      let X be constituted-DTrees non empty set;

      let C be set;

      :: TREES_9:def12

      func C -Subtrees X -> Subset of ( Subtrees X) equals { (t | p) where t be Element of X, p be Node of t : not p in ( Leaves ( dom t)) or (t . p) in C };

      coherence

      proof

        set W = { (t | p) where t be Element of X, p be Node of t : not p in ( Leaves ( dom t)) or (t . p) in C };

        W c= ( Subtrees X)

        proof

          let x be object;

          assume x in W;

          then ex t be Element of X, p be Node of t st x = (t | p) & ( not p in ( Leaves ( dom t)) or (t . p) in C);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: TREES_9:24

    

     Th24: x in (C -Subtrees X) iff ex t be Element of X, n be Node of t st x = (t | n) & ( not n in ( Leaves ( dom t)) or (t . n) in C);

    theorem :: TREES_9:25

    (C -Subtrees X) is empty iff for t be Element of X holds t is root & not (t . {} ) in C

    proof

      hereby

        assume

         A1: (C -Subtrees X) is empty;

        let t be Element of X;

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

        

         A2: not (t | e) in (C -Subtrees X) by A1;

        then e in ( Leaves ( dom t));

        hence t is root & not (t . {} ) in C by A2, Th4;

      end;

      assume

       A3: for t be Element of X holds t is root & not (t . {} ) in C;

      assume not (C -Subtrees X) is empty;

      then

      reconsider S = (C -Subtrees X) as non empty Subset of ( Subtrees X);

      set s = the Element of S;

      consider t be Element of X, n be Node of t such that s = (t | n) and

       A4: not n in ( Leaves ( dom t)) or (t . n) in C by Th24;

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

      t is root by A3;

      then

       A5: ( dom t) = { {} } by TREES_1: 29;

      then n = {} by TARSKI:def 1;

      then (e ^ <* 0 *>) in ( dom t) by A3, A4, TREES_1: 54;

      hence contradiction by A5, TARSKI:def 1;

    end;

    theorem :: TREES_9:26

    (C -Subtrees {t}) = (C -Subtrees t)

    proof

      hereby

        let x be object;

        assume x in (C -Subtrees {t});

        then

        consider u be Element of {t}, p be Node of u such that

         A1: x = (u | p) & ( not p in ( Leaves ( dom u)) or (u . p) in C);

        u = t by TARSKI:def 1;

        hence x in (C -Subtrees t) by A1;

      end;

      let x be object;

      assume x in (C -Subtrees t);

      then t in {t} & ex p be Node of t st x = (t | p) & ( not p in ( Leaves ( dom t)) or (t . p) in C) by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: TREES_9:27

    (C -Subtrees X) = ( union the set of all (C -Subtrees t) where t be Element of X)

    proof

      hereby

        let x be object;

        assume x in (C -Subtrees X);

        then

        consider t be Element of X such that

         A1: ex n be Node of t st x = (t | n) & ( not n in ( Leaves ( dom t)) or (t . n) in C);

        (C -Subtrees t) in the set of all (C -Subtrees s) where s be Element of X & x in (C -Subtrees t) by A1;

        hence x in ( union the set of all (C -Subtrees s) where s be Element of X) by TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union the set of all (C -Subtrees s) where s be Element of X);

      then

      consider Y be set such that

       A2: x in Y and

       A3: Y in the set of all (C -Subtrees s) where s be Element of X by TARSKI:def 4;

      consider t be Element of X such that

       A4: Y = (C -Subtrees t) by A3;

      ex p be Node of t st x = (t | p) & ( not p in ( Leaves ( dom t)) or (t . p) in C) by A2, A4;

      hence thesis;

    end;

    definition

      let X be non empty constituted-DTrees set;

      let C be set;

      :: TREES_9:def13

      func C -ImmediateSubtrees X -> Function of (C -Subtrees X), (( Subtrees X) * ) means for d be DecoratedTree st d in (C -Subtrees X) holds for p be FinSequence of ( Subtrees X) st p = (it . d) holds d = ((d . {} ) -tree p);

      existence

      proof

        defpred X[ object, object] means ex d be DecoratedTree, p be FinSequence of ( Subtrees X) st p = $2 & d = $1 & d = ((d . {} ) -tree p);

        

         A2: for x be object st x in (C -Subtrees X) holds ex y be object st y in (( Subtrees X) * ) & X[x, y]

        proof

          let x be object;

          assume x in (C -Subtrees X);

          then

          reconsider s = x as Element of ( Subtrees X);

          reconsider d = s as DecoratedTree;

          consider t be Element of X, sp be Node of t such that

           A3: s = (t | sp) by Th19;

          t is finite by A1;

          then

          consider z be set, p be DTree-yielding FinSequence such that

           A4: s = (z -tree p) by A3, Th8;

          ( rng p) c= ( Subtrees X)

          proof

            let x be object;

            

             A5: ( dom (t | sp)) = (( dom t) | sp) by TREES_2:def 10;

            assume x in ( rng p);

            then

            consider k be Nat such that

             A6: k < ( len p) & x = (p . (k + 1)) by Lm4;

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

            reconsider e = {} as Node of (s | <*k*>) by TREES_1: 22;

            

             A7: x = (s | <*k*>) by A4, A6, TREES_4:def 4;

            ( <*k*> ^ e) = <*k*> by FINSEQ_1: 34;

            then <*k*> in ( dom s) by A4, A6, A7, TREES_4: 11;

            then

            reconsider q = (sp ^ <*k*>) as Node of t by A3, A5, TREES_1:def 6;

            x = (t | q) by A3, A7, Th3;

            hence thesis;

          end;

          then

          reconsider p as FinSequence of ( Subtrees X) by FINSEQ_1:def 4;

          reconsider y = p as set;

          take y;

          thus y in (( Subtrees X) * ) by FINSEQ_1:def 11;

          take d, p;

          thus thesis by A4, TREES_4:def 4;

        end;

        consider f be Function such that

         A8: ( dom f) = (C -Subtrees X) & ( rng f) c= (( Subtrees X) * ) & for x be object st x in (C -Subtrees X) holds X[x, (f . x)] from FUNCT_1:sch 6( A2);

        reconsider f as Function of (C -Subtrees X), (( Subtrees X) * ) by A8, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        let d be DecoratedTree;

        assume d in (C -Subtrees X);

        then ex d9 be DecoratedTree, p be FinSequence of ( Subtrees X) st p = (f . d) & d9 = d & d9 = ((d9 . {} ) -tree p) by A8;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of (C -Subtrees X), (( Subtrees X) * ) such that

         A9: (for d be DecoratedTree st d in (C -Subtrees X) holds for p be FinSequence of ( Subtrees X) st p = (f1 . d) holds d = ((d . {} ) -tree p)) & for d be DecoratedTree st d in (C -Subtrees X) holds for p be FinSequence of ( Subtrees X) st p = (f2 . d) holds d = ((d . {} ) -tree p);

        now

          let x be object;

          assume

           A10: x in (C -Subtrees X);

          then

          reconsider s = x as Element of ( Subtrees X);

          reconsider p1 = (f1 . s), p2 = (f2 . s) as Element of (( Subtrees X) * ) by A10, FUNCT_2: 5;

          s = ((s . {} ) -tree p1) & s = ((s . {} ) -tree p2) by A9, A10;

          hence (f1 . x) = (f2 . x) by TREES_4: 15;

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    registration

      let t be Tree;

      cluster empty for Element of t;

      existence

      proof

         {} in t by TREES_1: 22;

        hence thesis;

      end;

    end

    theorem :: TREES_9:28

    for t be finite DecoratedTree, p be Element of ( dom t) holds ( len ( succ (t,p))) = ( len (p succ )) & ( dom ( succ (t,p))) = ( dom (p succ ))

    proof

      let t be finite DecoratedTree, p be Element of ( dom t);

      (ex q be Element of ( dom t) st q = p & ( succ (t,p)) = (t * (q succ ))) & ( rng (p succ )) c= ( dom t) by Def6;

      then ( dom ( succ (t,p))) = ( dom (p succ )) by RELAT_1: 27;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: TREES_9:29

    

     Th29: for p be FinTree-yielding FinSequence, n be empty Element of ( tree p) holds ( card ( succ n)) = ( len p)

    proof

      let p be FinTree-yielding FinSequence, n be empty Element of ( tree p);

      assume

       A1: not thesis;

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: ( card ( succ n)) < ( len p);

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

        then

        reconsider t = (p . (( card ( succ n)) + 1)) as finite Tree by TREES_3: 23;

        

         A3: (n ^ <*( card ( succ n))*>) = <*( card ( succ n))*> by FINSEQ_1: 34;

        n in t & ( <*( card ( succ n))*> ^ n) = <*( card ( succ n))*> by FINSEQ_1: 34, TREES_1: 22;

        then (n ^ <*( card ( succ n))*>) in ( tree p) by A2, A3, TREES_3:def 15;

        then (n ^ <*( card ( succ n))*>) in ( succ n);

        hence contradiction by Th7;

      end;

        suppose ( card ( succ n)) > ( len p);

        then (n ^ <*( len p)*>) in ( succ n) by Th7;

        then (n ^ <*( len p)*>) in ( tree p);

        then <*( len p)*> in ( tree p) by FINSEQ_1: 34;

        then

        consider i be Nat, q be FinSequence such that

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

         A5: <*( len p)*> = ( <*i*> ^ q) by TREES_3:def 15;

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

        .= i by A5, FINSEQ_1: 41;

        hence contradiction by A4;

      end;

    end;

    theorem :: TREES_9:30

    for t be finite DecoratedTree, x be set, p be DTree-yielding FinSequence st t = (x -tree p) holds for n be empty Element of ( dom t) holds ( succ (t,n)) = ( roots p)

    proof

      let t be finite DecoratedTree, x be set;

      let p be DTree-yielding FinSequence such that

       A1: t = (x -tree p);

      let n be empty Element of ( dom t);

      

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

      now

        let x be object;

        assume x in ( dom ( doms p));

        then

        consider i be Nat such that

         A3: x = (i + 1) & i < ( len p) by A2, Lm1;

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

        

         A4: (p . x) = (t | <*i*>) by A1, A3, TREES_4:def 4;

        n in ( dom (t | <*i*>)) & ( <*i*> ^ n) = <*i*> by FINSEQ_1: 34, TREES_1: 22;

        then

        reconsider ii = <*i*> as Node of t by A1, A3, A4, TREES_4: 11;

        x in ( dom p) by A3, Lm3;

        then (( doms p) . x) = ( dom (t | ii)) by A4, FUNCT_6: 22;

        hence (( doms p) . x) is finite Tree;

      end;

      then

      reconsider dp = ( doms p) as FinTree-yielding FinSequence by TREES_3: 23;

      

       A5: ( dom t) = ( tree dp) by A1, TREES_4: 10;

      

       A6: ex q be Element of ( dom t) st q = n & ( succ (t,n)) = (t * (q succ )) by Def6;

      ( rng (n succ )) c= ( dom t);

      then ( dom ( succ (t,n))) = ( dom (n succ )) by A6, RELAT_1: 27;

      then

       A7: ( len ( succ (t,n))) = ( len (n succ )) by FINSEQ_3: 29;

      

      then

       A8: ( len ( succ (t,n))) = ( card ( succ n)) by Def5

      .= ( len p) by A2, A5, Th29;

       A9:

      now

        let i be Nat;

        assume

         A10: i < ( len p);

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        (i + 1) in ( dom p) by Lm3, A10;

        then

         A11: {} in (( dom t) | <*ii*>) & ex T be DecoratedTree st T = (p . (i + 1)) & (( roots p) . (i + 1)) = (T . {} ) by TREES_1: 22, TREES_3:def 18;

        (p . (i + 1)) = (t | <*ii*>) by A1, A10, TREES_4:def 4;

        then

         A12: (( roots p) . (i + 1)) = (t . ( <*i*> ^ {} )) by A11, TREES_1: 22, TREES_2:def 10;

        (i + 1) in ( dom ( succ (t,n))) by A8, A10, Lm3;

        

        then (( succ (t,n)) . (i + 1)) = (t . ((n succ ) . (i + 1))) by A6, FUNCT_1: 12

        .= (t . (n ^ <*i*>)) by A7, A8, A10, Def5

        .= (t . <*i*>) by FINSEQ_1: 34;

        hence (( succ (t,n)) . (i + 1)) = (( roots p) . (i + 1)) by A12, FINSEQ_1: 34;

      end;

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

      then ( len ( roots p)) = ( len p) by FINSEQ_3: 29;

      hence thesis by A8, A9, Lm2;

    end;

    registration

      let T be finite-branching DecoratedTree, t be Node of T;

      cluster (T | t) -> finite-branching;

      coherence

      proof

        let x be Element of ( dom (T | t));

        

         A1: ( dom (T | t)) = (( dom T) | t) by TREES_2:def 10;

        then x in (( dom T) | t);

        then

        reconsider tx = (t ^ x) as Element of ( dom T) by TREES_1:def 6;

        ( dom T) = (( dom T) with-replacement (t,(( dom T) | t))) by TREES_2: 6;

        then (( succ tx),( succ x)) are_equipotent by A1, TREES_2: 37;

        then ( card ( succ x)) = ( card ( succ tx)) by CARD_1: 5;

        hence thesis;

      end;

    end

    theorem :: TREES_9:31

    for t be finite-branching DecoratedTree, p be Node of t, q be Node of (t | p) holds ( succ (t,(p ^ q))) = ( succ ((t | p),q))

    proof

      let t be finite-branching DecoratedTree, p be Node of t, q be Node of (t | p);

      

       A1: ( dom (t | p)) = (( dom t) | p) by TREES_2:def 10;

      then

      reconsider pq = (p ^ q) as Element of ( dom t) by TREES_1:def 6;

      reconsider q as Element of ( dom (t | p));

      ( dom t) = (( dom t) with-replacement (p,(( dom t) | p))) by TREES_2: 6;

      then (( succ pq),( succ q)) are_equipotent by A1, TREES_2: 37;

      then

       A2: ( card ( succ q)) = ( card ( succ pq)) by CARD_1: 5;

      

       A3: ex r be Element of ( dom (t | p)) st r = q & ( succ ((t | p),q)) = ((t | p) * (r succ )) by Def6;

      ( rng (q succ )) c= ( dom (t | p));

      then

       A4: ( dom ( succ ((t | p),q))) = ( dom (q succ )) by A3, RELAT_1: 27;

      

       A5: ex q be Element of ( dom t) st q = pq & ( succ (t,pq)) = (t * (q succ )) by Def6;

      ( rng (pq succ )) c= ( dom t);

      then

       A6: ( dom ( succ (t,pq))) = ( dom (pq succ )) by A5, RELAT_1: 27;

      

       A7: ( len (q succ )) = ( card ( succ q)) by Def5;

      

       A8: ( len (pq succ )) = ( card ( succ pq)) by Def5;

      then

       A9: ( dom (pq succ )) = ( dom (q succ )) by A7, A2, FINSEQ_3: 29;

      now

        let i be Nat;

        assume

         A10: i in ( dom (q succ ));

        then

        consider k be Nat such that

         A11: i = (k + 1) and

         A12: k < ( len (q succ )) by Lm1;

        

         A13: (q ^ <*k*>) in ( succ q) by A7, A12, Th7;

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

        

        thus (( succ (t,pq)) . i) = (t . ((pq succ ) . i)) by A5, A9, A6, A10, FUNCT_1: 12

        .= (t . (pq ^ <*k*>)) by A8, A7, A2, A11, A12, Def5

        .= (t . (p ^ (q ^ <*k*>))) by FINSEQ_1: 32

        .= ((t | p) . (q ^ <*k*>)) by A1, A13, TREES_2:def 10

        .= ((t | p) . ((q succ ) . i)) by A11, A12, Def5

        .= (( succ ((t | p),q)) . i) by A3, A4, A10, FUNCT_1: 12;

      end;

      hence thesis by A9, A6, A4;

    end;

    begin

    theorem :: TREES_9:32

    

     Th32: for n be Nat, r be FinSequence holds ex q be FinSequence st q = (r | ( Seg n)) & q is_a_prefix_of r

    proof

      let n be Nat, r be FinSequence;

      (r | ( Seg n)) is FinSequence by FINSEQ_1: 15;

      then

      consider q be FinSequence such that

       A1: q = (r | ( Seg n));

      q is_a_prefix_of r by A1, TREES_1:def 1;

      hence thesis by A1;

    end;

    theorem :: TREES_9:33

    

     Th33: for D be non empty set, r be FinSequence of D, r1,r2 be FinSequence, k be Nat st (k + 1) <= ( len r) & r1 = (r | ( Seg (k + 1))) & r2 = (r | ( Seg k)) holds ex x be Element of D st r1 = (r2 ^ <*x*>)

    proof

      let D be non empty set, r be FinSequence of D, r1,r2 be FinSequence, k be Nat;

      assume that

       A1: (k + 1) <= ( len r) and

       A2: r1 = (r | ( Seg (k + 1))) and

       A3: r2 = (r | ( Seg k));

      k < ( len r) by A1, NAT_1: 13;

      then

       A4: ( len r2) = k by A3, FINSEQ_1: 17;

      r2 is_a_prefix_of r by A3, TREES_1:def 1;

      then

       A5: ex q2 be FinSequence st r = (r2 ^ q2) by TREES_1: 1;

      then

      reconsider r99 = r2 as FinSequence of D by FINSEQ_1: 36;

      r1 is_a_prefix_of r by A2, TREES_1:def 1;

      then

       A6: ex q1 be FinSequence st r = (r1 ^ q1) by TREES_1: 1;

      then

      reconsider r9 = r1 as FinSequence of D by FINSEQ_1: 36;

      

       A7: ( len r1) = (k + 1) by A1, A2, FINSEQ_1: 17;

       A8:

      now

        assume r9 is_a_prefix_of r99;

        then (k + 1) <= (k + 0 ) by A7, A4, NAT_1: 43;

        hence contradiction by XREAL_1: 6;

      end;

      (r9,r99) are_c=-comparable by A6, A5, TREES_A: 1;

      then r99 is_a_prefix_of r9 by A8;

      then

      consider s be FinSequence such that

       A9: r9 = (r99 ^ s) by TREES_1: 1;

      reconsider s as FinSequence of D by A9, FINSEQ_1: 36;

      

       A10: ( len s) = 1

      proof

        consider m be Nat such that

         A11: m = ( len s);

        (k + 1) = (k + m) by A7, A4, A9, A11, FINSEQ_1: 22;

        hence thesis by A11;

      end;

      consider x be set such that

       A12: x = (s . 1);

      1 in {1} by TARSKI:def 1;

      then 1 in ( dom s) by A10, FINSEQ_1: 2, FINSEQ_1:def 3;

      then

       A13: x in ( rng s) by A12, FUNCT_1:def 3;

      s = <*x*> by A10, A12, FINSEQ_1: 40;

      hence thesis by A9, A13;

    end;

    theorem :: TREES_9:34

    

     Th34: for D be non empty set, r be FinSequence of D, r1 be FinSequence st 1 <= ( len r) & r1 = (r | ( Seg 1)) holds ex x be Element of D st r1 = <*x*>

    proof

      let D be non empty set, r be FinSequence of D, r1 be FinSequence;

      assume that

       A1: 1 <= ( len r) and

       A2: r1 = (r | ( Seg 1));

      consider x be set such that

       A3: x = (r1 . 1);

      1 in {1} by TARSKI:def 1;

      then 1 in ( dom r1) by A1, A2, FINSEQ_1: 2, FINSEQ_1: 17;

      then

       A4: x in ( rng r1) by A3, FUNCT_1:def 3;

      ( len r1) = 1 by A1, A2, FINSEQ_1: 17;

      then

       A5: r1 = <*x*> by A3, FINSEQ_1: 40;

      r1 is_a_prefix_of r by A2, TREES_1:def 1;

      then ex q1 be FinSequence st r = (r1 ^ q1) by TREES_1: 1;

      then

      reconsider r9 = r1 as FinSequence of D by FINSEQ_1: 36;

      ( rng r9) c= D;

      hence thesis by A5, A4;

    end;

    reserve T for DecoratedTree,

p for FinSequence of NAT ;

    theorem :: TREES_9:35

    (T . p) = ((T | p) . {} )

    proof

      ( <*> NAT ) in (( dom T) | p) by TREES_1: 22;

      

      then ((T | p) . ( <*> NAT )) = (T . (p ^ ( <*> NAT ))) by TREES_2:def 10

      .= (T . p) by FINSEQ_1: 34;

      hence thesis;

    end;

    reserve T for finite-branching DecoratedTree,

t for Element of ( dom T),

x for FinSequence,

n,m for Nat;

    theorem :: TREES_9:36

    

     Th36: ( succ (T,t)) = (T * (t succ ))

    proof

      ex q be Element of ( dom T) st q = t & ( succ (T,t)) = (T * (q succ )) by Def6;

      hence thesis;

    end;

    theorem :: TREES_9:37

    

     Th37: ( dom (T * (t succ ))) = ( dom (t succ ))

    proof

      ( rng (t succ )) c= ( dom T);

      hence thesis by RELAT_1: 27;

    end;

    theorem :: TREES_9:38

    

     Th38: ( dom ( succ (T,t))) = ( dom (t succ ))

    proof

      

      thus ( dom ( succ (T,t))) = ( dom (T * (t succ ))) by Th36

      .= ( dom (t succ )) by Th37;

    end;

    theorem :: TREES_9:39

    

     Th39: (t ^ <*n*>) in ( dom T) iff (n + 1) in ( dom (t succ ))

    proof

      now

        assume (t ^ <*n*>) in ( dom T);

        then (t ^ <*n*>) in ( succ t);

        then n < ( card ( succ t)) by Th7;

        then n < ( len (t succ )) by Def5;

        then

         A1: (n + 1) <= ( len (t succ )) by NAT_1: 13;

        ( 0 + 1) <= (n + 1) by XREAL_1: 6;

        then (n + 1) in ( Seg ( len (t succ ))) by A1, FINSEQ_1: 1;

        hence (n + 1) in ( dom (t succ )) by FINSEQ_1:def 3;

      end;

      hence (t ^ <*n*>) in ( dom T) implies (n + 1) in ( dom (t succ ));

      assume (n + 1) in ( dom (t succ ));

      then (n + 1) in ( Seg ( len (t succ ))) by FINSEQ_1:def 3;

      then (n + 1) <= ( len (t succ )) by FINSEQ_1: 1;

      then n < ( len (t succ )) by NAT_1: 13;

      then n < ( card ( succ t)) by Def5;

      then (t ^ <*n*>) in ( succ t) by Th7;

      hence thesis;

    end;

    theorem :: TREES_9:40

    

     Th40: for T, x, n st (x ^ <*n*>) in ( dom T) holds (T . (x ^ <*n*>)) = (( succ (T,x)) . (n + 1))

    proof

      let T, x, n;

      assume

       A1: (x ^ <*n*>) in ( dom T);

      x is_a_prefix_of (x ^ <*n*>) by TREES_1: 1;

      then x in ( dom T) by A1, TREES_1: 20;

      then

      consider q be Element of ( dom T) such that

       A2: q = x and

       A3: ( succ (T,x)) = (T * (q succ )) by Def6;

      

       A4: (n + 1) in ( dom (q succ )) by A1, A2, Th39;

      then (n + 1) in ( Seg ( len (q succ ))) by FINSEQ_1:def 3;

      then (n + 1) <= ( len (q succ )) by FINSEQ_1: 1;

      then

       A5: n < ( len (q succ )) by NAT_1: 13;

      (n + 1) in ( dom (T * (q succ ))) by A4, Th37;

      

      then (( succ (T,x)) . (n + 1)) = (T . ((q succ ) . (n + 1))) by A3, FUNCT_1: 12

      .= (T . (x ^ <*n*>)) by A2, A5, Def5;

      hence thesis;

    end;

    reserve x,x9 for Element of ( dom T),

y9 for set;

    theorem :: TREES_9:41

    x9 in ( succ x) implies (T . x9) in ( rng ( succ (T,x)))

    proof

      assume x9 in ( succ x);

      then

      consider n such that

       A1: x9 = (x ^ <*n*>) and (x ^ <*n*>) in ( dom T);

      

       A2: (T . x9) = (( succ (T,x)) . (n + 1)) by A1, Th40;

      ( dom ( succ (T,x))) = ( dom (T * (x succ ))) by Th36

      .= ( dom (x succ )) by Th37;

      then (n + 1) in ( dom ( succ (T,x))) by A1, Th39;

      hence thesis by A2, FUNCT_1:def 3;

    end;

    theorem :: TREES_9:42

    y9 in ( rng ( succ (T,x))) implies ex x9 st y9 = (T . x9) & x9 in ( succ x)

    proof

      consider k be Nat such that

       A1: ( dom ( succ (T,x))) = ( Seg k) by FINSEQ_1:def 2;

      assume y9 in ( rng ( succ (T,x)));

      then

      consider n9 be object such that

       A2: n9 in ( dom ( succ (T,x))) and

       A3: y9 = (( succ (T,x)) . n9) by FUNCT_1:def 3;

      ( Seg k) = { m where m be Nat : 1 <= m & m <= k } by FINSEQ_1:def 1;

      then

      consider m9 be Nat such that

       A4: n9 = m9 and

       A5: 1 <= m9 and m9 <= k by A2, A1;

      m9 <> 0 by A5;

      then

      consider n be Nat such that

       A6: (n + 1) = m9 by NAT_1: 6;

      reconsider n as Nat;

      (n + 1) in ( dom (x succ )) by A2, A4, A6, Th38;

      then (x ^ <*n*>) in ( dom T) by Th39;

      then

      consider x9 such that

       A7: x9 = (x ^ <*n*>);

      

       A8: x9 in ( succ x) by A7;

      y9 = (T . x9) by A3, A4, A6, A7, Th40;

      hence thesis by A8;

    end;

    reserve n,k1,k2,l,k,m for Nat,

x,y for set;

    scheme :: TREES_9:sch2

    ExDecTrees { D() -> non empty set , d() -> Element of D() , G( object) -> FinSequence of D() } :

ex T be finite-branching DecoratedTree of D() st (T . {} ) = d() & for t be Element of ( dom T), w be Element of D() st w = (T . t) holds ( succ (T,t)) = G(w);

      defpred P[ object, object] means (( len G($1)) = 0 & $2 = {} ) or ( len G($1)) <> 0 & ex m st (m + 1) = ( len G($1)) & $2 = ( { 0 } \/ ( Seg m));

      

       A1: for x be object st x in D() holds ex y be object st P[x, y]

      proof

        let x be object such that x in D();

        per cases ;

          suppose ( len G(x)) = 0 ;

          hence thesis;

        end;

          suppose ( len G(x)) <> 0 ;

          then

          consider m be Nat such that

           A2: (m + 1) = ( len G(x)) by NAT_1: 6;

          reconsider m as Nat;

          ex y st y = ( { 0 } \/ ( Seg m));

          hence thesis by A2;

        end;

      end;

      ex F be Function st ( dom F) = D() & for x be object st x in D() holds P[x, (F . x)] from CLASSES1:sch 1( A1);

      then

      consider F be Function such that

       A3: for x be object st x in D() holds ( len G(x)) = 0 & (F . x) = {} or ( len G(x)) <> 0 & ex m st (m + 1) = ( len G(x)) & (F . x) = ( { 0 } \/ ( Seg m));

      deffunc F( set) = (F . $1);

      

       A4: for k, x st x in D() holds k in F(x) iff (k + 1) in ( Seg ( len G(x)))

      proof

        let k, x such that

         A5: x in D();

        now

          assume

           A6: k in F(x);

          then

          consider m such that

           A7: (m + 1) = ( len G(x)) and

           A8: (F . x) = ( { 0 } \/ ( Seg m)) by A3, A5;

           0 <= k & k <= m

          proof

            per cases by A6, A8, XBOOLE_0:def 3;

              suppose k in { 0 };

              then k = 0 by TARSKI:def 1;

              hence thesis;

            end;

              suppose

               A9: k in ( Seg m);

              thus thesis by A9, FINSEQ_1: 1;

            end;

          end;

          then ( 0 + 1) <= (k + 1) & (k + 1) <= (m + 1) by XREAL_1: 6;

          hence (k + 1) in ( Seg ( len G(x))) by A7, FINSEQ_1: 1;

        end;

        hence k in F(x) implies (k + 1) in ( Seg ( len G(x)));

        assume

         A10: (k + 1) in ( Seg ( len G(x)));

        then ( len G(x)) <> 0 ;

        then

        consider m such that

         A11: (m + 1) = ( len G(x)) and

         A12: (F . x) = ( { 0 } \/ ( Seg m)) by A3, A5;

        k in ( { 0 } \/ ( Seg m))

        proof

          per cases ;

            suppose k = 0 ;

            then k in { 0 } by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose k <> 0 ;

            then 0 < k;

            then

             A13: ( 0 + 1) <= k by NAT_1: 13;

            (k + 1) <= ( len G(x)) by A10, FINSEQ_1: 1;

            then k <= m by A11, XREAL_1: 6;

            then k in ( Seg m) by A13, FINSEQ_1: 1;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence thesis by A12;

      end;

      

       A14: for x be set, t be Element of ( dom T) st x in D() holds { (t ^ <*k*>) : k in F(x) } = { (t ^ <*m*>) : (m + 1) in ( Seg ( len G(x))) }

      proof

        let x be set, t be Element of ( dom T) such that

         A15: x in D();

        thus { (t ^ <*k*>) : k in F(x) } c= { (t ^ <*m*>) : (m + 1) in ( Seg ( len G(x))) }

        proof

          let y be object;

          assume y in { (t ^ <*k*>) : k in F(x) };

          then

          consider k such that

           A16: y = (t ^ <*k*>) and

           A17: k in F(x);

          (k + 1) in ( Seg ( len G(x))) by A4, A15, A17;

          hence thesis by A16;

        end;

        thus { (t ^ <*m*>) : (m + 1) in ( Seg ( len G(x))) } c= { (t ^ <*k*>) : k in F(x) }

        proof

          let y be object;

          assume y in { (t ^ <*m*>) : (m + 1) in ( Seg ( len G(x))) };

          then

          consider m such that

           A18: y = (t ^ <*m*>) and

           A19: (m + 1) in ( Seg ( len G(x)));

          m in F(x) by A4, A15, A19;

          hence thesis by A18;

        end;

      end;

      defpred P[ set, set] means ex x, n st x in D() & $1 = [x, n] & (n in F(x) & $2 = (G(x) . (n + 1)) or not n in F(x) & $2 = d());

      

       A20: for c be Element of [:D(), NAT :] holds ex y be Element of D() st P[c, y]

      proof

        let c be Element of [:D(), NAT :];

        (c `1 ) in D() & (c `2 ) in NAT by MCART_1: 10;

        then

        consider x be Element of D(), n be Nat such that

         A21: x = (c `1 ) & n = (c `2 );

        

         A22: c = [x, n] by A21, MCART_1: 21;

        per cases ;

          suppose

           A23: n in F(x);

          then (n + 1) in ( Seg ( len G(x))) by A4;

          then (n + 1) in ( dom G(x)) by FINSEQ_1:def 3;

          then

           A24: (G(x) . (n + 1)) in ( rng G(x)) by FUNCT_1:def 3;

          thus thesis by A22, A23, A24;

        end;

          suppose not n in F(x);

          hence thesis by A22;

        end;

      end;

      ex S be Function of [:D(), NAT :], D() st for c be Element of [:D(), NAT :] holds P[c, (S . c)] from FUNCT_2:sch 3( A20);

      then

      consider S be Function of [:D(), NAT :], D() such that

       A25: for c be Element of [:D(), NAT :] holds P[c, (S . c)];

      

       A26: for n, x, m st (m + 1) = ( len G(x)) & x in D() holds n in F(x) iff 0 <= n & n <= m

      proof

        let n, x, m such that

         A27: (m + 1) = ( len G(x)) and

         A28: x in D();

        thus n in F(x) implies 0 <= n & n <= m

        proof

          

           A29: ex k st (k + 1) = ( len G(x)) & F(x) = ( { 0 } \/ ( Seg k)) by A3, A27, A28;

          assume

           A30: n in F(x);

          per cases by A27, A30, A29, XBOOLE_0:def 3;

            suppose n in { 0 };

            then n = 0 by TARSKI:def 1;

            hence thesis;

          end;

            suppose

             A31: n in ( Seg m);

            thus thesis by A31, FINSEQ_1: 1;

          end;

        end;

        thus 0 <= n & n <= m implies n in F(x)

        proof

          assume that 0 <= n and

           A32: n <= m;

          

           A33: ex k st (k + 1) = ( len G(x)) & F(x) = ( { 0 } \/ ( Seg k)) by A3, A27, A28;

          per cases ;

            suppose n = 0 ;

            then n in { 0 } by TARSKI:def 1;

            hence thesis by A33, XBOOLE_0:def 3;

          end;

            suppose n <> 0 ;

            then 0 < n;

            then ( 0 + 1) <= n by NAT_1: 13;

            then n in ( Seg m) by A32, FINSEQ_1: 1;

            hence thesis by A27, A33, XBOOLE_0:def 3;

          end;

        end;

      end;

      

       A34: for d be Element of D(), k1, k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d)

      proof

        let d be Element of D(), k1, k2;

        assume that

         A35: k1 <= k2 and

         A36: k2 in F(d);

        ex m st (m + 1) = ( len G(d)) & (F . d) = ( { 0 } \/ ( Seg m)) by A3, A36;

        then

        consider m such that

         A37: (m + 1) = ( len G(d));

        k2 <= m by A26, A36, A37;

        then 0 <= k1 & k1 <= m by A35, XXREAL_0: 2;

        hence thesis by A26, A37;

      end;

      consider T be DecoratedTree of D() such that

       A38: (T . {} ) = d() & for t be Element of ( dom T) holds ( succ t) = { (t ^ <*k*>) : k in F(.) } & for n st n in F(.) holds (T . (t ^ <*n*>)) = (S . ((T . t),n)) from TREES_2:sch 8( A34);

      for t be Element of ( dom T) holds ( succ t) is finite

      proof

        let t be Element of ( dom T);

        defpred P[ set, object] means ex m st (m + 1) = $1 & $2 = (t ^ <*m*>);

        

         A39: for k be Nat st k in ( Seg ( len G(.))) holds ex x be object st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len G(.)));

          then k <> 0 by FINSEQ_1: 1;

          then

          consider m be Nat such that

           A40: (m + 1) = k by NAT_1: 6;

          reconsider m as Nat;

          ex x st x = (t ^ <*m*>);

          hence thesis by A40;

        end;

        ex L be FinSequence st ( dom L) = ( Seg ( len G(.))) & for k be Nat st k in ( Seg ( len G(.))) holds P[k, (L . k)] from FINSEQ_1:sch 1( A39);

        then

        consider L be FinSequence such that

         A41: ( dom L) = ( Seg ( len G(.))) and

         A42: for k be Nat st k in ( Seg ( len G(.))) holds P[k, (L . k)];

        

         A43: for k st 1 <= (k + 1) & (k + 1) <= ( len G(.)) holds (L . (k + 1)) = (t ^ <*k*>)

        proof

          let k;

          assume 1 <= (k + 1) & (k + 1) <= ( len G(.));

          then (k + 1) in ( Seg ( len G(.))) by FINSEQ_1: 1;

          then ex m st (m + 1) = (k + 1) & (L . (k + 1)) = (t ^ <*m*>) by A42;

          hence thesis;

        end;

        

         A44: ( succ t) = { (t ^ <*k*>) : k in F(.) } by A38;

        ( succ t) c= ( rng L)

        proof

          let x be object;

          assume x in ( succ t);

          then

          consider k such that

           A45: x = (t ^ <*k*>) and

           A46: k in F(.) by A44;

          

           A47: (k + 1) in ( Seg ( len G(.))) by A4, A46;

          then 1 <= (k + 1) & (k + 1) <= ( len G(.)) by FINSEQ_1: 1;

          then (L . (k + 1)) = (t ^ <*k*>) by A43;

          hence thesis by A41, A45, A47, FUNCT_1:def 3;

        end;

        hence thesis;

      end;

      then ( dom T) is finite-branching;

      then

      reconsider T as finite-branching DecoratedTree of D() by Def4;

      

       A48: for n, x st x in D() & n in F(x) holds (S . (x,n)) = (G(x) . (n + 1))

      proof

        let n, x such that

         A49: x in D() and

         A50: n in F(x);

        

         A51: n in NAT by ORDINAL1:def 12;

         [x, n] in [:D(), NAT :] by A49, ZFMISC_1:def 2, A51;

        then

        consider c be Element of [:D(), NAT :] such that

         A52: c = [x, n];

        consider x9 be set, n9 be Nat such that x9 in D() and

         A53: c = [x9, n9] and

         A54: n9 in F(x9) & (S . c) = (G(x9) . (n9 + 1)) or not n9 in F(x9) & (S . c) = d() by A25;

        x9 = x by A52, A53, XTUPLE_0: 1;

        hence thesis by A50, A52, A53, A54, XTUPLE_0: 1;

      end;

      now

        let t be Element of ( dom T), w be Element of D() such that

         A55: w = (T . t);

        ( succ t) = { (t ^ <*k*>) : k in F(w) } by A38, A55;

        then

         A56: ( succ t) = { (t ^ <*k*>) : (k + 1) in ( Seg ( len G(w))) } by A14;

        

         A57: ( dom G(w)) = ( Seg ( len G(w))) by FINSEQ_1:def 3;

        

         A58: ( dom (t succ )) = ( Seg ( len (t succ ))) by FINSEQ_1:def 3;

        

         A59: ( dom (t succ )) c= ( dom G(w))

        proof

          let n9 be object;

          

           A60: ( Seg ( len (t succ ))) = { k where k be Nat : 1 <= k & k <= ( len (t succ )) } by FINSEQ_1:def 1;

          assume n9 in ( dom (t succ ));

          then

          consider m be Nat such that

           A61: n9 = m and

           A62: 1 <= m and

           A63: m <= ( len (t succ )) by A58, A60;

           0 <> m by A62;

          then

          consider n be Nat such that

           A64: m = (n + 1) by NAT_1: 6;

          reconsider n as Nat;

          (n + 1) in ( dom (t succ )) by A58, A60, A62, A63, A64;

          then (t ^ <*n*>) in ( dom T) by Th39;

          then (t ^ <*n*>) in ( succ t);

          then

          consider k such that

           A65: (t ^ <*k*>) = (t ^ <*n*>) and

           A66: (k + 1) in ( Seg ( len G(w))) by A56;

           <*k*> = <*n*> by A65, FINSEQ_1: 33;

          hence thesis by A57, A61, A64, A66, TREES_1: 5;

        end;

        ( dom G(w)) c= ( dom (t succ ))

        proof

          let n9 be object;

          

           A67: ( Seg ( len G(w))) = { k where k be Nat : 1 <= k & k <= ( len G(w)) } by FINSEQ_1:def 1;

          assume n9 in ( dom G(w));

          then

          consider m be Nat such that

           A68: n9 = m and

           A69: 1 <= m and

           A70: m <= ( len G(w)) by A57, A67;

           0 <> m by A69;

          then

          consider n be Nat such that

           A71: m = (n + 1) by NAT_1: 6;

          reconsider n as Nat;

          (n + 1) in ( Seg ( len G(w))) by A67, A69, A70, A71;

          then (t ^ <*n*>) in ( succ t) by A56;

          hence thesis by A68, A71, Th39;

        end;

        then

         A72: ( dom G(w)) = ( dom (t succ )) by A59;

        then

         A73: ( dom ( succ (T,t))) = ( dom G(w)) by Th38;

        for m be Nat st m in ( dom ( succ (T,t))) holds (( succ (T,t)) . m) = (G(w) . m)

        proof

          let m be Nat;

          

           A74: ( Seg ( len G(w))) = { k where k be Nat : 1 <= k & k <= ( len G(w)) } by FINSEQ_1:def 1;

          assume

           A75: m in ( dom ( succ (T,t)));

          then

           A76: m in ( Seg ( len G(w))) by A73, FINSEQ_1:def 3;

          then ( len G(w)) <> 0 ;

          then

          consider l such that

           A77: (l + 1) = ( len G(.)) and

           A78: (F . (T . t)) = ( { 0 } \/ ( Seg l)) by A3, A55;

          consider k be Nat such that

           A79: m = k and

           A80: 1 <= k and

           A81: k <= ( len G(w)) by A76, A74;

           0 <> k by A80;

          then

          consider n be Nat such that

           A82: m = (n + 1) by A79, NAT_1: 6;

          reconsider n as Nat;

          

           A83: n <= l by A55, A79, A81, A82, A77, XREAL_1: 6;

          

           A84: n in ( { 0 } \/ ( Seg l))

          proof

            per cases ;

              suppose n = 0 ;

              then n in { 0 } by TARSKI:def 1;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose n <> 0 ;

              then 0 < n;

              then ( 0 + 1) <= n by NAT_1: 13;

              then n in ( Seg l) by A83, FINSEQ_1: 1;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          (n + 1) in ( dom (t succ )) by A75, A82, Th38;

          then (t ^ <*n*>) in ( dom T) by Th39;

          

          then (( succ (T,t)) . (n + 1)) = (T . (t ^ <*n*>)) by Th40

          .= (S . ((T . t),n)) by A38, A78, A84

          .= (G(w) . (n + 1)) by A48, A55, A78, A84;

          hence thesis by A82;

        end;

        hence ( succ (T,t)) = G(w) by A72, Th38;

      end;

      hence thesis by A38;

    end;

    theorem :: TREES_9:43

    

     Th43: for T be Tree, t be Element of T holds ( ProperPrefixes t) is finite Chain of T

    proof

      let T be Tree, t be Element of T;

      ( ProperPrefixes t) c= T & for p,q be FinSequence of NAT st p in ( ProperPrefixes t) & q in ( ProperPrefixes t) holds (p,q) are_c=-comparable by TREES_1: 18, TREES_1:def 3;

      hence thesis by TREES_2:def 3;

    end;

    theorem :: TREES_9:44

    

     Th44: for T be Tree holds (T -level 0 ) = { {} }

    proof

      let T be Tree;

      

       A1: { {} } c= { w where w be Element of T : ( len w) = 0 }

      proof

        let x be object;

        assume x in { {} };

        then

         A2: x = {} by TARSKI:def 1;

         {} in T by TREES_1: 22;

        then

        consider t be Element of T such that

         A3: t = {} ;

        ( len t) = 0 by A3;

        hence thesis by A2, A3;

      end;

      { w where w be Element of T : ( len w) = 0 } c= { {} }

      proof

        let x be object;

        assume x in { w where w be Element of T : ( len w) = 0 };

        then

        consider w be Element of T such that

         A4: w = x and

         A5: ( len w) = 0 ;

        w = {} by A5;

        hence thesis by A4, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: TREES_9:45

    

     Th45: for T be Tree holds (T -level (n + 1)) = ( union { ( succ w) where w be Element of T : ( len w) = n })

    proof

      let T be Tree;

      thus (T -level (n + 1)) c= ( union { ( succ w) where w be Element of T : ( len w) = n })

      proof

        let x be object;

        assume

         A1: x in (T -level (n + 1));

        then

        reconsider t = x as Element of T;

        (t | ( Seg n)) is FinSequence of NAT by FINSEQ_1: 18;

        then

        consider s be FinSequence of NAT such that

         A2: s = (t | ( Seg n));

        s is_a_prefix_of t by A2, TREES_1:def 1;

        then

        reconsider s as Element of T by TREES_1: 20;

        

         A3: ex w9 be Element of T st t = w9 & ( len w9) = (n + 1) by A1;

        (n + 0 ) <= (n + 1) by XREAL_1: 6;

        then ( len s) = n by A3, A2, FINSEQ_1: 17;

        then

         A4: ( succ s) in { ( succ w) where w be Element of T : ( len w) = n };

        ( Seg (n + 1)) = ( dom t) by A3, FINSEQ_1:def 3;

        then t = (t | ( Seg (n + 1)));

        then ex m be Element of NAT st t = (s ^ <*m*>) by A3, A2, Th33;

        then t in ( succ s);

        hence thesis by A4, TARSKI:def 4;

      end;

      thus ( union { ( succ w) where w be Element of T : ( len w) = n }) c= (T -level (n + 1))

      proof

        set X = { ( succ w) where w be Element of T : ( len w) = n };

        let x be object;

        assume x in ( union X);

        then

        consider Y be set such that

         A5: x in Y and

         A6: Y in X by TARSKI:def 4;

        consider w be Element of T such that

         A7: Y = ( succ w) and

         A8: ( len w) = n by A6;

        reconsider t = x as Element of T by A5, A7;

        consider k such that

         A9: t = (w ^ <*k*>) and (w ^ <*k*>) in T by A5, A7;

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

        then ( len t) = (n + 1) by A8, A9, FINSEQ_1: 22;

        hence thesis;

      end;

    end;

    theorem :: TREES_9:46

    

     Th46: for T be finite-branching Tree, n be Nat holds (T -level n) is finite

    proof

      let T be finite-branching Tree;

      defpred Q[ Nat] means (T -level $1) is finite;

      

       A1: for n st Q[n] holds Q[(n + 1)]

      proof

        let n such that

         A2: (T -level n) is finite;

        set X = { ( succ w) where w be Element of T : ( len w) = n };

        

         A3: X is finite

        proof

          defpred P[ object, object] means ex w be Element of T st $1 = w & $2 = ( succ w);

          

           A4: for x be object st x in (T -level n) holds ex y be object st P[x, y]

          proof

            let x be object;

            assume x in (T -level n);

            then

            consider w be Element of T such that

             A5: w = x;

            consider y such that

             A6: y = ( succ w);

            take y, w;

            thus thesis by A5, A6;

          end;

          consider f be Function such that

           A7: ( dom f) = (T -level n) & for x be object st x in (T -level n) holds P[x, (f . x)] from CLASSES1:sch 1( A4);

          

           A8: X c= ( rng f)

          proof

            let x be object;

            assume x in X;

            then

            consider w be Element of T such that

             A9: x = ( succ w) and

             A10: ( len w) = n;

            

             A11: w in (T -level n) by A10;

            then ex w9 be Element of T st w = w9 & (f . w) = ( succ w9) by A7;

            hence thesis by A7, A9, A11, FUNCT_1:def 3;

          end;

          ( card ( rng f)) c= ( card ( dom f)) by CARD_1: 12;

          then ( rng f) is finite by A2, A7;

          hence thesis by A8;

        end;

        

         A12: for Y be set st Y in X holds Y is finite

        proof

          let Y be set;

          assume Y in X;

          then ex w be Element of T st Y = ( succ w) & ( len w) = n;

          hence thesis;

        end;

        (T -level (n + 1)) = ( union { ( succ w) where w be Element of T : ( len w) = n }) by Th45;

        hence thesis by A3, A12, FINSET_1: 7;

      end;

      

       A13: Q[ 0 ] by Th44;

      thus for n holds Q[n] from NAT_1:sch 2( A13, A1);

    end;

    theorem :: TREES_9:47

    

     Th47: for T be finite-branching Tree holds T is finite iff ex n be Nat st (T -level n) = {}

    proof

      let T be finite-branching Tree;

      deffunc F( Nat) = (T -level $1);

      now

        assume

         A1: T is finite;

        now

          assume

           A2: not ex n be Nat st (T -level n) = {} ;

          

           A3: for n holds ex C be finite Chain of T st ( card C) = n

          proof

            let n;

            (T -level n) <> {} by A2;

            then

            consider t be object such that

             A4: t in (T -level n) by XBOOLE_0:def 1;

            consider w be Element of T such that t = w and

             A5: ( len w) = n by A4;

            ( ProperPrefixes w) is finite Chain of T by Th43;

            then

            consider C be finite Chain of T such that

             A6: C = ( ProperPrefixes w);

            ( card C) = n by A5, A6, TREES_1: 35;

            hence thesis;

          end;

          for t be Element of T holds ( succ t) is finite;

          then ex C be Chain of T st not C is finite by A3, TREES_2: 29;

          hence contradiction by A1;

        end;

        hence ex n be Nat st (T -level n) = {} ;

      end;

      hence T is finite implies ex n be Nat st (T -level n) = {} ;

      given n such that

       A7: (T -level n) = {} ;

      set X = { F(m) where m be Nat : m <= n };

      

       A8: T c= ( union X)

      proof

        let x be object;

        assume x in T;

        then

        reconsider t = x as Element of T;

        consider m such that

         A9: m = ( len t);

        

         A10: t in F(m) by A9;

        ( len t) < n

        proof

          consider q be FinSequence such that

           A11: q = (t | ( Seg n)) and

           A12: q is_a_prefix_of t by Th32;

          assume n <= ( len t);

          then

           A13: ( len q) = n by A11, FINSEQ_1: 17;

          reconsider q as Element of T by A12, TREES_1: 20;

          q in (T -level n) by A13;

          hence contradiction by A7;

        end;

        then F(m) in X by A9;

        hence thesis by A10, TARSKI:def 4;

      end;

      

       A14: X is finite

      proof

        defpred P[ set, object] means ex l, m st m = (l + 1) & $1 = m & F(l) = $2;

        

         A15: for k be Nat st k in ( Seg (n + 1)) holds ex x be object st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg (n + 1));

          then 0 <> k by FINSEQ_1: 1;

          then

          consider l be Nat such that

           A16: k = (l + 1) by NAT_1: 6;

          reconsider l as Nat;

          consider x such that

           A17: x = F(l);

          take x, l, (l + 1);

          thus thesis by A16, A17;

        end;

        consider p be FinSequence such that

         A18: ( dom p) = ( Seg (n + 1)) & for k be Nat st k in ( Seg (n + 1)) holds P[k, (p . k)] from FINSEQ_1:sch 1( A15);

        

         A19: for k st (k + 1) in ( Seg (n + 1)) holds (p . (k + 1)) = F(k)

        proof

          let k;

          assume (k + 1) in ( Seg (n + 1));

          then ex l, m st m = (l + 1) & (k + 1) = m & F(l) = (p . (k + 1)) by A18;

          hence thesis;

        end;

        X c= ( rng p)

        proof

          let y be object;

          assume y in X;

          then

          consider m such that

           A20: y = F(m) and

           A21: m <= n;

          

           A22: ( 0 + 1) <= (m + 1) by XREAL_1: 6;

          (m + 1) <= (n + 1) by A21, XREAL_1: 6;

          then

           A23: (m + 1) in ( Seg (n + 1)) by A22, FINSEQ_1: 1;

          then (p . (m + 1)) = F(m) by A19;

          hence thesis by A18, A20, A23, FUNCT_1:def 3;

        end;

        hence thesis;

      end;

      for Y be set st Y in X holds Y is finite

      proof

        let Y be set;

        assume Y in X;

        then ex m st Y = F(m) & m <= n;

        hence thesis by Th46;

      end;

      then ( union X) is finite by A14, FINSET_1: 7;

      hence thesis by A8;

    end;

    theorem :: TREES_9:48

    

     Th48: for T be finite-branching Tree st not T is finite holds ex C be Chain of T st not C is finite

    proof

      let T be finite-branching Tree such that

       A1: not T is finite;

      

       A2: for n holds ex C be finite Chain of T st ( card C) = n

      proof

        let n;

        (T -level n) <> {} by A1, Th47;

        then

        consider t be object such that

         A3: t in (T -level n) by XBOOLE_0:def 1;

        

         A4: ex w be Element of T st t = w & ( len w) = n by A3;

        reconsider t as Element of T by A3;

        ( ProperPrefixes t) is finite Chain of T by Th43;

        then

        consider C be finite Chain of T such that

         A5: C = ( ProperPrefixes t);

        ( card C) = n by A4, A5, TREES_1: 35;

        hence thesis;

      end;

      for t be Element of T holds ( succ t) is finite;

      hence thesis by A2, TREES_2: 29;

    end;

    theorem :: TREES_9:49

    

     Th49: for T be finite-branching Tree st not T is finite holds ex B be Branch of T st not B is finite

    proof

      let T be finite-branching Tree;

      assume not T is finite;

      then

      consider C be Chain of T such that

       A1: not C is finite by Th48;

      consider B be Branch of T such that

       A2: C c= B by TREES_2: 28;

       not B is finite by A1, A2;

      hence thesis;

    end;

    theorem :: TREES_9:50

    

     Th50: for T be Tree, C be Chain of T, t be Element of T st t in C & not C is finite holds ex t9 be Element of T st t9 in C & t is_a_proper_prefix_of t9

    proof

      let T be Tree, C be Chain of T, t be Element of T such that

       A1: t in C and

       A2: not C is finite;

      now

        assume

         A3: not ex t9 be Element of T st t9 in C & t is_a_proper_prefix_of t9;

        

         A4: for t9 be Element of T st t9 in C holds t9 is_a_prefix_of t

        proof

          let t9 be Element of T such that

           A5: t9 in C;

          now

            assume

             A6: not t9 is_a_prefix_of t;

            (t,t9) are_c=-comparable by A1, A5, TREES_2:def 3;

            then t is_a_prefix_of t9 by A6;

            then t is_a_proper_prefix_of t9 by A6;

            hence contradiction by A3, A5;

          end;

          hence thesis;

        end;

        C c= (( ProperPrefixes t) \/ {t})

        proof

          let x be object;

          assume

           A7: x in C;

          then

          reconsider t9 = x as Element of T;

          

           A8: t9 is_a_prefix_of t by A4, A7;

          t9 in (( ProperPrefixes t) \/ {t})

          proof

            per cases by A8;

              suppose t9 is_a_proper_prefix_of t;

              then t9 in ( ProperPrefixes t) by TREES_1: 12;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose t9 = t;

              then t9 in {t} by TARSKI:def 1;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          hence thesis;

        end;

        hence contradiction by A2;

      end;

      hence thesis;

    end;

    theorem :: TREES_9:51

    

     Th51: for T be Tree, B be Branch of T, t be Element of T st t in B & not B is finite holds ex t9 be Element of T st t9 in B & t9 in ( succ t)

    proof

      let T be Tree, B be Branch of T, t be Element of T;

      assume t in B & not B is finite;

      then

      consider t99 be Element of T such that

       A1: t99 in B and

       A2: t is_a_proper_prefix_of t99 by Th50;

      t is_a_prefix_of t99 by A2;

      then

      consider r be FinSequence such that

       A3: t99 = (t ^ r) by TREES_1: 1;

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

      (r | ( Seg 1)) is FinSequence of NAT by FINSEQ_1: 18;

      then

      consider r1 be FinSequence of NAT such that

       A4: r1 = (r | ( Seg 1));

      1 <= ( len r)

      proof

        ( len t) < ( len t99) by A2, TREES_1: 6;

        then

        consider m be Nat such that

         A5: (( len t) + m) = ( len t99) by NAT_1: 10;

        m <> 0 by A2, A5, TREES_1: 6;

        then 0 < m;

        then

         A6: ( 0 + 1) <= m by NAT_1: 13;

        ( len t99) = (( len t) + ( len r)) by A3, FINSEQ_1: 22;

        hence thesis by A5, A6;

      end;

      then

      consider n be Element of NAT such that

       A7: r1 = <*n*> by A4, Th34;

      

       A8: r1 is_a_prefix_of r by A4, TREES_1:def 1;

      then

       A9: (t ^ r1) is_a_prefix_of t99 by A3, FINSEQ_6: 13;

      (t ^ <*n*>) in T by A3, A7, A8, FINSEQ_6: 13, TREES_1: 20;

      then

      consider t9 be Element of T such that

       A10: t9 = (t ^ <*n*>);

      t9 in ( succ t) by A10;

      hence thesis by A1, A7, A9, A10, TREES_2: 25;

    end;

    theorem :: TREES_9:52

    

     Th52: for f be sequence of NAT st (for n holds (f . (n + 1)) qua Nat <= (f . n) qua Nat) holds ex m st for n st m <= n holds (f . n) = (f . m)

    proof

      let f be sequence of NAT such that

       A1: for n holds (f . (n + 1)) qua Nat <= (f . n) qua Nat;

      

       A2: for m, k st m <= k holds (f . k) qua Nat <= (f . m) qua Nat

      proof

        defpred P[ Nat] means for m st m <= $1 holds (f . $1) qua Element of NAT <= (f . m) qua Nat;

        

         A3: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A4: P[k];

          now

            let m;

            assume

             A5: m <= (k + 1);

            per cases by A5, NAT_1: 8;

              suppose

               A6: m <= k;

              reconsider fk = (f . k), fm = (f . m), fk1 = (f . (k + 1)) as Nat;

              

               A7: fk1 <= fk by A1;

              fk <= fm by A4, A6;

              hence (f . (k + 1)) qua Nat <= (f . m) qua Nat by A7, XXREAL_0: 2;

            end;

              suppose m = (k + 1);

              hence (f . (k + 1)) qua Nat <= (f . m) qua Nat;

            end;

          end;

          hence thesis;

        end;

        

         A8: P[ 0 ] by XXREAL_0: 1;

        

         A9: for k holds P[k] from NAT_1:sch 2( A8, A3);

        let m, k;

        assume m <= k;

        hence thesis by A9;

      end;

      defpred P[ set] means $1 in ( rng f);

      

       A10: ex k be Nat st P[k]

      proof

        consider y such that

         A11: y = (f . 0 );

        reconsider k = y as Nat by A11;

        take k;

        ( dom f) = NAT by FUNCT_2:def 1;

        hence thesis by A11, FUNCT_1:def 3;

      end;

      ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A10);

      then

      consider l be Nat such that

       A12: l in ( rng f) and

       A13: for n be Nat st n in ( rng f) holds l <= n;

      consider x be object such that

       A14: x in ( dom f) and

       A15: l = (f . x) by A12, FUNCT_1:def 3;

      reconsider m = x as Nat by A14;

      

       A16: ( dom f) = NAT by FUNCT_2:def 1;

      for k st m <= k holds (f . k) = (f . m)

      proof

        let k such that

         A17: m <= k;

        now

          reconsider fk = (f . k), fm = (f . m) as Nat;

          assume

           A18: (f . k) <> (f . m);

          fk <= fm by A2, A17;

          then

           A19: fk < fm by A18, XXREAL_0: 1;

          k in NAT by ORDINAL1:def 12;

          then (f . k) in ( rng f) by A16, FUNCT_1:def 3;

          hence contradiction by A13, A15, A19;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    scheme :: TREES_9:sch3

    FinDecTree { D() -> non empty set , T() -> finite-branching DecoratedTree of D() , F( Element of D()) -> Nat } :

T() is finite

      provided

       A1: for t,t9 be Element of ( dom T()), d be Element of D() st t9 in ( succ t) & d = (T() . t9) holds F(d) < F(.);

      now

        assume not T() is finite;

        then not ( dom T()) is finite by FINSET_1: 10;

        then

        consider B be Branch of ( dom T()) such that

         A2: not B is finite by Th49;

        defpred P[ object, object] means ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & t in B & t9 in B & $1 = (T() . t) & $2 = (T() . t9);

        defpred Q[ object] means ex t be Element of ( dom T()) st t in B & $1 = (T() . t);

        

         A3: for x be object st x in D() & Q[x] holds ex y be object st y in D() & P[x, y] & Q[y]

        proof

          let x be object;

          assume that x in D() and

           A4: Q[x];

          consider t be Element of ( dom T()) such that

           A5: t in B and

           A6: x = (T() . t) by A4;

          consider t9 be Element of ( dom T()) such that

           A7: t9 in B & t9 in ( succ t) by A2, A5, Th51;

          ex y st y = (T() . t9);

          hence thesis by A5, A6, A7;

        end;

         {} in B by TREES_2: 26;

        then Q[(T() . {} )];

        then

         A8: (T() . {} ) in D() & Q[(T() . {} )];

        ex g be Function st ( dom g) = NAT & ( rng g) c= D() & (g . 0 ) = (T() . {} ) & for k holds P[(g . k), (g . (k + 1))] & Q[(g . k)] from TREES_2:sch 5( A8, A3);

        then

        consider g be Function such that ( dom g) = NAT and ( rng g) c= D() and (g . 0 ) = (T() . {} ) and

         A9: for k holds (ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & t in B & t9 in B & (g . k) = (T() . t) & (g . (k + 1)) = (T() . t9)) & ex t be Element of ( dom T()) st t in B & (g . k) = (T() . t);

        defpred P[ object, object] means ex d be Element of D() st d = (g . $1) & $2 = F(d);

        

         A10: for x be object st x in NAT holds ex y be object st y in NAT & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider k = x as Element of NAT ;

          consider t be Element of ( dom T()) such that t in B and

           A11: (g . k) = (T() . t) by A9;

          reconsider y = F(.) as set;

          take y;

          y in NAT by ORDINAL1:def 12;

          hence thesis by A11;

        end;

        ex f be sequence of NAT st for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A10);

        then

        consider f be sequence of NAT such that

         A12: for x be object st x in NAT holds ex d be Element of D() st d = (g . x) & (f . x) = F(d);

        

         A13: for k holds ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & t in B & t9 in B & (f . k) = F(.) & (f . (k + 1)) = F(.)

        proof

          let k;

          

           A14: ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & t in B & t9 in B & (g . k) = (T() . t) & (g . (k + 1)) = (T() . t9) by A9;

          k in NAT by ORDINAL1:def 12;

          then (ex d be Element of D() st d = (g . k) & (f . k) = F(d)) & ex d1 be Element of D() st d1 = (g . (k + 1)) & (f . (k + 1)) = F(d1) by A12;

          hence thesis by A14;

        end;

        

         A15: for n holds ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & (f . n) = F(.) & (f . (n + 1)) = F(.) & (f . (n + 1)) qua Nat < (f . n) qua Nat

        proof

          let n;

          ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & t in B & t9 in B & (f . n) = F(.) & (f . (n + 1)) = F(.) by A13;

          hence thesis by A1;

        end;

        for n holds (f . (n + 1)) qua Nat <= (f . n) qua Nat

        proof

          let n;

          ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & (f . n) = F(.) & (f . (n + 1)) = F(.) & (f . (n + 1)) qua Nat < (f . n) qua Nat by A15;

          hence thesis;

        end;

        then

        consider m such that

         A16: for n st m <= n holds (f . n) = (f . m) by Th52;

        

         A17: (m + 0 ) <= (m + 1) by XREAL_1: 6;

        ex t,t9 be Element of ( dom T()) st t9 in ( succ t) & (f . m) = F(.) & (f . (m + 1)) = F(.) & (f . (m + 1)) qua Nat < (f . m) qua Nat by A15;

        hence contradiction by A16, A17;

      end;

      hence thesis;

    end;