trees_1.miz



    begin

    reserve X,x,y,z for set,

k,n,m for Nat,

f for Function,

p,q,r for FinSequence of NAT ;

    notation

      let p,q be FinSequence;

      synonym p is_a_prefix_of q for p c= q;

    end

    definition

      let p,q be FinSequence;

      :: original: is_a_prefix_of

      redefine

      :: TREES_1:def1

      pred p is_a_prefix_of q means ex n st p = (q | ( Seg n));

      compatibility

      proof

        thus p c= q implies ex n st p = (q | ( Seg n))

        proof

          assume

           A1: p c= q;

          consider n be Nat such that

           A2: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

          reconsider n as Nat;

          take n;

          thus thesis by A1, A2, GRFUNC_1: 23;

        end;

        thus thesis by RELAT_1: 59;

      end;

    end

    theorem :: TREES_1:1

    

     Th1: for p,q be FinSequence holds p is_a_prefix_of q iff ex r be FinSequence st q = (p ^ r)

    proof

      let p,q be FinSequence;

      thus p is_a_prefix_of q implies ex r be FinSequence st q = (p ^ r) by FINSEQ_1: 80;

      given r be FinSequence such that

       A1: q = (p ^ r);

      ( dom p) = ( Seg ( len p)) & p = (q | ( dom p)) by A1, FINSEQ_1: 21, FINSEQ_1:def 3;

      hence thesis;

    end;

    ::$Canceled

    theorem :: TREES_1:3

    

     Th2: <*x*> is_a_prefix_of <*y*> implies x = y

    proof

      assume

       A1: <*x*> is_a_prefix_of <*y*>;

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

      then

       A2: <*x*> = <*y*> by A1, CARD_2: 102;

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

      hence thesis by A2, FINSEQ_1: 40;

    end;

    notation

      let p,q be FinSequence;

      synonym p is_a_proper_prefix_of q for p c< q;

    end

    theorem :: TREES_1:4

    

     Th3: for p,q be finite set st (p,q) are_c=-comparable & ( card p) = ( card q) holds p = q by CARD_2: 102;

    reserve p1,p2,p3 for FinSequence;

    theorem :: TREES_1:5

    

     Th4: ( <*x*>, <*y*>) are_c=-comparable implies x = y

    proof

      assume

       A1: ( <*x*>, <*y*>) are_c=-comparable ;

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

      then

       A2: <*x*> = <*y*> by A1, Th3;

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

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: TREES_1:6

    

     Th5: for p,q be finite set st p c< q holds ( card p) < ( card q)

    proof

      let p,q be finite set;

      assume that

       A1: p c= q and

       A2: p <> q;

      

       A3: ( card p) <= ( card q) by A1, NAT_1: 43;

      (p,q) are_c=-comparable by A1;

      hence thesis by A3, A2, Th3, XXREAL_0: 1;

    end;

    theorem :: TREES_1:7

    

     Th6: (p1 ^ <*x*>) is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2

    proof

      assume (p1 ^ <*x*>) is_a_prefix_of p2;

      then

      consider p3 such that

       A1: p2 = ((p1 ^ <*x*>) ^ p3) by Th1;

      p2 = (p1 ^ ( <*x*> ^ p3)) by A1, FINSEQ_1: 32;

      hence p1 is_a_prefix_of p2 by Th1;

      assume p1 = p2;

      

      then ( len p1) = (( len (p1 ^ <*x*>)) + ( len p3)) by A1, FINSEQ_1: 22

      .= ((( len p1) + ( len <*x*>)) + ( len p3)) by FINSEQ_1: 22

      .= ((( len p1) + 1) + ( len p3)) by FINSEQ_1: 39;

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

      hence contradiction by NAT_1: 13;

    end;

    theorem :: TREES_1:8

    

     Th7: p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of (p2 ^ <*x*>)

    proof

      assume p1 is_a_prefix_of p2;

      then

      consider p3 such that

       A1: p2 = (p1 ^ p3) by Th1;

      (p2 ^ <*x*>) = (p1 ^ (p3 ^ <*x*>)) by A1, FINSEQ_1: 32;

      hence p1 is_a_prefix_of (p2 ^ <*x*>) by Th1;

      assume p1 = (p2 ^ <*x*>);

      

      then ( len p2) = (( len (p2 ^ <*x*>)) + ( len p3)) by A1, FINSEQ_1: 22

      .= ((( len p2) + ( len <*x*>)) + ( len p3)) by FINSEQ_1: 22

      .= ((( len p2) + 1) + ( len p3)) by FINSEQ_1: 39;

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

      hence contradiction by NAT_1: 13;

    end;

    theorem :: TREES_1:9

    

     Th8: p1 is_a_proper_prefix_of (p2 ^ <*x*>) implies p1 is_a_prefix_of p2

    proof

      assume that

       A1: p1 is_a_prefix_of (p2 ^ <*x*>) and

       A2: p1 <> (p2 ^ <*x*>);

      

       A3: ex p3 st (p2 ^ <*x*>) = (p1 ^ p3) by A1, Th1;

      

       A4: ( len p1) <= ( len (p2 ^ <*x*>)) by A1, NAT_1: 43;

      ( len (p2 ^ <*x*>)) = (( len p2) + ( len <*x*>)) & ( len <*x*>) = 1 by FINSEQ_1: 22, FINSEQ_1: 39;

      then ( len p1) < (( len p2) + 1) by A1, A2, A4, CARD_2: 102, XXREAL_0: 1;

      then ( len p1) <= ( len p2) by NAT_1: 13;

      then ex p3 st (p1 ^ p3) = p2 by A3, FINSEQ_1: 47;

      hence thesis by Th1;

    end;

    theorem :: TREES_1:10

     {} is_a_proper_prefix_of p2 or {} <> p2 implies p1 is_a_proper_prefix_of (p1 ^ p2)

    proof

      assume

       A1: {} is_a_proper_prefix_of p2 or {} <> p2;

      thus p1 is_a_prefix_of (p1 ^ p2) by Th1;

      assume p1 = (p1 ^ p2);

      then ( len p1) = (( len p1) + ( len p2)) by FINSEQ_1: 22;

      then p2 = {} ;

      hence contradiction by A1;

    end;

    definition

      let p be FinSequence;

      :: TREES_1:def2

      func ProperPrefixes p -> set means

      : Def2: for x be object holds x in it iff ex q be FinSequence st x = q & q is_a_proper_prefix_of p;

      existence

      proof

        set E = ( rng p);

        defpred X[ object] means ex q be FinSequence st $1 = q & q is_a_proper_prefix_of p;

        consider X such that

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

        take X;

        let x be object;

        thus x in X implies ex q be FinSequence st x = q & q is_a_proper_prefix_of p by A1;

        given q be FinSequence such that

         A2: x = q and

         A3: q is_a_proper_prefix_of p;

        q is_a_prefix_of p by A3;

        then ex n st q = (p | ( Seg n));

        then ( rng q) c= E by RELAT_1: 70;

        then

        reconsider q as FinSequence of E by FINSEQ_1:def 4;

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

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let S1,S2 be set such that

         A4: for x be object holds x in S1 iff ex q be FinSequence st x = q & q is_a_proper_prefix_of p and

         A5: for x be object holds x in S2 iff ex q be FinSequence st x = q & q is_a_proper_prefix_of p;

        defpred X[ object] means ex q be FinSequence st $1 = q & q is_a_proper_prefix_of p;

        

         A6: for x be object holds x in S1 iff X[x] by A4;

        

         A7: for x be object holds x in S2 iff X[x] by A5;

        thus thesis from XBOOLE_0:sch 2( A6, A7);

      end;

    end

    theorem :: TREES_1:11

    

     Th10: for p be FinSequence st x in ( ProperPrefixes p) holds x is FinSequence

    proof

      let p be FinSequence;

      assume x in ( ProperPrefixes p);

      then ex q be FinSequence st x = q & q is_a_proper_prefix_of p by Def2;

      hence thesis;

    end;

    theorem :: TREES_1:12

    

     Th11: for p,q be FinSequence holds p in ( ProperPrefixes q) iff p is_a_proper_prefix_of q

    proof

      let p,q be FinSequence;

      thus p in ( ProperPrefixes q) implies p is_a_proper_prefix_of q

      proof

        assume p in ( ProperPrefixes q);

        then ex r be FinSequence st p = r & r is_a_proper_prefix_of q by Def2;

        hence thesis;

      end;

      thus thesis by Def2;

    end;

    theorem :: TREES_1:13

    

     Th12: for p,q be FinSequence st p in ( ProperPrefixes q) holds ( len p) < ( len q) by Th11, Th5;

    theorem :: TREES_1:14

    for p,q,r be FinSequence st (q ^ r) in ( ProperPrefixes p) holds q in ( ProperPrefixes p)

    proof

      let p,q,r be FinSequence;

      assume

       A1: (q ^ r) in ( ProperPrefixes p);

      

       A2: q is_a_prefix_of (q ^ r) by Th1;

      (q ^ r) is_a_proper_prefix_of p by A1, Th11;

      then q is_a_proper_prefix_of p by A2, XBOOLE_1: 59;

      hence thesis by Th11;

    end;

    theorem :: TREES_1:15

    

     Th14: ( ProperPrefixes {} ) = {}

    proof

      set x = the Element of ( ProperPrefixes {} );

      assume

       A1: not thesis;

      then

      reconsider x as FinSequence by Th10;

      x is_a_proper_prefix_of {} by A1, Th11;

      hence contradiction by XBOOLE_1: 62;

    end;

    set D = { {} };

    theorem :: TREES_1:16

    

     Th15: ( ProperPrefixes <*x*>) = { {} }

    proof

      thus ( ProperPrefixes <*x*>) c= D

      proof

        let y be object;

        assume y in ( ProperPrefixes <*x*>);

        then

        consider p be FinSequence such that

         A1: y = p and

         A2: p is_a_proper_prefix_of <*x*> by Def2;

        

         A3: ( len p) < ( len <*x*>) by A2, Th5;

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

        then p = {} by A3, NAT_1: 13;

        hence thesis by A1, TARSKI:def 1;

      end;

      let y be object;

      assume y in D;

      then

       A4: y = {} by TARSKI:def 1;

       {} is_a_prefix_of <*x*>;

      then {} is_a_proper_prefix_of <*x*>;

      hence thesis by A4, Def2;

    end;

    theorem :: TREES_1:17

    for p,q be FinSequence st p is_a_prefix_of q holds ( ProperPrefixes p) c= ( ProperPrefixes q)

    proof

      let p,q be FinSequence such that

       A1: p is_a_prefix_of q;

      let x be object;

      assume

       A2: x in ( ProperPrefixes p);

      then

      reconsider r = x as FinSequence by Th10;

      r is_a_proper_prefix_of p by A2, Th11;

      then r is_a_proper_prefix_of q by A1, XBOOLE_1: 58;

      hence thesis by Th11;

    end;

    theorem :: TREES_1:18

    

     Th17: for p,q,r be FinSequence st q in ( ProperPrefixes p) & r in ( ProperPrefixes p) holds (q,r) are_c=-comparable

    proof

      let p,q,r be FinSequence;

      assume q in ( ProperPrefixes p);

      then

       A1: ex q1 be FinSequence st q = q1 & q1 is_a_proper_prefix_of p by Def2;

      assume r in ( ProperPrefixes p);

      then

       A2: ex r1 be FinSequence st r = r1 & r1 is_a_proper_prefix_of p by Def2;

      q is_a_prefix_of p by A1;

      then

      consider n such that

       A3: q = (p | ( Seg n));

      r is_a_prefix_of p by A2;

      then

      consider k such that

       A4: r = (p | ( Seg k));

      

       A5: n <= k implies thesis

      proof

        assume n <= k;

        then ( Seg n) c= ( Seg k) by FINSEQ_1: 5;

        then q = (r | ( Seg n)) by A3, A4, FUNCT_1: 51;

        then q is_a_prefix_of r;

        hence thesis;

      end;

      k <= n implies thesis

      proof

        assume k <= n;

        then ( Seg k) c= ( Seg n) by FINSEQ_1: 5;

        then r = (q | ( Seg k)) by A3, A4, FUNCT_1: 51;

        then r is_a_prefix_of q;

        hence thesis;

      end;

      hence thesis by A5;

    end;

    definition

      let X;

      :: TREES_1:def3

      attr X is Tree-like means

      : Def3: X c= ( NAT * ) & (for p st p in X holds ( ProperPrefixes p) c= X) & for p, k, n st (p ^ <*k*>) in X & n <= k holds (p ^ <*n*>) in X;

    end

    registration

      cluster { {} } -> Tree-like;

      coherence

      proof

        thus D c= ( NAT * )

        proof

          let x be object;

          assume x in D;

          then x = {} by TARSKI:def 1;

          hence thesis by FINSEQ_1: 49;

        end;

        thus for p st p in D holds ( ProperPrefixes p) c= D by TARSKI:def 1, Th14;

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      cluster non empty Tree-like for set;

      existence

      proof

        take D = {( <*> NAT )};

        thus thesis;

      end;

    end

    definition

      mode Tree is Tree-like non empty set;

    end

    reserve T,T1 for Tree;

    theorem :: TREES_1:19

    

     Th18: x in T implies x is FinSequence of NAT

    proof

      T c= ( NAT * ) by Def3;

      hence thesis by FINSEQ_1:def 11;

    end;

    definition

      let T;

      :: original: Element

      redefine

      mode Element of T -> FinSequence of NAT ;

      coherence by Th18;

    end

    theorem :: TREES_1:20

    

     Th19: for p,q be FinSequence st p in T & q is_a_prefix_of p holds q in T

    proof

      let p,q be FinSequence;

      assume that

       A1: p in T and

       A2: q is_a_prefix_of p;

      reconsider r = p as Element of T by A1;

      

       A3: ( ProperPrefixes r) c= T by Def3;

      q is_a_proper_prefix_of p or q = p by A2;

      then q in ( ProperPrefixes p) or p = q by Th11;

      hence thesis by A3;

    end;

    theorem :: TREES_1:21

    

     Th20: for r be FinSequence st (q ^ r) in T holds q in T

    proof

      let r be FinSequence;

      assume

       A1: (q ^ r) in T;

      then

      reconsider p = (q ^ r) as FinSequence of NAT by Th18;

      reconsider s = (p | ( Seg ( len q))) as FinSequence of NAT by FINSEQ_1: 18;

      ( len p) = (( len q) + ( len r)) by FINSEQ_1: 22;

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

      then

       A2: ( len s) = ( len q) by FINSEQ_1: 17;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len q);

        then

         A3: n in ( Seg ( len q)) by FINSEQ_1: 1;

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

        then (p . n) = (q . n) by A3, FINSEQ_1:def 7;

        hence (q . n) = (s . n) by A3, FUNCT_1: 49;

      end;

      then q = s by A2, FINSEQ_1: 14;

      then

       A4: q is_a_prefix_of p;

      now

        assume q <> p;

        then q is_a_proper_prefix_of p by A4;

        then

         A5: q in ( ProperPrefixes p) by Def2;

        ( ProperPrefixes p) c= T by A1, Def3;

        hence thesis by A5;

      end;

      hence thesis by A1;

    end;

    theorem :: TREES_1:22

    

     Th21: {} in T & ( <*> NAT ) in T

    proof

      reconsider x = the Element of T as FinSequence of NAT ;

      x in T;

      then

       A1: ( {} ^ x) in T by FINSEQ_1: 34;

       {} = ( <*> NAT );

      hence thesis by A1, Th20;

    end;

    theorem :: TREES_1:23

     { {} } is Tree;

    registration

      let T, T1;

      cluster (T \/ T1) -> Tree-like;

      coherence

      proof

        set D = (T \/ T1);

        T c= ( NAT * ) & T1 c= ( NAT * ) by Def3;

        hence D c= ( NAT * ) by XBOOLE_1: 8;

        thus for p st p in D holds ( ProperPrefixes p) c= D

        proof

          let p;

          assume p in D;

          then p in T or p in T1 by XBOOLE_0:def 3;

          then

           A1: ( ProperPrefixes p) c= T or ( ProperPrefixes p) c= T1 by Def3;

          T c= D & T1 c= D by XBOOLE_1: 7;

          hence thesis by A1;

        end;

        let p, k, n;

        assume that

         A2: (p ^ <*k*>) in D and

         A3: n <= k;

        (p ^ <*k*>) in T or (p ^ <*k*>) in T1 by A2, XBOOLE_0:def 3;

        then (p ^ <*n*>) in T or (p ^ <*n*>) in T1 by A3, Def3;

        hence thesis by XBOOLE_0:def 3;

      end;

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

      coherence

      proof

        set D = (T /\ T1);

        thus D is Tree-like

        proof

          T c= ( NAT * ) & (T /\ T1) c= T by Def3, XBOOLE_1: 17;

          hence D c= ( NAT * );

          thus for p st p in D holds ( ProperPrefixes p) c= D

          proof

            let p;

            assume

             A4: p in D;

            then

             A5: p in T by XBOOLE_0:def 4;

            

             A6: p in T1 by A4, XBOOLE_0:def 4;

            

             A7: ( ProperPrefixes p) c= T by A5, Def3;

            ( ProperPrefixes p) c= T1 by A6, Def3;

            hence thesis by A7, XBOOLE_1: 19;

          end;

          let p, k, n;

          assume that

           A8: (p ^ <*k*>) in D and

           A9: n <= k;

          

           A10: (p ^ <*k*>) in T by A8, XBOOLE_0:def 4;

          

           A11: (p ^ <*k*>) in T1 by A8, XBOOLE_0:def 4;

          

           A12: (p ^ <*n*>) in T by A9, A10, Def3;

          (p ^ <*n*>) in T1 by A9, A11, Def3;

          hence thesis by A12, XBOOLE_0:def 4;

        end;

         {} in T & {} in T1 by Th21;

        hence thesis by XBOOLE_0:def 4;

      end;

    end

    theorem :: TREES_1:24

    (T \/ T1) is Tree;

    theorem :: TREES_1:25

    (T /\ T1) is Tree;

    registration

      cluster finite for Tree;

      existence

      proof

        take D;

        thus thesis;

      end;

    end

    reserve fT,fT1 for finite Tree;

    theorem :: TREES_1:26

    (fT \/ fT1) is finite Tree;

    theorem :: TREES_1:27

    (fT /\ T) is finite Tree;

    definition

      let n;

      :: TREES_1:def4

      func elementary_tree n -> Tree equals ({ <*k*> : k < n } \/ { {} });

      correctness

      proof

        set IT = ({ <*k*> : k < n } \/ D);

        IT is Tree-like

        proof

          thus IT c= ( NAT * )

          proof

            let x be object;

            assume x in IT;

            then

             A1: x in { <*k*> : k < n } or x in D by XBOOLE_0:def 3;

            

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

            now

              assume x in { <*k*> : k < n };

              then

              consider k such that

               A3: x = <*k*> & k < n;

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

              x = <*k*> by A3;

              hence thesis by FINSEQ_1:def 11;

            end;

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

          end;

          thus for p st p in IT holds ( ProperPrefixes p) c= IT

          proof

            let p;

            assume p in IT;

            then

             A4: p in { <*k*> : k < n } or p in D by XBOOLE_0:def 3;

            now

              assume p in { <*k*> : k < n };

              then ex k st p = <*k*> & k < n;

              then ( ProperPrefixes p) = D by Th15;

              hence thesis by XBOOLE_1: 7;

            end;

            hence thesis by A4, Th14, TARSKI:def 1;

          end;

          let p, k, m;

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

          then (p ^ <*k*>) in { <*j*> where j be Nat : j < n } or (p ^ <*k*>) in D by XBOOLE_0:def 3;

          then

          consider l be Nat such that

           A5: (p ^ <*k*>) = <*l*> and

           A6: l < n by TARSKI:def 1;

          (( len p) + ( len <*k*>)) = ( len <*l*>) by A5, FINSEQ_1: 22

          .= 1 by FINSEQ_1: 39;

          then (( len p) + 1) = ( 0 + 1) by FINSEQ_1: 39;

          then

           A7: p = {} ;

          then

           A8: <*k*> = <*l*> by A5, FINSEQ_1: 34;

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

          then

           A9: k = l by A8, FINSEQ_1:def 8;

          assume

           A10: m <= k;

          

           A11: (p ^ <*m*>) = <*m*> by A7, FINSEQ_1: 34;

          m < n by A6, A9, A10, XXREAL_0: 2;

          then (p ^ <*m*>) in { <*j*> where j be Nat : j < n } by A11;

          hence thesis by XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster ( elementary_tree n) -> finite;

      coherence

      proof

        set IT = ( elementary_tree n);

        (IT,( Seg (n + 1))) are_equipotent

        proof

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

          

           A1: x in IT & F[x, y] & F[x, z] implies y = z

          proof

            assume that x in IT and

             A2: (x = {} & y = 1 or ex n st x = <*n*> & y = (n + 2)) & (x = {} & z = 1 or ex n st x = <*n*> & z = (n + 2));

            now

              given n1 be Nat such that

               A3: x = <*n1*> & y = (n1 + 2);

              given n2 be Nat such that

               A4: x = <*n2*> & z = (n2 + 2);

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

              hence thesis by A3, A4, FINSEQ_1:def 8;

            end;

            hence thesis by A2;

          end;

          

           A5: for x be object st x in IT holds ex y be object st F[x, y]

          proof

            let x be object;

            assume

             A6: x in IT;

             A7:

            now

              assume x in { <*k*> : k < n };

              then

              consider k such that

               A8: x = <*k*> and k < n;

              reconsider y = (k + 2) as set;

              take y;

              thus F[x, y] by A8;

            end;

            now

              assume

               A9: x in D;

              reconsider y = 1 as set;

              take y;

              thus F[x, y] by A9, TARSKI:def 1;

            end;

            hence thesis by A6, A7, XBOOLE_0:def 3;

          end;

          consider f such that

           A10: ( dom f) = IT & for x be object st x in IT holds F[x, (f . x)] from CLASSES1:sch 1( A5);

          take f;

          thus f is one-to-one

          proof

            let x,y be object;

            assume that

             A11: x in ( dom f) and

             A12: y in ( dom f) and

             A13: (f . x) = (f . y);

            

             A14: x = {} & (f . x) = 1 or ex n st x = <*n*> & (f . x) = (n + 2) by A10, A11;

            

             A15: y = {} & (f . y) = 1 or ex n st y = <*n*> & (f . y) = (n + 2) by A10, A12;

             A16:

            now

              assume that x = {} and

               A17: (f . x) = 1;

              given n such that y = <*n*> and

               A18: (f . y) = (n + 2);

              ( 0 + 1) = ((n + 1) + 1) by A13, A17, A18;

              hence contradiction;

            end;

            now

              assume that y = {} and

               A19: (f . y) = 1;

              given n such that x = <*n*> and

               A20: (f . x) = (n + 2);

              ( 0 + 1) = ((n + 1) + 1) by A13, A19, A20;

              hence contradiction;

            end;

            hence thesis by A13, A14, A15, A16;

          end;

          thus ( dom f) = IT by A10;

          thus ( rng f) c= ( Seg (n + 1))

          proof

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A21: y in ( dom f) and

             A22: x = (f . y) by FUNCT_1:def 3;

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

            then

             A23: 1 in ( Seg (n + 1)) by FINSEQ_1: 1;

            now

              given k such that

               A24: y = <*k*> and

               A25: x = (k + 2);

              y in { <*j*> where j be Nat : j < n } or y in D by A10, A21, XBOOLE_0:def 3;

              then

              consider l be Nat such that

               A26: y = <*l*> & l < n by A24, TARSKI:def 1;

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

              then (k + 1) <= n by A24, A26, NAT_1: 13;

              then (1 + 0 ) <= ((k + 1) + 1) & ((k + 1) + 1) <= (n + 1) by XREAL_1: 7;

              hence thesis by A25, FINSEQ_1: 1;

            end;

            hence thesis by A10, A21, A22, A23;

          end;

          let x be object;

          assume

           A27: x in ( Seg (n + 1));

          then

          reconsider k = x as Nat;

          

           A28: 1 <= k by A27, FINSEQ_1: 1;

          

           A29: k <= (n + 1) by A27, FINSEQ_1: 1;

           {} in D by TARSKI:def 1;

          then

           A30: {} in IT by XBOOLE_0:def 3;

          then F[ {} , (f . {} )] by A10;

          then

           A31: 1 in ( rng f) by A10, A30, FUNCT_1:def 3;

          now

            assume 1 < k;

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

            then

            consider m be Nat such that

             A32: k = (2 + m) by NAT_1: 10;

            reconsider m as Nat;

            ((1 + 1) + m) = (1 + (1 + m));

            then (1 + m) <= n by A29, A32, XREAL_1: 6;

            then m < n by NAT_1: 13;

            then <*m*> in { <*j*> where j be Nat : j < n };

            then

             A33: <*m*> in IT by XBOOLE_0:def 3;

            then F[ <*m*>, (f . <*m*>)] by A10;

            then k = (f . <*m*>) by A1, A32, A33;

            hence k in ( rng f) by A10, A33, FUNCT_1:def 3;

          end;

          hence thesis by A28, A31, XXREAL_0: 1;

        end;

        hence thesis by CARD_1: 38;

      end;

    end

    theorem :: TREES_1:28

    

     Th27: k < n implies <*k*> in ( elementary_tree n)

    proof

      assume k < n;

      then <*k*> in { <*j*> where j be Nat : j < n };

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TREES_1:29

    

     Th28: ( elementary_tree 0 ) = { {} }

    proof

      now

        set x = the Element of { <*j*> where j be Nat : j < 0 };

        assume { <*j*> where j be Nat : j < 0 } <> {} ;

        then x in { <*j*> where j be Nat : j < 0 };

        then ex k st x = <*k*> & k < 0 ;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: TREES_1:30

    p in ( elementary_tree n) implies p = {} or ex k st k < n & p = <*k*>

    proof

      assume p in ( elementary_tree n);

      then

       A1: p in D or p in { <*k*> : k < n } by XBOOLE_0:def 3;

      p in { <*k*> : k < n } implies ex k st p = <*k*> & k < n;

      hence thesis by A1, TARSKI:def 1;

    end;

    definition

      let T;

      :: TREES_1:def5

      func Leaves T -> Subset of T means

      : Def5: p in it iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;

      existence

      proof

        defpred X[ object] means for p st $1 = p holds for q st q in T holds not p is_a_proper_prefix_of q;

        consider X such that

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

        X c= T by A1;

        then

        reconsider X as Subset of T;

        take X;

        let p;

        thus p in X implies p in T & not ex q st q in T & p is_a_proper_prefix_of q by A1;

        assume that

         A2: p in T and

         A3: not ex q st q in T & p is_a_proper_prefix_of q;

        for r be FinSequence of NAT st p = r holds for q st q in T holds not r is_a_proper_prefix_of q by A3;

        hence p in X by A1, A2;

      end;

      uniqueness

      proof

        let L1,L2 be Subset of T such that

         A4: p in L1 iff p in T & not ex q st q in T & p is_a_proper_prefix_of q and

         A5: p in L2 iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;

        

         A6: T c= ( NAT * ) by Def3;

        then

         A7: L1 c= ( NAT * );

        

         A8: L2 c= ( NAT * ) by A6;

        now

          let x be object;

          thus x in L1 implies x in L2

          proof

            assume

             A9: x in L1;

            then

            reconsider p = x as FinSequence of NAT by A7, FINSEQ_1:def 11;

             not ex q st q in T & p is_a_proper_prefix_of q by A4, A9;

            hence thesis by A5, A9;

          end;

          assume

           A10: x in L2;

          then

          reconsider p = x as FinSequence of NAT by A8, FINSEQ_1:def 11;

           not ex q st q in T & p is_a_proper_prefix_of q by A5, A10;

          hence x in L1 by A4, A10;

        end;

        hence thesis by TARSKI: 2;

      end;

      let p;

      :: TREES_1:def6

      func T | p -> Tree means

      : Def6: q in it iff (p ^ q) in T;

      existence

      proof

        defpred X[ object] means for q st $1 = q holds (p ^ q) in T;

        consider X such that

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

        ( <*> NAT ) in ( NAT * ) & for q st ( <*> NAT ) = q holds (p ^ q) in T by A11, FINSEQ_1: 34, FINSEQ_1:def 11;

        then

        reconsider X as non empty set by A12;

        

         A13: X c= ( NAT * ) by A12;

         A14:

        now

          let q such that

           A15: q in X;

          thus ( ProperPrefixes q) c= X

          proof

            let x be object;

            assume x in ( ProperPrefixes q);

            then

            consider r be FinSequence such that

             A16: x = r and

             A17: r is_a_proper_prefix_of q by Def2;

            r is_a_prefix_of q by A17;

            then

             A18: ex n st r = (q | ( Seg n));

            then

            reconsider r as FinSequence of NAT by FINSEQ_1: 18;

            consider s be FinSequence such that

             A19: q = (r ^ s) by A18, FINSEQ_1: 80;

            

             A20: (p ^ q) in T by A12, A15;

            (p ^ q) = ((p ^ r) ^ s) by A19, FINSEQ_1: 32;

            then r in ( NAT * ) & for q st r = q holds (p ^ q) in T by A20, Th20, FINSEQ_1:def 11;

            hence thesis by A12, A16;

          end;

        end;

        now

          let q, k, n;

          assume that

           A21: (q ^ <*k*>) in X and

           A22: n <= k;

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

          (p ^ (q ^ <*kk*>)) in T by A12, A21;

          then ((p ^ q) ^ <*k*>) in T by FINSEQ_1: 32;

          then ((p ^ q) ^ <*n*>) in T by A22, Def3;

          then (q ^ <*nn*>) in ( NAT * ) & for r st r = (q ^ <*nn*>) holds (p ^ r) in T by FINSEQ_1: 32, FINSEQ_1:def 11;

          hence (q ^ <*n*>) in X by A12;

        end;

        then

        reconsider X as Tree by A13, A14, Def3;

        take X;

        let q;

        thus q in X implies (p ^ q) in T by A12;

        assume (p ^ q) in T;

        then q in ( NAT * ) & for r be FinSequence of NAT st q = r holds (p ^ r) in T by FINSEQ_1:def 11;

        hence thesis by A12;

      end;

      uniqueness

      proof

        let T1,T2 be Tree such that

         A23: q in T1 iff (p ^ q) in T and

         A24: q in T2 iff (p ^ q) in T;

        now

          let x be object;

          thus x in T1 implies x in T2

          proof

            assume

             A25: x in T1;

            then

            reconsider q = x as FinSequence of NAT by Th18;

            (p ^ q) in T by A23, A25;

            hence thesis by A24;

          end;

          assume

           A26: x in T2;

          then

          reconsider q = x as FinSequence of NAT by Th18;

          (p ^ q) in T by A24, A26;

          hence x in T1 by A23;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: TREES_1:31

    (T | ( <*> NAT )) = T

    proof

      

       A1: ( <*> NAT ) in T by Th21;

      thus (T | ( <*> NAT )) c= T

      proof

        let x be object;

        assume x in (T | ( <*> NAT ));

        then

        reconsider p = x as Element of (T | ( <*> NAT ));

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

        hence thesis by A1, Def6;

      end;

      let x be object;

      assume x in T;

      then

      reconsider p = x as Element of T;

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

      hence thesis by A1, Def6;

    end;

    registration

      let T be finite Tree;

      let p be Element of T;

      cluster (T | p) -> finite;

      coherence

      proof

        consider t be Function such that

         A1: ( rng t) = T and

         A2: ( dom t) in omega by FINSET_1:def 1;

        defpred P[ object, object] means ex q st (t . $1) = q & ((ex r st $2 = r & q = (p ^ r)) or (for r holds q <> (p ^ r)) & $2 = ( <*> NAT ));

        

         A3: for x be object st x in ( dom t) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( dom t);

          then (t . x) in T by A1, FUNCT_1:def 3;

          then

          reconsider q = (t . x) as FinSequence of NAT by Th18;

          (ex r st q = (p ^ r)) implies thesis;

          hence thesis;

        end;

        consider f be Function such that

         A4: ( dom f) = ( dom t) & for x be object st x in ( dom t) holds P[x, (f . x)] from CLASSES1:sch 1( A3);

        (T | p) is finite

        proof

          take f;

          thus ( rng f) c= (T | p)

          proof

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A5: y in ( dom f) and

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

            consider q such that

             A7: (t . y) = q and

             A8: (ex r st x = r & q = (p ^ r)) or (for r holds q <> (p ^ r)) & x = ( <*> NAT ) by A4, A5, A6;

            assume

             A9: not x in (T | p);

            (p ^ ( <*> NAT )) = p & q in T by A1, A4, A5, A7, FINSEQ_1: 34, FUNCT_1:def 3;

            hence contradiction by A8, A9, Def6;

          end;

          thus (T | p) c= ( rng f)

          proof

            let x be object;

            assume

             A10: x in (T | p);

            then

            reconsider q = x as FinSequence of NAT by Th18;

            (p ^ q) in T by A10, Def6;

            then

            consider y be object such that

             A11: y in ( dom t) and

             A12: (p ^ q) = (t . y) by A1, FUNCT_1:def 3;

             P[y, (f . y)] by A4, A11;

            then x = (f . y) by A12, FINSEQ_1: 33;

            hence thesis by A4, A11, FUNCT_1:def 3;

          end;

          thus thesis by A2, A4;

        end;

        hence thesis;

      end;

    end

    definition

      let T;

      assume

       A1: ( Leaves T) <> {} ;

      :: TREES_1:def7

      mode Leaf of T -> Element of T means it in ( Leaves T);

      existence

      proof

        set x = the Element of ( Leaves T);

        reconsider x as Element of T by A1, TARSKI:def 3;

        take x;

        thus thesis by A1;

      end;

    end

    definition

      let T;

      :: TREES_1:def8

      mode Subtree of T -> Tree means ex p be Element of T st it = (T | p);

      existence

      proof

        set p = the Element of T;

        take (T | p), p;

        thus thesis;

      end;

    end

    reserve t for Element of T;

    definition

      let T, p, T1;

      assume

       A1: p in T;

      :: TREES_1:def9

      func T with-replacement (p,T1) -> Tree means

      : Def9: q in it iff q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r);

      existence

      proof

        reconsider p9 = p as Element of T by A1;

         not p is_a_proper_prefix_of p9;

        then p in { t : not p is_a_proper_prefix_of t };

        then

        reconsider X = ({ t : not p is_a_proper_prefix_of t } \/ the set of all (p ^ s) where s be Element of T1) as non empty set;

        

         A2: x in { t : not p is_a_proper_prefix_of t } implies x is FinSequence of NAT & x in ( NAT * ) & x in T

        proof

          assume x in { t : not p is_a_proper_prefix_of t };

          then

           A3: ex t st x = t & not p is_a_proper_prefix_of t;

          hence x is FinSequence of NAT ;

          thus thesis by A3, FINSEQ_1:def 11;

        end;

        X is Tree-like

        proof

          thus X c= ( NAT * )

          proof

            let x be object;

            assume x in X;

            then

             A4: x in { t : not p is_a_proper_prefix_of t } or x in the set of all (p ^ s) where s be Element of T1 by XBOOLE_0:def 3;

            now

              assume x in the set of all (p ^ s) where s be Element of T1;

              then ex s be Element of T1 st x = (p ^ s);

              hence x is FinSequence of NAT ;

            end;

            hence thesis by A2, A4, FINSEQ_1:def 11;

          end;

          thus for q st q in X holds ( ProperPrefixes q) c= X

          proof

            let q such that

             A5: q in X;

             A6:

            now

              assume q in { t : not p is_a_proper_prefix_of t };

              then

               A7: ex t st q = t & not p is_a_proper_prefix_of t;

              then

               A8: ( ProperPrefixes q) c= T by Def3;

              thus ( ProperPrefixes q) c= X

              proof

                let x be object;

                assume

                 A9: x in ( ProperPrefixes q);

                then

                consider p1 such that

                 A10: x = p1 and

                 A11: p1 is_a_proper_prefix_of q by Def2;

                reconsider p1 as Element of T by A8, A9, A10;

                 not p is_a_proper_prefix_of p1 by A7, A11, XBOOLE_1: 56;

                then x in { s1 where s1 be Element of T : not p is_a_proper_prefix_of s1 } by A10;

                hence thesis by XBOOLE_0:def 3;

              end;

            end;

            now

              assume q in the set of all (p ^ s) where s be Element of T1;

              then

              consider s be Element of T1 such that

               A12: q = (p ^ s);

              thus ( ProperPrefixes q) c= X

              proof

                let x be object;

                assume

                 A13: x in ( ProperPrefixes q);

                then

                reconsider r = x as FinSequence by Th10;

                r is_a_proper_prefix_of (p ^ s) by A12, A13, Th11;

                then r is_a_prefix_of (p ^ s);

                then

                consider r1 be FinSequence such that

                 A14: (p ^ s) = (r ^ r1) by Th1;

                 A15:

                now

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

                  then

                  consider r2 be FinSequence such that

                   A16: (p ^ r2) = r by A14, FINSEQ_1: 47;

                  (p ^ s) = (p ^ (r2 ^ r1)) by A14, A16, FINSEQ_1: 32;

                  then s = (r2 ^ r1) by FINSEQ_1: 33;

                  then

                   A17: ( dom r2) = ( Seg ( len r2)) & (s | ( dom r2)) = r2 by FINSEQ_1: 21, FINSEQ_1:def 3;

                  then

                  reconsider r2 as FinSequence of NAT by FINSEQ_1: 18;

                  r2 is_a_prefix_of s by A17;

                  then

                  reconsider r2 as Element of T1 by Th19;

                  r = (p ^ r2) by A16;

                  then r in the set of all (p ^ v) where v be Element of T1;

                  hence r in X by XBOOLE_0:def 3;

                end;

                now

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

                  then ex r2 be FinSequence st (r ^ r2) = p by A14, FINSEQ_1: 47;

                  then

                   A18: (p | ( dom r)) = r by FINSEQ_1: 21;

                  

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

                  then

                  reconsider r3 = r as FinSequence of NAT by A18, FINSEQ_1: 18;

                  

                   A20: r3 is_a_prefix_of p by A18, A19;

                  then

                   A21: not p is_a_proper_prefix_of r3 by XBOOLE_0:def 8;

                  reconsider r3 as Element of T by A1, A20, Th19;

                  r3 in { t : not p is_a_proper_prefix_of t } by A21;

                  hence r in X by XBOOLE_0:def 3;

                end;

                hence thesis by A15;

              end;

            end;

            hence thesis by A5, A6, XBOOLE_0:def 3;

          end;

          let q, k, n such that

           A22: (q ^ <*k*>) in X and

           A23: n <= k;

           A24:

          now

            assume (q ^ <*k*>) in { t : not p is_a_proper_prefix_of t };

            then

             A25: ex s be Element of T st (q ^ <*k*>) = s & not p is_a_proper_prefix_of s;

            then

            reconsider u = (q ^ <*n*>) as Element of T by A23, Def3;

            now

              assume p is_a_proper_prefix_of u;

              then p is_a_prefix_of q by Th8;

              hence contradiction by A25, Th7;

            end;

            then (q ^ <*n*>) in { t : not p is_a_proper_prefix_of t };

            hence thesis by XBOOLE_0:def 3;

          end;

          now

            assume (q ^ <*k*>) in the set of all (p ^ s) where s be Element of T1;

            then

            consider s be Element of T1 such that

             A26: (q ^ <*k*>) = (p ^ s);

             A27:

            now

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

              then

              consider r be FinSequence such that

               A28: (q ^ r) = p by A26, FINSEQ_1: 47;

              (q ^ <*k*>) = (q ^ (r ^ s)) by A26, A28, FINSEQ_1: 32;

              then

               A29: <*k*> = (r ^ s) by FINSEQ_1: 33;

               A30:

              now

                assume

                 A31: r = <*k*>;

                then

                reconsider s = (q ^ <*n*>) as Element of T by A1, A23, A28, Def3;

                now

                  assume

                   A32: p is_a_proper_prefix_of s;

                  ( len p) = (( len q) + ( len <*k*>)) by A28, A31, FINSEQ_1: 22

                  .= (( len q) + 1) by FINSEQ_1: 40

                  .= (( len q) + ( len <*n*>)) by FINSEQ_1: 40

                  .= ( len s) by FINSEQ_1: 22;

                  hence contradiction by A32, CARD_2: 102;

                end;

                hence (q ^ <*n*>) in { t : not p is_a_proper_prefix_of t };

              end;

              now

                assume that

                 A33: s = <*k*> and

                 A34: r = {} ;

                s = ( {} ^ s) & {} = ( <*> NAT ) by FINSEQ_1: 34;

                then ( {} ^ <*n*>) in T1 by A23, A33, Def3;

                then

                reconsider t = <*n*> as Element of T1 by FINSEQ_1: 34;

                (q ^ <*n*>) = (p ^ t) by A28, A34, FINSEQ_1: 34;

                hence (q ^ <*n*>) in the set of all (p ^ v) where v be Element of T1;

              end;

              hence thesis by A29, A30, FINSEQ_1: 88, XBOOLE_0:def 3;

            end;

            now

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

              then

              consider r be FinSequence such that

               A35: (p ^ r) = q by A26, FINSEQ_1: 47;

              (p ^ (r ^ <*k*>)) = (p ^ s) by A26, A35, FINSEQ_1: 32;

              then

               A36: (r ^ <*k*>) = s by FINSEQ_1: 33;

              then ( dom r) = ( Seg ( len r)) & (s | ( dom r)) = r by FINSEQ_1: 21, FINSEQ_1:def 3;

              then

              reconsider r as FinSequence of NAT by FINSEQ_1: 18;

              reconsider t = (r ^ <*n*>) as Element of T1 by A23, A36, Def3;

              (q ^ <*n*>) = (p ^ t) by A35, FINSEQ_1: 32;

              then (q ^ <*n*>) in the set of all (p ^ v) where v be Element of T1;

              hence thesis by XBOOLE_0:def 3;

            end;

            hence thesis by A27;

          end;

          hence thesis by A22, A24, XBOOLE_0:def 3;

        end;

        then

        reconsider X as Tree;

        take X;

        let q;

        thus q in X implies q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r)

        proof

          assume

           A37: q in X;

           A38:

          now

            assume q in { t : not p is_a_proper_prefix_of t };

            then ex s be Element of T st q = s & not p is_a_proper_prefix_of s;

            hence thesis;

          end;

          now

            assume q in the set of all (p ^ s) where s be Element of T1;

            then ex s be Element of T1 st q = (p ^ s);

            hence ex r st r in T1 & q = (p ^ r);

          end;

          hence thesis by A37, A38, XBOOLE_0:def 3;

        end;

        assume

         A39: q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r);

        

         A40: q in T & not p is_a_proper_prefix_of q implies q in { t : not p is_a_proper_prefix_of t };

        (ex r st r in T1 & q = (p ^ r)) implies q in the set of all (p ^ v) where v be Element of T1;

        hence thesis by A39, A40, XBOOLE_0:def 3;

      end;

      uniqueness

      proof

        let S1,S2 be Tree such that

         A41: q in S1 iff q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r) and

         A42: q in S2 iff q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r);

        thus S1 c= S2

        proof

          let x be object;

          assume

           A43: x in S1;

          then

          reconsider q = x as FinSequence of NAT by Th18;

          q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r) by A41, A43;

          hence thesis by A42;

        end;

        let x be object;

        assume

         A44: x in S2;

        then

        reconsider q = x as FinSequence of NAT by Th18;

        q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = (p ^ r) by A42, A44;

        hence thesis by A41;

      end;

    end

    theorem :: TREES_1:32

    

     Th31: p in T implies (T with-replacement (p,T1)) = ({ t1 where t1 be Element of T : not p is_a_proper_prefix_of t1 } \/ the set of all (p ^ s) where s be Element of T1)

    proof

      assume

       A1: p in T;

      thus (T with-replacement (p,T1)) c= ({ t : not p is_a_proper_prefix_of t } \/ the set of all (p ^ s) where s be Element of T1)

      proof

        let x be object;

        assume

         A2: x in (T with-replacement (p,T1));

        then

        reconsider q = x as FinSequence of NAT by Th18;

        

         A3: (ex r st r in T1 & q = (p ^ r)) implies x in the set of all (p ^ s) where s be Element of T1;

        q in T & not p is_a_proper_prefix_of q implies x in { t : not p is_a_proper_prefix_of t };

        hence thesis by A1, A2, A3, Def9, XBOOLE_0:def 3;

      end;

      let x be object such that

       A4: x in ({ t : not p is_a_proper_prefix_of t } \/ the set of all (p ^ s) where s be Element of T1);

       A5:

      now

        assume x in the set of all (p ^ s) where s be Element of T1;

        then ex s be Element of T1 st x = (p ^ s);

        hence thesis by A1, Def9;

      end;

      now

        assume x in { t : not p is_a_proper_prefix_of t };

        then ex t st x = t & not p is_a_proper_prefix_of t;

        hence thesis by A1, Def9;

      end;

      hence thesis by A4, A5, XBOOLE_0:def 3;

    end;

    theorem :: TREES_1:33

    p in T implies T1 = ((T with-replacement (p,T1)) | p)

    proof

      assume

       A1: p in T;

      then

       A2: p in (T with-replacement (p,T1)) by Def9;

      thus T1 c= ((T with-replacement (p,T1)) | p)

      proof

        let x be object;

        assume

         A3: x in T1;

        then

        reconsider q = x as FinSequence of NAT by Th18;

        (p ^ q) in (T with-replacement (p,T1)) by A1, A3, Def9;

        hence thesis by A2, Def6;

      end;

      let x be object;

      assume

       A4: x in ((T with-replacement (p,T1)) | p);

      then

      reconsider q = x as FinSequence of NAT by Th18;

      

       A5: (p ^ q) in (T with-replacement (p,T1)) by A2, A4, Def6;

       A6:

      now

        assume that (p ^ q) in T and

         A7: not p is_a_proper_prefix_of (p ^ q);

        p is_a_prefix_of (p ^ q) by Th1;

        

        then (p ^ q) = p by A7

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

        then q = {} by FINSEQ_1: 33;

        hence q in T1 by Th21;

      end;

      (ex r st r in T1 & (p ^ q) = (p ^ r)) implies q in T1 by FINSEQ_1: 33;

      hence thesis by A1, A5, A6, Def9;

    end;

    registration

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

      let T1 be finite Tree;

      cluster (T with-replacement (t,T1)) -> finite;

      coherence

      proof

        

         A1: { s where s be Element of T : not t is_a_proper_prefix_of s } c= T

        proof

          let x be object;

          assume x in { s where s be Element of T : not t is_a_proper_prefix_of s };

          then ex s be Element of T st x = s & not t is_a_proper_prefix_of s;

          hence thesis;

        end;

        (T1, the set of all (t ^ s) where s be Element of T1) are_equipotent

        proof

          defpred P[ object, object] means ex q st $1 = q & $2 = (t ^ q);

          

           A2: for x be object holds x in T1 implies ex y be object st P[x, y]

          proof

            let x be object;

            assume x in T1;

            then

            reconsider q = x as FinSequence of NAT by Th18;

            (t ^ q) = (t ^ q);

            hence thesis;

          end;

          consider f such that

           A3: ( dom f) = T1 & for x be object st x in T1 holds P[x, (f . x)] from CLASSES1:sch 1( A2);

          take f;

          thus f is one-to-one

          proof

            let x,y be object;

            assume that

             A4: x in ( dom f) & y in ( dom f) and

             A5: (f . x) = (f . y);

            (ex q st x = q & (f . x) = (t ^ q)) & ex r st y = r & (f . y) = (t ^ r) by A3, A4;

            hence thesis by A5, FINSEQ_1: 33;

          end;

          thus ( dom f) = T1 by A3;

          thus ( rng f) c= the set of all (t ^ s) where s be Element of T1

          proof

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A6: y in ( dom f) and

             A7: x = (f . y) by FUNCT_1:def 3;

            consider q such that

             A8: y = q and

             A9: (f . y) = (t ^ q) by A3, A6;

            reconsider q as Element of T1 by A3, A6, A8;

            x = (t ^ q) by A7, A9;

            hence thesis;

          end;

          let x be object;

          assume x in the set of all (t ^ s) where s be Element of T1;

          then

          consider s be Element of T1 such that

           A10: x = (t ^ s);

           P[s, (f . s)] by A3;

          hence thesis by A3, A10, FUNCT_1:def 3;

        end;

        then the set of all (t ^ s) where s be Element of T1 is finite by CARD_1: 38;

        then ({ v where v be Element of T : not t is_a_proper_prefix_of v } \/ the set of all (t ^ s) where s be Element of T1) is finite by A1;

        hence thesis by Th31;

      end;

    end

    reserve w for FinSequence;

    theorem :: TREES_1:34

    

     Th33: for p be FinSequence holds (( ProperPrefixes p),( dom p)) are_equipotent

    proof

      let p be FinSequence;

      defpred P[ object, object] means ex w st $1 = w & $2 = (( len w) + 1);

      

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

      proof

        let x be object;

        assume x in ( ProperPrefixes p);

        then

        consider q be FinSequence such that

         A2: x = q and q is_a_proper_prefix_of p by Def2;

        reconsider y = (( len q) + 1) as set;

        take y, q;

        thus thesis by A2;

      end;

      consider f such that

       A3: ( dom f) = ( ProperPrefixes p) and

       A4: for x be object st x in ( ProperPrefixes p) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      take f;

      thus f is one-to-one

      proof

        let x,y be object;

        assume that

         A5: x in ( dom f) & y in ( dom f) and

         A6: (f . x) = (f . y);

        (ex q be FinSequence st x = q & (f . x) = (( len q) + 1)) & ex r be FinSequence st y = r & (f . x) = (( len r) + 1) by A3, A4, A5, A6;

        hence thesis by A3, A5, Th3, Th17;

      end;

      thus ( dom f) = ( ProperPrefixes p) by A3;

      thus ( rng f) c= ( dom p)

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A7: y in ( dom f) and

         A8: x = (f . y) by FUNCT_1:def 3;

        consider q be FinSequence such that

         A9: y = q and

         A10: x = (( len q) + 1) by A3, A4, A7, A8;

        ( len q) < ( len p) by A3, A7, A9, Th12;

        then ( 0 + 1) <= (( len q) + 1) & (( len q) + 1) <= ( len p) by NAT_1: 13;

        then x in ( Seg ( len p)) by A10, FINSEQ_1: 1;

        hence thesis by FINSEQ_1:def 3;

      end;

      let x be object;

      assume

       A11: x in ( dom p);

      then

       A12: x in ( Seg ( len p)) by FINSEQ_1:def 3;

      reconsider n = x as Nat by A11;

      

       A13: 1 <= n by A12, FINSEQ_1: 1;

      

       A14: n <= ( len p) by A12, FINSEQ_1: 1;

      consider m be Nat such that

       A15: n = (1 + m) by A13, NAT_1: 10;

      reconsider m as Nat;

      reconsider q = (p | ( Seg m)) as FinSequence by FINSEQ_1: 15;

      

       A16: m <= ( len p) by A14, A15, NAT_1: 13;

      

       A17: m <> ( len p) by A14, A15, NAT_1: 13;

      

       A18: ( len q) = m by A16, FINSEQ_1: 17;

      

       A19: q is_a_prefix_of p;

      ( len q) = m by A16, FINSEQ_1: 17;

      then q is_a_proper_prefix_of p by A17, A19;

      then

       A20: q in ( ProperPrefixes p) by Th11;

      then ex r be FinSequence st q = r & (f . q) = (( len r) + 1) by A4;

      hence thesis by A3, A15, A18, A20, FUNCT_1:def 3;

    end;

    registration

      let p be FinSequence;

      cluster ( ProperPrefixes p) -> finite;

      coherence

      proof

        (( ProperPrefixes p),( dom p)) are_equipotent by Th33;

        hence thesis by CARD_1: 38;

      end;

    end

    theorem :: TREES_1:35

    for p be FinSequence holds ( card ( ProperPrefixes p)) = ( len p)

    proof

      let p be FinSequence;

      

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

      

       A2: (( ProperPrefixes p),( dom p)) are_equipotent by Th33;

      ( card ( dom p)) = ( card ( len p)) by A1, FINSEQ_1: 55;

      hence thesis by A2, CARD_1: 5;

    end;

    definition

      let IT be set;

      :: TREES_1:def10

      attr IT is AntiChain_of_Prefixes-like means

      : Def10: (for x st x in IT holds x is FinSequence) & for p1, p2 st p1 in IT & p2 in IT & p1 <> p2 holds not (p1,p2) are_c=-comparable ;

    end

    registration

      cluster AntiChain_of_Prefixes-like for set;

      existence

      proof

        take {} ;

        thus for x st x in {} holds x is FinSequence;

        let p1, p2;

        thus thesis;

      end;

    end

    definition

      mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set;

    end

    theorem :: TREES_1:36

    

     Th35: {w} is AntiChain_of_Prefixes-like

    proof

      thus for x st x in {w} holds x is FinSequence by TARSKI:def 1;

      let p1, p2;

      assume that

       A1: p1 in {w} and

       A2: p2 in {w};

      p1 = w by A1, TARSKI:def 1;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: TREES_1:37

    

     Th36: not (p1,p2) are_c=-comparable implies {p1, p2} is AntiChain_of_Prefixes-like

    proof

      assume

       A1: not (p1,p2) are_c=-comparable ;

      thus for x st x in {p1, p2} holds x is FinSequence by TARSKI:def 2;

      let q1,q2 be FinSequence;

      assume that

       A2: q1 in {p1, p2} and

       A3: q2 in {p1, p2};

      

       A4: q1 = p1 or q1 = p2 by A2, TARSKI:def 2;

      q2 = p1 or q2 = p2 by A3, TARSKI:def 2;

      hence thesis by A1, A4;

    end;

    definition

      let T;

      :: TREES_1:def11

      mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means

      : Def11: it c= T;

      existence

      proof

        set t = the Element of T;

        reconsider S = {t} as AntiChain_of_Prefixes by Th35;

        take S;

        let x be object;

        assume x in S;

        then x = t by TARSKI:def 1;

        hence thesis;

      end;

    end

    reserve t1,t2 for Element of T;

    theorem :: TREES_1:38

    

     Th37: {} is AntiChain_of_Prefixes of T & { {} } is AntiChain_of_Prefixes of T

    proof

       {} is AntiChain_of_Prefixes-like;

      then

      reconsider S = {} as AntiChain_of_Prefixes;

      S c= T;

      hence {} is AntiChain_of_Prefixes of T by Def11;

      reconsider S = D as AntiChain_of_Prefixes by Th35;

      S is AntiChain_of_Prefixes of T

      proof

        let x be object;

        assume x in S;

        then x = {} by TARSKI:def 1;

        hence thesis by Th21;

      end;

      hence thesis;

    end;

    theorem :: TREES_1:39

     {t} is AntiChain_of_Prefixes of T

    proof

      reconsider S = {t} as AntiChain_of_Prefixes by Th35;

      S is AntiChain_of_Prefixes of T

      proof

        let x be object;

        assume x in S;

        then x = t by TARSKI:def 1;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TREES_1:40

     not (t1,t2) are_c=-comparable implies {t1, t2} is AntiChain_of_Prefixes of T

    proof

      assume not (t1,t2) are_c=-comparable ;

      then

      reconsider A = {t1, t2} as AntiChain_of_Prefixes by Th36;

      A is AntiChain_of_Prefixes of T

      proof

        let x be object;

        assume x in A;

        then x = t1 or x = t2 by TARSKI:def 2;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let T be finite Tree;

      cluster -> finite for AntiChain_of_Prefixes of T;

      coherence

      proof

        let X be AntiChain_of_Prefixes of T;

        X c= T by Def11;

        hence thesis;

      end;

    end

    definition

      let T be finite Tree;

      :: TREES_1:def12

      func height T -> Nat means

      : Def12: (ex p st p in T & ( len p) = it ) & for p st p in T holds ( len p) <= it ;

      existence

      proof

        consider n be Nat such that

         A1: (T,( Seg n)) are_equipotent by FINSEQ_1: 56;

        defpred X[ Nat] means for p st p in T holds ( len p) <= $1;

        

         A2: ex n be Nat st X[n]

        proof

          now

            given p such that

             A3: p in T and

             A4: not ( len p) <= n;

            

             A5: ( ProperPrefixes p) c= T by A3, Def3;

            

             A6: (( ProperPrefixes p),( dom p)) are_equipotent by Th33;

            

             A7: ( card ( ProperPrefixes p)) c= ( card T) by A5, CARD_1: 11;

            

             A8: ( card ( ProperPrefixes p)) = ( card ( dom p)) by A6, CARD_1: 5;

            

             A9: ( card T) = ( card ( Seg n)) & ( dom p) = ( Seg ( len p)) by A1, CARD_1: 5, FINSEQ_1:def 3;

            ( Seg n) c= ( Seg ( len p)) by A4, FINSEQ_1: 5;

            then

             A10: ( card ( Seg n)) c= ( card ( Seg ( len p))) by CARD_1: 11;

            ( card ( Seg n)) = ( card n) & ( card ( Seg ( len p))) = ( card ( len p)) by FINSEQ_1: 55;

            then ( card n) = ( card ( len p)) by A7, A8, A9, A10;

            hence contradiction by A4;

          end;

          then

          consider n be Nat such that

           A11: X[n];

          reconsider n as Nat;

          take n;

          thus thesis by A11;

        end;

        consider n be Nat such that

         A12: X[n] and

         A13: for m be Nat st X[m] holds n <= m from NAT_1:sch 5( A2);

        set x = the Element of T;

        reconsider n as Nat;

        take n;

        thus ex p st p in T & ( len p) = n

        proof

          assume

           A14: for p st p in T holds ( len p) <> n;

          reconsider x as FinSequence of NAT ;

          ( len x) <= n by A12;

          then ( len x) < n by A14, XXREAL_0: 1;

          then

          consider k be Nat such that

           A15: n = (k + 1) by NAT_1: 6;

          reconsider k as Nat;

          for p st p in T holds ( len p) <= k

          proof

            let p;

            assume

             A16: p in T;

            then ( len p) <= n by A12;

            then ( len p) < (k + 1) by A14, A15, A16, XXREAL_0: 1;

            hence thesis by NAT_1: 13;

          end;

          then n <= k by A13;

          hence contradiction by A15, NAT_1: 13;

        end;

        let p;

        assume p in T;

        hence thesis by A12;

      end;

      uniqueness

      proof

        let l1,l2 be Nat;

        given p1 be FinSequence of NAT such that

         A17: p1 in T & ( len p1) = l1;

        assume

         A18: for p st p in T holds ( len p) <= l1;

        given p2 be FinSequence of NAT such that

         A19: p2 in T & ( len p2) = l2;

        assume for p st p in T holds ( len p) <= l2;

        then

         A20: l1 <= l2 by A17;

        l2 <= l1 by A18, A19;

        hence thesis by A20, XXREAL_0: 1;

      end;

      :: TREES_1:def13

      func width T -> Nat means

      : Def13: ex X be AntiChain_of_Prefixes of T st it = ( card X) & for Y be AntiChain_of_Prefixes of T holds ( card Y) <= ( card X);

      existence

      proof

        defpred X[ Nat] means ex X be finite set st $1 = ( card X) & X c= T & (for p, q st p in X & q in X & p <> q holds not (p,q) are_c=-comparable );

         0 = ( card {} ) & for p, q st p in {} & q in {} & p <> q holds not (p,q) are_c=-comparable ;

        then

         A21: ex n be Nat st X[n] by XBOOLE_1: 2;

        

         A22: for n be Nat st X[n] holds n <= ( card T)

        proof

          let n be Nat;

          given X be finite set such that

           A23: n = ( card X) & X c= T and for p, q st p in X & q in X & p <> q holds not (p,q) are_c=-comparable ;

          

           A24: ( Segm ( card X)) c= ( Segm ( card T)) & ( card X) = ( card n) by A23, CARD_1: 11;

          ( card T) = ( card ( Segm ( card T)));

          hence thesis by A24, NAT_1: 40;

        end;

        consider n be Nat such that

         A25: X[n] and

         A26: for m be Nat st X[m] holds m <= n from NAT_1:sch 6( A22, A21);

        consider X be finite set such that

         A27: n = ( card X) and

         A28: X c= T and

         A29: for p, q st p in X & q in X & p <> q holds not (p,q) are_c=-comparable by A25;

        X is AntiChain_of_Prefixes-like

        proof

          thus for x st x in X holds x is FinSequence

          proof

            let x;

            assume

             A30: x in X;

            T c= ( NAT * ) by Def3;

            hence thesis by A30, A28;

          end;

          let p1, p2;

          assume

           A31: p1 in X & p2 in X;

          then

          reconsider q1 = p1, q2 = p2 as Element of T by A28;

          p1 = q1 & p2 = q2;

          hence thesis by A29, A31;

        end;

        then

        reconsider X as AntiChain_of_Prefixes;

        reconsider X as AntiChain_of_Prefixes of T by A28, Def11;

        reconsider n as Nat;

        take n, X;

        thus n = ( card X) by A27;

        let Y be AntiChain_of_Prefixes of T;

        Y c= T & for p, q st p in Y & q in Y & p <> q holds not (p,q) are_c=-comparable by Def10, Def11;

        hence thesis by A26, A27;

      end;

      uniqueness

      proof

        let n1,n2 be Nat;

        given X1 be AntiChain_of_Prefixes of T such that

         A32: n1 = ( card X1) and

         A33: for Y be AntiChain_of_Prefixes of T holds ( card Y) <= ( card X1);

        given X2 be AntiChain_of_Prefixes of T such that

         A34: n2 = ( card X2) and

         A35: for Y be AntiChain_of_Prefixes of T holds ( card Y) <= ( card X2);

        

         A36: ( card X1) <= ( card X2) by A35;

        ( card X2) <= ( card X1) by A33;

        hence thesis by A32, A34, A36, XXREAL_0: 1;

      end;

    end

    theorem :: TREES_1:41

    1 <= ( width fT)

    proof

      (ex X be AntiChain_of_Prefixes of fT st ( width fT) = ( card X) & for Y be AntiChain_of_Prefixes of fT holds ( card Y) <= ( card X)) & D is AntiChain_of_Prefixes of fT by Def13, Th37;

      then ( card D) <= ( width fT);

      hence thesis by CARD_1: 30;

    end;

    theorem :: TREES_1:42

    ( height ( elementary_tree 0 )) = 0

    proof

      now

        thus ex p st p in ( elementary_tree 0 ) & ( len p) = 0

        proof

          take ( <*> NAT );

          thus thesis by Th28, TARSKI:def 1;

        end;

        let p;

        assume p in ( elementary_tree 0 );

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

        hence ( len p) <= 0 ;

      end;

      hence thesis by Def12;

    end;

    theorem :: TREES_1:43

    ( height fT) = 0 implies fT = ( elementary_tree 0 )

    proof

      assume

       A1: ( height fT) = 0 ;

      thus fT c= ( elementary_tree 0 )

      proof

        let x be object;

        assume x in fT;

        then

        reconsider t = x as Element of fT;

        ( len t) = 0 by A1, Def12;

        then x = {} ;

        hence thesis by Th21;

      end;

      let x be object;

      assume x in ( elementary_tree 0 );

      then x = {} by Th28, TARSKI:def 1;

      hence thesis by Th21;

    end;

    theorem :: TREES_1:44

    ( height ( elementary_tree (n + 1))) = 1

    proof

      set T = ( elementary_tree (n + 1));

      now

        thus ex p st p in T & ( len p) = 1

        proof

          take p = <* 0 *>;

          thus p in T by Th27;

          thus thesis by FINSEQ_1: 40;

        end;

        let p such that

         A1: p in T;

        

         A2: p in D implies p = {} by TARSKI:def 1;

        now

          assume p in { <*k*> : k < (n + 1) };

          then ex k st p = <*k*> & k < (n + 1);

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

        end;

        hence ( len p) <= 1 by A1, A2, XBOOLE_0:def 3;

      end;

      hence thesis by Def12;

    end;

    theorem :: TREES_1:45

    ( width ( elementary_tree 0 )) = 1

    proof

      set T = ( elementary_tree 0 );

      now

        reconsider X = D as AntiChain_of_Prefixes of T by Th37;

        take X;

        thus 1 = ( card X) by CARD_1: 30;

        let Y be AntiChain_of_Prefixes of T;

        Y c= X by Def11, Th28;

        hence ( card Y) <= ( card X) by NAT_1: 43;

      end;

      hence thesis by Def13;

    end;

    theorem :: TREES_1:46

    ( width ( elementary_tree (n + 1))) = (n + 1)

    proof

      set T = ( elementary_tree (n + 1));

      now

        { <*k*> : k < (n + 1) } is AntiChain_of_Prefixes-like

        proof

          thus x in { <*k*> : k < (n + 1) } implies x is FinSequence

          proof

            assume x in { <*k*> : k < (n + 1) };

            then ex k st x = <*k*> & k < (n + 1);

            hence thesis;

          end;

          let p1, p2;

          assume p1 in { <*k*> : k < (n + 1) } & p2 in { <*m*> : m < (n + 1) };

          then (ex k st p1 = <*k*> & k < (n + 1)) & ex m st p2 = <*m*> & m < (n + 1);

          hence thesis by Th4;

        end;

        then

        reconsider X = { <*k*> : k < (n + 1) } as AntiChain_of_Prefixes;

        X c= T by XBOOLE_1: 7;

        then

        reconsider X as AntiChain_of_Prefixes of T by Def11;

        take X;

        (X,( Seg (n + 1))) are_equipotent

        proof

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

          

           A1: x in X & P[x, y] & P[x, z] implies y = z

          proof

            assume x in X;

            given n1 be Nat such that

             A2: x = <*n1*> & y = (n1 + 1);

            given n2 be Nat such that

             A3: x = <*n2*> & z = (n2 + 1);

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

            hence thesis by A2, A3, FINSEQ_1:def 8;

          end;

          

           A4: for x be object holds x in X implies ex y be object st P[x, y]

          proof

            let x be object;

            assume x in X;

            then

            consider k such that

             A5: x = <*k*> and k < (n + 1);

            reconsider y = (k + 1) as set;

            take y;

            thus thesis by A5;

          end;

          consider f such that

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

          take f;

          thus f is one-to-one

          proof

            let x,y be object;

            assume that

             A7: x in ( dom f) & y in ( dom f) and

             A8: (f . x) = (f . y);

            (ex k1 be Nat st x = <*k1*> & (f . x) = (k1 + 1)) & ex k2 be Nat st y = <*k2*> & (f . y) = (k2 + 1) by A6, A7;

            hence thesis by A8;

          end;

          thus ( dom f) = X by A6;

          thus ( rng f) c= ( Seg (n + 1))

          proof

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A9: y in ( dom f) and

             A10: x = (f . y) by FUNCT_1:def 3;

            consider k such that

             A11: y = <*k*> and

             A12: x = (k + 1) by A6, A9, A10;

            consider m such that

             A13: y = <*m*> & m < (n + 1) by A6, A9;

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

            then ( 0 + 1) <= (k + 1) & (k + 1) <= (n + 1) by A11, A13, NAT_1: 13;

            hence thesis by A12, FINSEQ_1: 1;

          end;

          let x be object;

          assume

           A14: x in ( Seg (n + 1));

          then

          reconsider k = x as Nat;

          

           A15: 1 <= k by A14, FINSEQ_1: 1;

          

           A16: k <= (n + 1) by A14, FINSEQ_1: 1;

          consider m be Nat such that

           A17: k = (1 + m) by A15, NAT_1: 10;

          reconsider m as Nat;

          m < (n + 1) by A16, A17, NAT_1: 13;

          then

           A18: <*m*> in X;

          then P[ <*m*>, (f . <*m*>)] by A6;

          then x = (f . <*m*>) by A1, A17, A18;

          hence thesis by A6, A18, FUNCT_1:def 3;

        end;

        then

         A19: ( card ( Seg (n + 1))) = ( card X) by CARD_1: 5;

        hence (n + 1) = ( card X) by FINSEQ_1: 57;

        let Y be AntiChain_of_Prefixes of T;

        

         A20: Y c= T by Def11;

        

         A21: {} in Y implies Y = D

        proof

          assume that

           A22: {} in Y and

           A23: Y <> D;

          consider x be object such that

           A24: not (x in Y iff x in D) by A23, TARSKI: 2;

          

           A25: {} <> x by A22, A24, TARSKI:def 1;

          reconsider x as FinSequence of NAT by A20, A24, Th18;

           {} is_a_prefix_of x;

          then ( {} ,x) are_c=-comparable ;

          hence contradiction by A22, A24, A25, Def10, TARSKI:def 1;

        end;

        

         A26: ( card D) = 1 & 1 <= (1 + n) by CARD_1: 30, NAT_1: 11;

        now

          assume

           A27: not {} in Y;

          Y c= X

          proof

            let x be object;

            assume

             A28: x in Y;

            then x in { <*k*> : k < (n + 1) } or x in D by A20, XBOOLE_0:def 3;

            hence thesis by A27, A28, TARSKI:def 1;

          end;

          hence ( card Y) <= ( card X) by NAT_1: 43;

        end;

        hence ( card Y) <= ( card X) by A19, A21, A26, FINSEQ_1: 57;

      end;

      hence thesis by Def13;

    end;

    theorem :: TREES_1:47

    for t be Element of fT holds ( height (fT | t)) <= ( height fT)

    proof

      let t be Element of fT;

      consider p such that

       A1: p in (fT | t) and

       A2: ( len p) = ( height (fT | t)) by Def12;

      (t ^ p) in fT by A1, Def6;

      then

       A3: ( len (t ^ p)) <= ( height fT) by Def12;

      ( len (t ^ p)) = (( len t) + ( len p)) & ( len p) <= (( len p) + ( len t)) by FINSEQ_1: 22, NAT_1: 11;

      hence thesis by A2, A3, XXREAL_0: 2;

    end;

    theorem :: TREES_1:48

    

     Th47: for t be Element of fT st t <> {} holds ( height (fT | t)) < ( height fT)

    proof

      let t be Element of fT;

      assume t <> {} ;

      then

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

      consider p such that

       A2: p in (fT | t) and

       A3: ( len p) = ( height (fT | t)) by Def12;

      (t ^ p) in fT by A2, Def6;

      then

       A4: ( len (t ^ p)) <= ( height fT) by Def12;

      ( len (t ^ p)) = (( len t) + ( len p)) & (( len p) + 1) <= (( len t) + ( len p)) by A1, FINSEQ_1: 22, XREAL_1: 7;

      then (( height (fT | t)) + 1) <= ( height fT) by A3, A4, XXREAL_0: 2;

      hence thesis by NAT_1: 13;

    end;

    scheme :: TREES_1:sch1

    TreeInd { P[ Tree] } :

for fT holds P[fT]

      provided

       A1: for fT st for n be Element of NAT st <*n*> in fT holds P[(fT | <*n*>)] holds P[fT];

      defpred X[ set] means for fT holds ( height fT) = $1 implies P[fT];

      

       A2: for n be Nat st for k be Nat st k < n holds X[k] holds X[n]

      proof

        let n be Nat such that

         A3: for k be Nat st k < n holds for fT st ( height fT) = k holds P[fT];

        let fT such that

         A4: ( height fT) = n;

        now

          let k be Element of NAT ;

          assume <*k*> in fT;

          then

          reconsider k9 = <*k*> as Element of fT;

          ( height (fT | k9)) < ( height fT) by Th47;

          hence P[(fT | <*k*>)] by A3, A4;

        end;

        hence thesis by A1;

      end;

      

       A5: for n be Nat holds X[n] from NAT_1:sch 4( A2);

      let fT;

      ( height fT) = ( height fT);

      hence thesis by A5;

    end;

    begin

    reserve s,t for FinSequence;

    theorem :: TREES_1:49

    (w ^ t) is_a_proper_prefix_of (w ^ s) implies t is_a_proper_prefix_of s

    proof

      assume

       A1: (w ^ t) is_a_proper_prefix_of (w ^ s);

      then (w ^ t) is_a_prefix_of (w ^ s);

      then

      consider a be FinSequence such that

       A2: (w ^ s) = ((w ^ t) ^ a) by Th1;

      ((w ^ t) ^ a) = (w ^ (t ^ a)) by FINSEQ_1: 32;

      then s = (t ^ a) by A2, FINSEQ_1: 33;

      then t is_a_prefix_of s by Th1;

      hence thesis by A1;

    end;

    theorem :: TREES_1:50

    n <> m implies not <*n*> is_a_prefix_of ( <*m*> ^ s)

    proof

      assume

       A1: n <> m;

      assume <*n*> is_a_prefix_of ( <*m*> ^ s);

      then

       A2: ex a be FinSequence st ( <*m*> ^ s) = ( <*n*> ^ a) by Th1;

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

      .= n by A2, FINSEQ_1: 41;

      hence contradiction by A1;

    end;

    theorem :: TREES_1:51

    ( elementary_tree 1) = { {} , <* 0 *>}

    proof

      now

        let x be object;

        thus x in { {} , <* 0 *>} implies x in { <*n*> : n < 1 } or x in D

        proof

          assume x in { {} , <* 0 *>};

          then x = {} or x = <* 0 *> by TARSKI:def 2;

          hence thesis by TARSKI:def 1;

        end;

        assume

         A1: x in { <*n*> : n < 1 } or x in D;

        now

          per cases by A1;

            suppose x in { <*n*> : n < 1 };

            then

            consider n such that

             A2: x = <*n*> and

             A3: n < 1;

            n = 0 by A3, NAT_1: 25;

            hence x in { {} , <* 0 *>} by A2, TARSKI:def 2;

          end;

            suppose x in D;

            then x = {} by TARSKI:def 1;

            hence x in { {} , <* 0 *>} by TARSKI:def 2;

          end;

        end;

        hence x in { {} , <* 0 *>};

      end;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TREES_1:52

     not <*n*> is_a_proper_prefix_of <*m*> by Th2;

    theorem :: TREES_1:53

    ( elementary_tree 2) = { {} , <* 0 *>, <*1*>}

    proof

      now

        let x be object;

        thus x in { {} , <* 0 *>, <*1*>} implies x in { <*n*> : n < 2 } or x in D

        proof

          assume x in { {} , <* 0 *>, <*1*>};

          then x = {} or x = <* 0 *> or x = <*1*> by ENUMSET1:def 1;

          hence thesis by TARSKI:def 1;

        end;

        assume

         A1: x in { <*n*> : n < 2 } or x in D;

        now

          per cases by A1;

            suppose x in { <*n*> : n < 2 };

            then

            consider n such that

             A2: x = <*n*> and

             A3: n < 2;

            n = 0 or ... or n = 2 by A3;

            hence x in { {} , <* 0 *>, <*1*>} by A2, A3, ENUMSET1:def 1;

          end;

            suppose x in D;

            then x = {} by TARSKI:def 1;

            hence x in { {} , <* 0 *>, <*1*>} by ENUMSET1:def 1;

          end;

        end;

        hence x in { {} , <* 0 *>, <*1*>};

      end;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TREES_1:54

    for T be Tree, t be Element of T holds t in ( Leaves T) iff not (t ^ <* 0 *>) in T

    proof

      let T be Tree, t be Element of T;

      hereby

        assume

         A1: t in ( Leaves T);

        t is_a_proper_prefix_of (t ^ <* 0 *>) by Th6;

        hence not (t ^ <* 0 *>) in T by A1, Def5;

      end;

      assume that

       A2: not (t ^ <* 0 *>) in T and

       A3: not t in ( Leaves T);

      consider q be FinSequence of NAT such that

       A4: q in T and

       A5: t is_a_proper_prefix_of q by A3, Def5;

      t is_a_prefix_of q by A5;

      then

      consider r be FinSequence such that

       A6: q = (t ^ r) by Th1;

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

      ( len q) = (( len t) + ( len r)) by A6, FINSEQ_1: 22;

      then ( len r) <> 0 by A5, Th5;

      then r <> {} ;

      then

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

       A7: r = ( <*x*> ^ p) by FINSEQ_2: 130;

      q = ((t ^ <*x*>) ^ p) by A6, A7, FINSEQ_1: 32;

      then (t ^ <*x*>) in T by A4, Th20;

      hence contradiction by A2, Def3;

    end;

    theorem :: TREES_1:55

    for T be Tree, t be Element of T holds t in ( Leaves T) iff not ex n be Nat st (t ^ <*n*>) in T

    proof

      let T be Tree, t be Element of T;

      hereby

        assume

         A1: t in ( Leaves T);

        given n be Nat such that

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

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

        

         A3: not t is_a_proper_prefix_of (t ^ <*nn*>) by A1, A2, Def5;

        t is_a_prefix_of (t ^ <*n*>) by Th1;

        then

         A4: t = (t ^ <*n*>) by A3;

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

        hence contradiction by A4, FINSEQ_1: 33;

      end;

      assume that

       A5: not (ex n be Nat st (t ^ <*n*>) in T) and

       A6: not t in ( Leaves T);

      consider q be FinSequence of NAT such that

       A7: q in T and

       A8: t is_a_proper_prefix_of q by A6, Def5;

      t is_a_prefix_of q by A8;

      then

      consider r be FinSequence such that

       A9: q = (t ^ r) by Th1;

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

      ( len q) = (( len t) + ( len r)) by A9, FINSEQ_1: 22;

      then ( len r) <> 0 by A8, Th5;

      then r <> {} ;

      then

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

       A10: r = ( <*x*> ^ p) by FINSEQ_2: 130;

      q = ((t ^ <*x*>) ^ p) by A9, A10, FINSEQ_1: 32;

      hence contradiction by A5, A7, Th20;

    end;

    definition

      :: TREES_1:def14

      func TrivialInfiniteTree -> set equals the set of all (k |-> 0 ) where k be Nat;

      coherence ;

    end

    registration

      cluster TrivialInfiniteTree -> non empty Tree-like;

      coherence

      proof

        set X = TrivialInfiniteTree ;

        ( 0 |-> 0 ) in X;

        hence X is non empty;

        thus X c= ( NAT * )

        proof

          let x be object;

          assume x in X;

          then ex k be Nat st x = (k |-> 0 );

          hence thesis by FINSEQ_1:def 11;

        end;

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

        proof

          let p be FinSequence of NAT ;

          assume p in X;

          then

          consider m be Nat such that

           A1: p = (m |-> 0 );

          let x be object;

          assume

           A2: x in ( ProperPrefixes p);

          then

          reconsider x as FinSequence by Th10;

          

           A3: for k be Nat st 1 <= k & k <= ( len x) holds (x . k) = ((( len x) |-> 0 ) . k)

          proof

            x is_a_proper_prefix_of p by A2, Th11;

            then

             A4: x c= p;

            let k be Nat;

            assume 1 <= k & k <= ( len x);

            then

             A5: k in ( dom x) by FINSEQ_3: 25;

            

            thus ((( len x) |-> 0 ) . k) = 0

            .= (p . k) by A1

            .= (x . k) by A5, A4, GRFUNC_1: 2;

          end;

          ( len x) = ( len (( len x) |-> 0 )) by CARD_1:def 7;

          then x = (( len x) |-> 0 ) by A3, FINSEQ_1: 14;

          hence thesis;

        end;

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

        assume (p ^ <*m*>) in X;

        then

        consider k be Nat such that

         A6: (p ^ <*m*>) = (k |-> 0 );

        assume

         A7: n <= m;

        ( len (p ^ <*m*>)) = (( len p) + 1) by FINSEQ_2: 16;

        then ((p ^ <*m*>) . ( len (p ^ <*m*>))) = m by FINSEQ_1: 42;

        then

         A8: m = 0 by A6;

        

         A9: for z be Nat st 1 <= z & z <= ( len (p ^ <*n*>)) holds ((( len (p ^ <*n*>)) |-> 0 ) . z) = ((p ^ <*n*>) . z)

        proof

          let z be Nat;

          assume 1 <= z & z <= ( len (p ^ <*n*>));

          

          thus ((( len (p ^ <*n*>)) |-> 0 ) . z) = 0

          .= ((p ^ <*m*>) . z) by A6

          .= ((p ^ <*n*>) . z) by A7, A8;

        end;

        ( len (p ^ <*n*>)) = ( len (( len (p ^ <*n*>)) |-> 0 )) by CARD_1:def 7;

        then (( len (p ^ <*n*>)) |-> 0 ) = (p ^ <*n*>) by A9, FINSEQ_1: 14;

        hence thesis;

      end;

    end

    theorem :: TREES_1:56

    

     Th55: ( NAT , TrivialInfiniteTree ) are_equipotent

    proof

      defpred P[ Nat, set] means $2 = ($1 |-> 0 );

      

       A1: for x be Element of NAT holds ex y be Element of TrivialInfiniteTree st P[x, y]

      proof

        let x be Element of NAT ;

        (x |-> 0 ) in TrivialInfiniteTree ;

        then

        reconsider y = (x |-> 0 ) as Element of TrivialInfiniteTree ;

        take y;

        thus thesis;

      end;

      consider f be sequence of TrivialInfiniteTree such that

       A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      thus f is one-to-one

      proof

        let x,y be object;

        assume

         A3: x in ( dom f) & y in ( dom f);

        assume

         A4: (f . x) = (f . y);

        reconsider x, y as Element of NAT by A3, FUNCT_2:def 1;

         P[x, (f . x)] & P[y, (f . y)] by A2;

        hence thesis by A4, FINSEQ_2: 143;

      end;

      thus

       A5: ( dom f) = NAT by FUNCT_2:def 1;

      thus ( rng f) c= TrivialInfiniteTree by RELAT_1:def 19;

      let a be object;

      assume a in TrivialInfiniteTree ;

      then

      consider k be Nat such that

       A6: a = (k |-> 0 );

      

       A7: k in NAT by ORDINAL1:def 12;

      then (f . k) = a by A2, A6;

      hence thesis by A5, FUNCT_1:def 3, A7;

    end;

    registration

      cluster TrivialInfiniteTree -> infinite;

      coherence by Th55, CARD_1: 38;

    end