bintree2.miz



    begin

    

     Lm1: for D be set, p,q be FinSequence of D holds (p ^ q) is FinSequence of D;

    

     Lm2: for D be non empty set, x be Element of D holds <*x*> is FinSequence of D;

    theorem :: BINTREE2:1

    

     Th1: for D be set holds for p be FinSequence holds for n be Nat holds p in (D * ) implies (p | ( Seg n)) in (D * )

    proof

      let D be set;

      let p be FinSequence;

      let n be Nat;

      assume p in (D * );

      then p is FinSequence of D by FINSEQ_1:def 11;

      then (p | ( Seg n)) is FinSequence of D by FINSEQ_1: 18;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: BINTREE2:2

    

     Th2: for T be binary Tree holds for t be Element of T holds t is FinSequence of BOOLEAN

    proof

      let T be binary Tree;

      let t be Element of T;

      defpred P[ FinSequence] means $1 is Element of T implies ( rng $1) c= BOOLEAN ;

      

       A1: for p be FinSequence of NAT holds for x be Element of NAT st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of NAT ;

        let x be Element of NAT ;

        assume

         A2: P[p];

        assume

         A3: (p ^ <*x*>) is Element of T;

        then

        reconsider p1 = p as Element of T by TREES_1: 21;

        (p ^ <*x*>) in { (p ^ <*n*>) where n be Nat : (p ^ <*n*>) in T } by A3;

        then

         A4: (p ^ <*x*>) in ( succ p1) by TREES_2:def 5;

        then not p in ( Leaves T) by BINTREE1: 3;

        then ( succ p1) = {(p ^ <* 0 *>), (p ^ <*1*>)} by BINTREE1:def 2;

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

        then x = 0 or x = 1 by FINSEQ_2: 17;

        then

         A5: x in { 0 , 1} by TARSKI:def 2;

        

         A6: {x} c= BOOLEAN by A5, TARSKI:def 1;

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

        then (( rng p) \/ ( rng <*x*>)) c= BOOLEAN by A2, A3, A6, TREES_1: 21, XBOOLE_1: 8;

        hence thesis by FINSEQ_1: 31;

      end;

      

       A7: P[( <*> NAT )] by XBOOLE_1: 2;

      for p be FinSequence of NAT holds P[p] from FINSEQ_2:sch 2( A7, A1);

      then ( rng t) c= BOOLEAN ;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let T be binary Tree;

      :: original: Element

      redefine

      mode Element of T -> FinSequence of BOOLEAN ;

      coherence by Th2;

    end

    theorem :: BINTREE2:3

    

     Th3: for T be Tree st T = ( { 0 , 1} * ) holds T is binary

    proof

      let T be Tree;

      assume

       A1: T = ( { 0 , 1} * );

      now

        let t be Element of T;

        assume not t in ( Leaves T);

        { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } = {(t ^ <* 0 *>), (t ^ <*1*>)}

        proof

          thus { (t ^ <*n*>) where n be Nat : (t ^ <*n*>) in T } c= {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let x be object;

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

            then

            consider n be Nat such that

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

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

            reconsider tn = (t ^ <*n*>) as FinSequence of { 0 , 1} qua set by A1, A3, FINSEQ_1:def 11;

            (( len t) + 1) in ( Seg (( len t) + 1)) by FINSEQ_1: 4;

            then (( len t) + 1) in ( Seg ( len tn)) by FINSEQ_2: 16;

            then (( len t) + 1) in ( dom tn) by FINSEQ_1:def 3;

            

            then (tn /. (( len t) + 1)) = ((t ^ <*n*>) . (( len t) + 1)) by PARTFUN1:def 6

            .= n by FINSEQ_1: 42;

            then n = 0 or n = 1 by TARSKI:def 2;

            hence thesis by A2, TARSKI:def 2;

          end;

          let x be object;

          

           A4: t is FinSequence of { 0 , 1} by A1, FINSEQ_1:def 11;

          ( rng <*1*>) c= { 0 , 1}

          proof

            let z be object;

            assume z in ( rng <*1*>);

            then z in {1} by FINSEQ_1: 38;

            then z = 1 by TARSKI:def 1;

            hence thesis by TARSKI:def 2;

          end;

          then <*1*> is FinSequence of { 0 , 1} by FINSEQ_1:def 4;

          then (t ^ <*1*>) is FinSequence of { 0 , 1} by A4, Lm1;

          then

           A5: (t ^ <*1*>) in T by A1, FINSEQ_1:def 11;

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

          then

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

          ( rng <* 0 *>) c= { 0 , 1}

          proof

            let z be object;

            assume z in ( rng <* 0 *>);

            then z in { 0 } by FINSEQ_1: 38;

            then z = 0 by TARSKI:def 1;

            hence thesis by TARSKI:def 2;

          end;

          then <* 0 *> is FinSequence of { 0 , 1} by FINSEQ_1:def 4;

          then (t ^ <* 0 *>) is FinSequence of { 0 , 1} by A4, Lm1;

          then (t ^ <* 0 *>) in T by A1, FINSEQ_1:def 11;

          hence thesis by A5, A6;

        end;

        hence ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} by TREES_2:def 5;

      end;

      hence thesis by BINTREE1:def 2;

    end;

    theorem :: BINTREE2:4

    

     Th4: for T be Tree st T = ( { 0 , 1} * ) holds ( Leaves T) = {}

    proof

      

       A1: { 0 } c= BOOLEAN

      proof

        let z be object;

        assume z in { 0 };

        then z = FALSE by TARSKI:def 1;

        hence thesis;

      end;

      let T be Tree;

      assume

       A2: T = ( { 0 , 1} * );

      assume ( Leaves T) <> {} ;

      then

      consider x be object such that

       A3: x in ( Leaves T) by XBOOLE_0:def 1;

      reconsider x1 = x as Element of T by A3;

      T is binary by A2, Th3;

      then

       A4: x1 is FinSequence of BOOLEAN by Th2;

      then

      reconsider x1 = x as FinSequence of NAT ;

      set y1 = (x1 ^ <* 0 *>);

       0 in { 0 } by TARSKI:def 1;

      then <* 0 *> is FinSequence of BOOLEAN by A1, Lm2;

      then y1 is FinSequence of BOOLEAN by A4, Lm1;

      then

       A5: y1 in T by A2, FINSEQ_1:def 11;

      x1 is_a_proper_prefix_of y1 by TREES_1: 8;

      hence contradiction by A3, A5, TREES_1:def 5;

    end;

    theorem :: BINTREE2:5

    for T be binary Tree holds for n be Nat holds for t be Element of T st t in (T -level n) holds t is Element of (n -tuples_on BOOLEAN )

    proof

      let T be binary Tree;

      let n be Nat;

      let t be Element of T;

      assume t in (T -level n);

      then t in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

      then ex t2 be Element of T st t2 = t & ( len t2) = n;

      hence thesis by FINSEQ_2: 92;

    end;

    theorem :: BINTREE2:6

    for T be Tree st for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} holds ( Leaves T) = {}

    proof

      let T be Tree;

      assume

       A1: for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)};

      assume ( Leaves T) <> {} ;

      then

      consider x be object such that

       A2: x in ( Leaves T) by XBOOLE_0:def 1;

      reconsider t = x as Element of T by A2;

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

      hence contradiction by A2, BINTREE1: 3;

    end;

    theorem :: BINTREE2:7

    

     Th7: for T be Tree st for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)} holds T is binary

    proof

      let T be Tree;

      assume for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)};

      then for t be Element of T st not t in ( Leaves T) holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)};

      hence thesis by BINTREE1:def 2;

    end;

    theorem :: BINTREE2:8

    

     Th8: for T be Tree holds T = ( { 0 , 1} * ) iff for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)}

    proof

      let T be Tree;

      thus T = ( { 0 , 1} * ) implies for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)}

      proof

        assume

         A1: T = ( { 0 , 1} * );

        let t be Element of T;

        T is binary & not t in ( Leaves T) by A1, Th3, Th4;

        hence thesis by BINTREE1:def 2;

      end;

      assume

       A2: for t be Element of T holds ( succ t) = {(t ^ <* 0 *>), (t ^ <*1*>)};

      thus T = ( { 0 , 1} * )

      proof

        thus T c= ( { 0 , 1} * )

        proof

          let x be object;

          assume

           A3: x in T;

          T is binary by A2, Th7;

          then x is FinSequence of { 0 , 1} by A3, Th2;

          hence thesis by FINSEQ_1:def 11;

        end;

        defpred P[ FinSequence] means $1 in T;

        let x be object;

        assume x in ( { 0 , 1} * );

        then

         A4: x is FinSequence of { 0 , 1} by FINSEQ_1:def 11;

        

         A5: for p be FinSequence of { 0 , 1} holds for n be Element of { 0 , 1} st P[p] holds P[(p ^ <*n*>)]

        proof

          let p be FinSequence of { 0 , 1};

          let n be Element of { 0 , 1};

          

           A6: n = 0 or n = 1 by TARSKI:def 2;

          assume p in T;

          then

          reconsider p1 = p as Element of T;

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

          then (p ^ <*n*>) in ( succ p1) by A6, TARSKI:def 2;

          hence thesis;

        end;

        

         A7: P[( <*> { 0 , 1})] by TREES_1: 22;

        for p be FinSequence of { 0 , 1} holds P[p] from FINSEQ_2:sch 2( A7, A5);

        hence thesis by A4;

      end;

    end;

    scheme :: BINTREE2:sch1

    DecoratedBinTreeEx { A() -> non empty set , a() -> Element of A() , P[ object, object, object] } :

ex D be binary DecoratedTree of A() st ( dom D) = ( { 0 , 1} * ) & (D . {} ) = a() & for x be Node of D holds P[(D . x), (D . (x ^ <* 0 *>)), (D . (x ^ <*1*>))]

      provided

       A1: for a be Element of A() holds ex b,c be Element of A() st P[a, b, c];

      defpred Q[ object, object] means ex b,c be Element of A() st P[$1, b, c] & $2 = [b, c];

      

       A2: for e be object st e in A() holds ex u be object st u in [:A(), A():] & Q[e, u]

      proof

        let e be object;

        assume e in A();

        then

        consider b,c be Element of A() such that

         A3: P[e, b, c] by A1;

        take u = [b, c];

        thus u in [:A(), A():];

        thus thesis by A3;

      end;

      consider f be Function such that

       A4: ( dom f) = A() and

       A5: ( rng f) c= [:A(), A():] and

       A6: for e be object st e in A() holds Q[e, (f . e)] from FUNCT_1:sch 6( A2);

      deffunc F( object) = ( IFEQ (($1 `2 ), 0 ,((f . ($1 `1 )) `1 ),((f . ($1 `1 )) `2 )));

      

       A7: for x be object st x in [:A(), NAT :] holds F(x) in A()

      proof

        let x be object;

        assume x in [:A(), NAT :];

        then (x `1 ) in A() by MCART_1: 10;

        then

         A8: (f . (x `1 )) in ( rng f) by A4, FUNCT_1:def 3;

        then

         A9: ((f . (x `1 )) `2 ) in A() by A5, MCART_1: 10;

        

         A10: ((f . (x `1 )) `1 ) in A() by A5, A8, MCART_1: 10;

        now

          per cases ;

            suppose (x `2 ) = 0 ;

            hence thesis by A10, FUNCOP_1:def 8;

          end;

            suppose (x `2 ) <> 0 ;

            hence thesis by A9, FUNCOP_1:def 8;

          end;

        end;

        hence thesis;

      end;

      consider F be Function of [:A(), NAT :], A() such that

       A11: for x be object st x in [:A(), NAT :] holds (F . x) = F(x) from FUNCT_2:sch 2( A7);

      deffunc F( set) = 2;

      consider D be DecoratedTree of A() such that

       A12: (D . {} ) = a() and

       A13: for d be Element of ( dom D) holds ( succ d) = { (d ^ <*k*>) where k be Nat : k < F(.) } & for n be Nat st n < F(.) holds (D . (d ^ <*n*>)) = (F . ((D . d),n)) from TREES_2:sch 9;

      now

        let t be Element of ( dom D);

        assume not t in ( Leaves ( dom D));

        { (t ^ <*k*>) where k be Nat : k < 2 } = {(t ^ <* 0 *>), (t ^ <*1*>)}

        proof

          thus { (t ^ <*k*>) where k be Nat : k < 2 } c= {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let v be object;

            assume v in { (t ^ <*k*>) where k be Nat : k < 2 };

            then

            consider k be Nat such that

             A14: v = (t ^ <*k*>) and

             A15: k < 2;

            k = 0 or k = 1 by A15, NAT_1: 23;

            hence thesis by A14, TARSKI:def 2;

          end;

          let v be object;

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

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

          hence thesis;

        end;

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

      end;

      then ( dom D) is binary by BINTREE1:def 2;

      then

      reconsider D as binary DecoratedTree of A() by BINTREE1:def 3;

      take D;

      now

        let t be Element of ( dom D);

        { (t ^ <*k*>) where k be Nat : k < 2 } = {(t ^ <* 0 *>), (t ^ <*1*>)}

        proof

          thus { (t ^ <*k*>) where k be Nat : k < 2 } c= {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let v be object;

            assume v in { (t ^ <*k*>) where k be Nat : k < 2 };

            then

            consider k be Nat such that

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

             A17: k < 2;

            k = 0 or k = 1 by A17, NAT_1: 23;

            hence thesis by A16, TARSKI:def 2;

          end;

          let v be object;

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

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

          hence thesis;

        end;

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

      end;

      hence ( dom D) = ( { 0 , 1} * ) by Th8;

      thus (D . {} ) = a() by A12;

      let x be Node of D;

      for e be set st e in A() holds P[e, (F . (e, 0 )), (F . (e,1))]

      proof

        let e be set;

        assume

         A18: e in A();

        then

        consider b,c be Element of A() such that

         A19: P[e, b, c] and

         A20: (f . e) = [b, c] by A6;

         [e, 1] in [:A(), NAT :] by A18, ZFMISC_1: 87;

        

        then

         A21: (F . [e, 1]) = ( IFEQ (( [e, 1] `2 ), 0 ,((f . ( [e, 1] `1 )) `1 ),((f . ( [e, 1] `1 )) `2 ))) by A11

        .= ((f . ( [e, 1] `1 )) `2 ) by FUNCOP_1:def 8

        .= ((f . e) `2 )

        .= c by A20;

         [e, 0 ] in [:A(), NAT :] by A18, ZFMISC_1: 87;

        

        then (F . [e, 0 ]) = ( IFEQ (( [e, 0 ] `2 ), 0 ,((f . ( [e, 0 ] `1 )) `1 ),((f . ( [e, 0 ] `1 )) `2 ))) by A11

        .= ((f . ( [e, 0 ] `1 )) `1 ) by FUNCOP_1:def 8

        .= ((f . e) `1 )

        .= b by A20;

        hence thesis by A19, A21;

      end;

      then P[(D . x), (F . ((D . x), 0 )), (F . ((D . x),1))];

      then P[(D . x), (D . (x ^ <* 0 *>)), (F . ((D . x),1))] by A13;

      hence thesis by A13;

    end;

    scheme :: BINTREE2:sch2

    DecoratedBinTreeEx1 { A() -> non empty set , a() -> Element of A() , P,Q[ object, object] } :

ex D be binary DecoratedTree of A() st ( dom D) = ( { 0 , 1} * ) & (D . {} ) = a() & for x be Node of D holds P[(D . x), (D . (x ^ <* 0 *>))] & Q[(D . x), (D . (x ^ <*1*>))]

      provided

       A1: for a be Element of A() holds ex b be Element of A() st P[a, b]

       and

       A2: for a be Element of A() holds ex b be Element of A() st Q[a, b];

      deffunc F( set) = 2;

      defpred P1[ object, object] means (($1 `2 ) = 0 implies P[($1 `1 ), $2]) & (($1 `2 ) = 1 implies Q[($1 `1 ), $2]);

      

       A3: for e be object st e in [:A(), NAT :] holds ex u be object st u in A() & P1[e, u]

      proof

        let e be object;

        assume e in [:A(), NAT :];

        then

        reconsider e1 = (e `1 ) as Element of A() by MCART_1: 10;

        consider u1 be Element of A() such that

         A4: P[e1, u1] by A1;

        consider u2 be Element of A() such that

         A5: Q[e1, u2] by A2;

        take u = ( IFEQ ((e `2 ), 0 ,u1,u2));

        thus u in A();

        thus (e `2 ) = 0 implies P[(e `1 ), u] by A4, FUNCOP_1:def 8;

        thus thesis by A5, FUNCOP_1:def 8;

      end;

      consider F be Function such that

       A6: ( dom F) = [:A(), NAT :] & ( rng F) c= A() and

       A7: for e be object st e in [:A(), NAT :] holds P1[e, (F . e)] from FUNCT_1:sch 6( A3);

      reconsider F as Function of [:A(), NAT :], A() by A6, FUNCT_2: 2;

      consider D be DecoratedTree of A() such that

       A8: (D . {} ) = a() and

       A9: for d be Element of ( dom D) holds ( succ d) = { (d ^ <*k*>) where k be Nat : k < F(.) } & for n be Nat st n < F(.) holds (D . (d ^ <*n*>)) = (F . ((D . d),n)) from TREES_2:sch 9;

      now

        let t be Element of ( dom D);

        assume not t in ( Leaves ( dom D));

        { (t ^ <*k*>) where k be Nat : k < 2 } = {(t ^ <* 0 *>), (t ^ <*1*>)}

        proof

          thus { (t ^ <*k*>) where k be Nat : k < 2 } c= {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let v be object;

            assume v in { (t ^ <*k*>) where k be Nat : k < 2 };

            then

            consider k be Nat such that

             A10: v = (t ^ <*k*>) and

             A11: k < 2;

            k = 0 or k = 1 by A11, NAT_1: 23;

            hence thesis by A10, TARSKI:def 2;

          end;

          let v be object;

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

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

          hence thesis;

        end;

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

      end;

      then ( dom D) is binary by BINTREE1:def 2;

      then

      reconsider D as binary DecoratedTree of A() by BINTREE1:def 3;

      take D;

      now

        let t be Element of ( dom D);

        { (t ^ <*k*>) where k be Nat : k < 2 } = {(t ^ <* 0 *>), (t ^ <*1*>)}

        proof

          thus { (t ^ <*k*>) where k be Nat : k < 2 } c= {(t ^ <* 0 *>), (t ^ <*1*>)}

          proof

            let v be object;

            assume v in { (t ^ <*k*>) where k be Nat : k < 2 };

            then

            consider k be Nat such that

             A12: v = (t ^ <*k*>) and

             A13: k < 2;

            k = 0 or k = 1 by A13, NAT_1: 23;

            hence thesis by A12, TARSKI:def 2;

          end;

          let v be object;

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

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

          hence thesis;

        end;

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

      end;

      hence ( dom D) = ( { 0 , 1} * ) by Th8;

      thus (D . {} ) = a() by A8;

      let x be Node of D;

      ( [(D . x), 0 ] `2 ) = 0 ;

      then P[( [(D . x), 0 ] `1 ), (F . [(D . x), 0 ])] by A7;

      then P[(D . x), (F . ((D . x), 0 ))];

      hence P[(D . x), (D . (x ^ <* 0 *>))] by A9;

      ( [(D . x), 1] `2 ) = 1;

      then Q[( [(D . x), 1] `1 ), (F . [(D . x), 1])] by A7;

      then Q[(D . x), (F . ((D . x),1))];

      hence thesis by A9;

    end;

    

     Lm3: for D be non empty set holds for f be FinSequence of D holds ( Rev f) is FinSequence of D;

    definition

      let T be binary Tree;

      let n be non zero Nat;

      :: BINTREE2:def1

      func NumberOnLevel (n,T) -> Function of (T -level n), NAT means

      : Def1: for t be Element of T st t in (T -level n) holds for F be Element of (n -tuples_on BOOLEAN ) st F = ( Rev t) holds (it . t) = (( Absval F) + 1);

      existence

      proof

        defpred P[ object, object] means ex t be Element of T st t = $1 & for F be Tuple of n, BOOLEAN st F = ( Rev t) holds $2 = (( Absval F) + 1);

        

         A1: for e be object st e in (T -level n) holds ex u be object st u in NAT & P[e, u]

        proof

          let e be object;

          assume e in (T -level n);

          then e in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider t be Element of T such that

           A2: t = e and

           A3: ( len t) = n;

          ( len ( Rev t)) = n by A3, FINSEQ_5:def 3;

          then

          reconsider F1 = ( Rev t) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          take u = (( Absval F1) + 1);

          thus u in NAT ;

          take t;

          thus t = e by A2;

          let F be Tuple of n, BOOLEAN ;

          assume F = ( Rev t);

          hence thesis;

        end;

        consider f be Function such that

         A4: ( dom f) = (T -level n) & ( rng f) c= NAT and

         A5: for e be object st e in (T -level n) holds P[e, (f . e)] from FUNCT_1:sch 6( A1);

        reconsider f as Function of (T -level n), NAT by A4, FUNCT_2: 2;

        take f;

        let t be Element of T;

        assume t in (T -level n);

        then

         A6: ex t1 be Element of T st t1 = t & for F be Tuple of n, BOOLEAN st F = ( Rev t1) holds (f . t) = (( Absval F) + 1) by A5;

        let F be Element of (n -tuples_on BOOLEAN );

        assume F = ( Rev t);

        hence thesis by A6;

      end;

      uniqueness

      proof

        let f1,f2 be Function of (T -level n), NAT such that

         A7: for t be Element of T st t in (T -level n) holds for F be Element of (n -tuples_on BOOLEAN ) st F = ( Rev t) holds (f1 . t) = (( Absval F) + 1) and

         A8: for t be Element of T st t in (T -level n) holds for F be Element of (n -tuples_on BOOLEAN ) st F = ( Rev t) holds (f2 . t) = (( Absval F) + 1);

        now

          let x be object;

          assume

           A9: x in (T -level n);

          then x in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider t be Element of T such that

           A10: t = x and

           A11: ( len t) = n;

          ( len ( Rev t)) = n by A11, FINSEQ_5:def 3;

          then

          reconsider F = ( Rev t) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          

          thus (f1 . x) = (( Absval F) + 1) by A7, A9, A10

          .= (f2 . x) by A8, A9, A10;

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    registration

      let T be binary Tree;

      let n be non zero Nat;

      cluster ( NumberOnLevel (n,T)) -> one-to-one;

      coherence

      proof

        now

          let x1,x2 be object;

          assume that

           A1: x1 in ( dom ( NumberOnLevel (n,T))) and

           A2: x2 in ( dom ( NumberOnLevel (n,T))) and

           A3: (( NumberOnLevel (n,T)) . x1) = (( NumberOnLevel (n,T)) . x2);

          

           A4: x1 in (T -level n) by A1, FUNCT_2:def 1;

          then x1 in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider t1 be Element of T such that

           A5: t1 = x1 and

           A6: ( len t1) = n;

          

           A7: x2 in (T -level n) by A2, FUNCT_2:def 1;

          then x2 in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider t2 be Element of T such that

           A8: t2 = x2 and

           A9: ( len t2) = n;

          ( len ( Rev t2)) = n by A9, FINSEQ_5:def 3;

          then

          reconsider F2 = ( Rev t2) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          ( len ( Rev t1)) = n by A6, FINSEQ_5:def 3;

          then

          reconsider F1 = ( Rev t1) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          (( Absval F1) + 1) = (( NumberOnLevel (n,T)) . x1) by A4, A5, Def1

          .= (( Absval F2) + 1) by A3, A7, A8, Def1;

          hence x1 = x2 by A5, A8, BINARI_3: 2, BINARI_3: 3;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

    end

    begin

    definition

      let T be Tree;

      :: BINTREE2:def2

      attr T is full means

      : Def2: T = ( { 0 , 1} * );

    end

    theorem :: BINTREE2:9

    

     Th9: ( { 0 , 1} * ) is Tree

    proof

      set X = ( { 0 , 1} * );

       A1:

      now

        let p be FinSequence of NAT ;

        assume

         A2: p in X;

        thus ( ProperPrefixes p) c= X

        proof

          let y be object;

          assume y in ( ProperPrefixes p);

          then

          consider q be FinSequence such that

           A3: y = q and

           A4: q is_a_proper_prefix_of p by TREES_1:def 2;

          q is_a_prefix_of p by A4;

          then ex n be Nat st q = (p | ( Seg n)) by TREES_1:def 1;

          hence thesis by A2, A3, Th1;

        end;

      end;

       A5:

      now

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

        assume that

         A6: (p ^ <*k*>) in X and

         A7: n <= k;

        

         A8: (p ^ <*k*>) is FinSequence of { 0 , 1} by A6, FINSEQ_1:def 11;

        then

        reconsider kk = <*k*> as FinSequence of { 0 , 1} by FINSEQ_1: 36;

        1 in ( Seg 1) by FINSEQ_1: 3;

        then 1 in ( dom <*k*>) by FINSEQ_1: 38;

        then (kk . 1) in { 0 , 1} by FINSEQ_2: 11;

        then

         A9: k in { 0 , 1} by FINSEQ_1: 40;

        now

          per cases by A9, TARSKI:def 2;

            suppose k = 0 ;

            hence n = 0 or n = 1 by A7;

          end;

            suppose

             A10: k = 1;

            n = 1 or n = 0

            proof

              assume n <> 1;

              then n < ( 0 + 1) by A7, A10, XXREAL_0: 1;

              hence thesis by NAT_1: 13;

            end;

            hence n = 0 or n = 1;

          end;

        end;

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

        then

         A11: <*n*> is FinSequence of { 0 , 1} by Lm2;

        p is FinSequence of { 0 , 1} by A8, FINSEQ_1: 36;

        then (p ^ <*n*>) is FinSequence of { 0 , 1} by A11, Lm1;

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

      end;

      X c= ( NAT * ) by FINSEQ_1: 62;

      hence thesis by A1, A5, TREES_1:def 3;

    end;

    theorem :: BINTREE2:10

    

     Th10: for T be Tree st T = ( { 0 , 1} * ) holds for n be Nat holds ( 0* n) in (T -level n)

    proof

      let T be Tree;

      assume

       A1: T = ( { 0 , 1} * );

      let n be Nat;

      ( len ( 0* n)) = n & ( 0* n) in T by A1, BINARI_3: 4, CARD_1:def 7;

      then ( 0* n) in { w where w be Element of T : ( len w) = n };

      hence thesis by TREES_2:def 6;

    end;

    theorem :: BINTREE2:11

    

     Th11: for T be Tree st T = ( { 0 , 1} * ) holds for n be non zero Nat holds for y be Element of (n -tuples_on BOOLEAN ) holds y in (T -level n)

    proof

      let T be Tree;

      assume

       A1: T = ( { 0 , 1} * );

      let n be non zero Nat;

      let y be Element of (n -tuples_on BOOLEAN );

      y in { w where w be Element of T : ( len w) = n } by A1;

      hence thesis by TREES_2:def 6;

    end;

    registration

      let T be binary Tree;

      let n be Nat;

      cluster (T -level n) -> finite;

      coherence by TREES_9: 46;

    end

    registration

      cluster full -> binary for Tree;

      coherence by Th3;

    end

    registration

      cluster full for Tree;

      existence by Th9, Def2;

    end

    theorem :: BINTREE2:12

    

     Th12: for T be full Tree holds for n be non zero Nat holds ( Seg (2 to_power n)) c= ( rng ( NumberOnLevel (n,T)))

    proof

      let T be full Tree;

      let n be non zero Nat;

      let y be object;

      assume y in ( Seg (2 to_power n));

      then y in { k where k be Nat : 1 <= k & k <= (2 to_power n) } by FINSEQ_1:def 1;

      then

      consider k be Nat such that

       A1: k = y and

       A2: 1 <= k and

       A3: k <= (2 to_power n);

      

       A4: (k - 1) >= (1 - 1) by A2, XREAL_1: 9;

      set t = ( Rev (n -BinarySequence (k -' 1)));

      

       A5: ( len t) = ( len (n -BinarySequence (k -' 1))) by FINSEQ_5:def 3

      .= n by CARD_1:def 7;

      then ( len ( Rev t)) = n by FINSEQ_5:def 3;

      then

      reconsider F = ( Rev t) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

      T = ( { 0 , 1} * ) by Def2;

      then t in T by FINSEQ_1:def 11;

      then t in { w where w be Element of T : ( len w) = n } by A5;

      then

       A6: t in (T -level n) by TREES_2:def 6;

      then

       A7: t in ( dom ( NumberOnLevel (n,T))) by FUNCT_2:def 1;

      k < ((2 to_power n) + 1) by A3, NAT_1: 13;

      then (k - 1) < (2 to_power n) by XREAL_1: 19;

      then

       A8: (k -' 1) < (2 to_power n) by A4, XREAL_0:def 2;

      (( NumberOnLevel (n,T)) . t) = (( Absval F) + 1) by A6, Def1

      .= (( Absval (n -BinarySequence (k -' 1))) + 1)

      .= ((k -' 1) + 1) by A8, BINARI_3: 35

      .= ((k - 1) + 1) by A4, XREAL_0:def 2

      .= y by A1;

      hence thesis by A7, FUNCT_1:def 3;

    end;

    definition

      let T be full Tree;

      let n be non zero Nat;

      :: BINTREE2:def3

      func FinSeqLevel (n,T) -> FinSequence of (T -level n) equals (( NumberOnLevel (n,T)) " );

      coherence

      proof

        reconsider k = n as non zero Nat;

        T = ( { 0 , 1} * ) by Def2;

        then

         A1: (T -level n) is non empty by Th10;

        for y be object holds y in ( Seg (2 to_power n)) iff ex x be object st x in ( dom ( NumberOnLevel (k,T))) & y = (( NumberOnLevel (k,T)) . x)

        proof

          let y be object;

          thus y in ( Seg (2 to_power n)) implies ex x be object st x in ( dom ( NumberOnLevel (k,T))) & y = (( NumberOnLevel (k,T)) . x)

          proof

            assume

             A2: y in ( Seg (2 to_power n));

            take ((( NumberOnLevel (n,T)) " ) . y);

            ( Seg (2 to_power n)) c= ( rng ( NumberOnLevel (n,T))) by Th12;

            hence thesis by A2, FUNCT_1: 32;

          end;

          given x be object such that

           A3: x in ( dom ( NumberOnLevel (k,T))) and

           A4: y = (( NumberOnLevel (k,T)) . x);

          

           A5: x in (T -level n) by A3, FUNCT_2:def 1;

          then x in { t where t be Element of T : ( len t) = n } by TREES_2:def 6;

          then

          consider t be Element of T such that

           A6: t = x and

           A7: ( len t) = n;

          ( len ( Rev t)) = n by A7, FINSEQ_5:def 3;

          then

          reconsider F = ( Rev t) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          ( Absval F) < (2 to_power n) by BINARI_3: 1;

          then

           A8: 1 <= (( Absval F) + 1) & (( Absval F) + 1) <= (2 to_power n) by NAT_1: 11, NAT_1: 13;

          y = (( Absval F) + 1) by A4, A5, A6, Def1;

          hence thesis by A8, FINSEQ_1: 1;

        end;

        then ( rng ( NumberOnLevel (n,T))) = ( Seg (2 to_power n)) by FUNCT_1:def 3;

        then

         A9: ( dom (( NumberOnLevel (k,T)) " )) = ( Seg (2 to_power n)) by FUNCT_1: 33;

        ( rng (( NumberOnLevel (k,T)) " )) = ( dom ( NumberOnLevel (k,T))) by FUNCT_1: 33

        .= (T -level n) by FUNCT_2:def 1;

        then (( NumberOnLevel (n,T)) " ) is Function of ( Seg (2 to_power n)), (T -level n) by A9, FUNCT_2: 2;

        hence thesis by A1, FINSEQ_2: 25;

      end;

    end

    registration

      let T be full Tree;

      let n be non zero Nat;

      cluster ( FinSeqLevel (n,T)) -> one-to-one;

      coherence by FUNCT_1: 40;

    end

    theorem :: BINTREE2:13

    

     Th13: for T be full Tree holds for n be non zero Nat holds (( NumberOnLevel (n,T)) . ( 0* n)) = 1

    proof

      let T be full Tree;

      let n be non zero Nat;

      

       A1: ( len ( Rev ( 0* n))) = ( len ( 0* n)) by FINSEQ_5:def 3

      .= n by CARD_1:def 7;

      

       A2: T = ( { 0 , 1} * ) by Def2;

      then ( 0* n) is Element of T by BINARI_3: 4;

      then ( Rev ( 0* n)) is FinSequence of BOOLEAN by Lm3;

      then

      reconsider F = ( Rev ( 0* n)) as Element of (n -tuples_on BOOLEAN ) by A1, FINSEQ_2: 92;

      ( 0* n) in (T -level n) by A2, Th10;

      

      hence (( NumberOnLevel (n,T)) . ( 0* n)) = (( Absval F) + 1) by Def1

      .= ( 0 + 1) by BINARI_3: 6, BINARI_3: 8

      .= 1;

    end;

    theorem :: BINTREE2:14

    

     Th14: for T be full Tree holds for n be non zero Nat holds for y be Element of (n -tuples_on BOOLEAN ) st y = ( 0* n) holds (( NumberOnLevel (n,T)) . ( 'not' y)) = (2 to_power n)

    proof

      let T be full Tree;

      let n be non zero Nat;

      let y be Element of (n -tuples_on BOOLEAN );

      assume

       A1: y = ( 0* n);

      then

       A2: ( Rev ( 'not' y)) = ( 'not' y) by BINARI_3: 9;

      ( len ( Rev ( 'not' y))) = ( len ( 'not' y)) by FINSEQ_5:def 3

      .= n by CARD_1:def 7;

      then

      reconsider F = ( Rev ( 'not' y)) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

      reconsider ny = ( 'not' y) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

      T = ( { 0 , 1} * ) by Def2;

      then ny in (T -level n) by Th11;

      

      hence (( NumberOnLevel (n,T)) . ( 'not' y)) = (( Absval F) + 1) by Def1

      .= (((2 to_power n) - 1) + 1) by A1, A2, BINARI_3: 7

      .= (2 to_power n);

    end;

    theorem :: BINTREE2:15

    

     Th15: for T be full Tree holds for n be non zero Nat holds (( FinSeqLevel (n,T)) . 1) = ( 0* n)

    proof

      let T be full Tree;

      let n be non zero Nat;

      T = ( { 0 , 1} * ) by Def2;

      then ( 0* n) in (T -level n) by Th10;

      then

       A1: ( 0* n) in ( dom ( NumberOnLevel (n,T))) by FUNCT_2:def 1;

      1 = (( NumberOnLevel (n,T)) . ( 0* n)) by Th13;

      hence thesis by A1, FUNCT_1: 32;

    end;

    theorem :: BINTREE2:16

    

     Th16: for T be full Tree holds for n be non zero Nat holds for y be Element of (n -tuples_on BOOLEAN ) st y = ( 0* n) holds (( FinSeqLevel (n,T)) . (2 to_power n)) = ( 'not' y)

    proof

      let T be full Tree;

      let n be non zero Nat;

      let y be Element of (n -tuples_on BOOLEAN );

      reconsider ny = ( 'not' y) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

      T = ( { 0 , 1} * ) by Def2;

      then ny in (T -level n) by Th11;

      then

       A1: ( 'not' y) in ( dom ( NumberOnLevel (n,T))) by FUNCT_2:def 1;

      assume y = ( 0* n);

      then (2 to_power n) = (( NumberOnLevel (n,T)) . ( 'not' y)) by Th14;

      hence thesis by A1, FUNCT_1: 32;

    end;

    theorem :: BINTREE2:17

    

     Th17: for T be full Tree holds for n be non zero Nat holds for i be Nat st i in ( Seg (2 to_power n)) holds (( FinSeqLevel (n,T)) . i) = ( Rev (n -BinarySequence (i -' 1)))

    proof

      let T be full Tree;

      let n be non zero Nat;

      let i be Nat;

      reconsider nB = (n -BinarySequence (i -' 1)) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

      assume

       A1: i in ( Seg (2 to_power n));

      then

       A2: 1 <= i by FINSEQ_1: 1;

      i <= (2 to_power n) by A1, FINSEQ_1: 1;

      then i < ((2 to_power n) + 1) by NAT_1: 13;

      then (i - 1) < (2 to_power n) by XREAL_1: 19;

      then (i -' 1) < (2 to_power n) by A2, XREAL_1: 233;

      

      then

       A3: (( Absval nB) + 1) = ((i -' 1) + 1) by BINARI_3: 35

      .= ((i - 1) + 1) by A2, XREAL_1: 233

      .= i;

      

       A4: ( len ( Rev nB)) = ( len nB) by FINSEQ_5:def 3

      .= n by CARD_1:def 7;

      then

      reconsider RnB = ( Rev nB) as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 92;

      RnB in ( { 0 , 1} * ) by FINSEQ_1:def 11;

      then RnB is Element of T by Def2;

      then RnB in { t where t be Element of T : ( len t) = n } by A4;

      then

       A5: RnB in (T -level n) by TREES_2:def 6;

      nB = ( Rev RnB);

      then

       A6: (( NumberOnLevel (n,T)) . RnB) = (( Absval nB) + 1) by A5, Def1;

      RnB in ( dom ( NumberOnLevel (n,T))) by A5, FUNCT_2:def 1;

      hence thesis by A6, A3, FUNCT_1: 32;

    end;

    theorem :: BINTREE2:18

    

     Th18: for T be full Tree holds for n be Nat holds ( card (T -level n)) = (2 to_power n)

    proof

      let T be full Tree;

      defpred R[ Nat] means ( card (T -level $1)) = (2 to_power $1);

      

       A1: T = ( { 0 , 1} * ) by Def2;

      

       A2: for n be Nat st R[n] holds R[(n + 1)]

      proof

        defpred P[ set, set] means ex p be FinSequence st p = $1 & $2 = (p ^ <* 0 *>);

        let n be Nat;

        set Tn10 = { p where p be Element of T : ( len p) = (n + 1) & (p . (n + 1)) = 0 };

        set Tn11 = { p where p be Element of T : ( len p) = (n + 1) & (p . (n + 1)) = 1 };

        

         A3: (( 0* (n + 1)) . (n + 1)) = 0 by FINSEQ_1: 4, FUNCOP_1: 7;

        ( len ( 0* (n + 1))) = (n + 1) & ( 0* (n + 1)) in T by A1, BINARI_3: 4, CARD_1:def 7;

        then

         A4: ( 0* (n + 1)) in Tn10 by A3;

        

         A5: Tn11 c= (T -level (n + 1))

        proof

          let x be object;

          assume x in Tn11;

          then

          consider p be Element of T such that

           A6: p = x and

           A7: ( len p) = (n + 1) and (p . (n + 1)) = 1;

          p in { w where w be Element of T : ( len w) = (n + 1) } by A7;

          hence thesis by A6, TREES_2:def 6;

        end;

        ( rng <*1*>) c= { 0 , 1}

        proof

          let z be object;

          assume z in ( rng <*1*>);

          then z in {1} by FINSEQ_1: 38;

          then z = 1 by TARSKI:def 1;

          hence thesis by TARSKI:def 2;

        end;

        then

         A8: <*1*> is FinSequence of { 0 , 1} by FINSEQ_1:def 4;

        defpred P1[ set, set] means ex p be FinSequence st p = $1 & $2 = (p ^ <*1*>);

        

         A9: Tn10 c= (T -level (n + 1))

        proof

          let x be object;

          assume x in Tn10;

          then

          consider p be Element of T such that

           A10: p = x and

           A11: ( len p) = (n + 1) and (p . (n + 1)) = 0 ;

          p in { w where w be Element of T : ( len w) = (n + 1) } by A11;

          hence thesis by A10, TREES_2:def 6;

        end;

        ( 0* n) in ( { 0 , 1} * ) by BINARI_3: 4;

        then ( 0* n) is FinSequence of { 0 , 1} by FINSEQ_1:def 11;

        then (( 0* n) ^ <*1*>) is FinSequence of { 0 , 1} by A8, Lm1;

        then

         A12: (( 0* n) ^ <*1*>) in T by A1, FINSEQ_1:def 11;

        reconsider Tn = (T -level n) as finite non empty set by A1, Th10;

        assume

         A13: ( card (T -level n)) = (2 to_power n);

        ( len ( 0* n)) = n by CARD_1:def 7;

        then

         A14: ((( 0* n) ^ <*1*>) . (n + 1)) = 1 by FINSEQ_1: 42;

        ( len (( 0* n) ^ <*1*>)) = (( len ( 0* n)) + 1) by FINSEQ_2: 16

        .= (n + 1) by CARD_1:def 7;

        then (( 0* n) ^ <*1*>) in Tn11 by A12, A14;

        then

        reconsider Tn10, Tn11 as non empty finite set by A4, A9, A5;

        

         A15: (Tn10 \/ Tn11) c= (T -level (n + 1)) by A9, A5, XBOOLE_1: 8;

        

         A16: for x be Element of Tn holds ex y be Element of Tn11 st P1[x, y]

        proof

          let x be Element of Tn;

          x in (T -level n);

          then x in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider p be Element of T such that

           A17: p = x and

           A18: ( len p) = n;

          set y = (p ^ <*1*>);

          (p ^ <*1*>) is FinSequence of { 0 , 1} by A8, Lm1;

          then

           A19: y in T by A1, FINSEQ_1:def 11;

          ( len y) = (n + 1) & (y . (n + 1)) = 1 by A18, FINSEQ_1: 42, FINSEQ_2: 16;

          then y in { t where t be Element of T : ( len t) = (n + 1) & (t . (n + 1)) = 1 } by A19;

          then

          reconsider y as Element of Tn11;

          take y, p;

          thus thesis by A17;

        end;

        consider f1 be Function of Tn, Tn11 such that

         A20: for x be Element of Tn holds P1[x, (f1 . x)] from FUNCT_2:sch 3( A16);

        now

          let y be object;

          assume y in Tn11;

          then

          consider t be Element of T such that

           A21: t = y and

           A22: ( len t) = (n + 1) and

           A23: (t . (n + 1)) = 1;

          consider p be FinSequence of BOOLEAN , d be Element of BOOLEAN such that

           A24: t = (p ^ <*d*>) by A22, FINSEQ_2: 19;

          reconsider x = p as object;

          take x;

          

           A25: (( len p) + 1) = (n + 1) by A22, A24, FINSEQ_2: 16;

          p in T by A1, FINSEQ_1:def 11;

          then

           A26: p in { w where w be Element of T : ( len w) = n } by A25;

          hence x in Tn by TREES_2:def 6;

          reconsider x9 = x as Element of Tn by A26, TREES_2:def 6;

          ex q be FinSequence st q = x9 & (f1 . x9) = (q ^ <*1*>) by A20;

          hence y = (f1 . x) by A21, A23, A24, A25, FINSEQ_1: 42;

        end;

        then

         A27: ( rng f1) = Tn11 by FUNCT_2: 10;

        

         A28: for x be Element of Tn holds ex y be Element of Tn10 st P[x, y]

        proof

          let x be Element of Tn;

          x in (T -level n);

          then x in { w where w be Element of T : ( len w) = n } by TREES_2:def 6;

          then

          consider p be Element of T such that

           A29: p = x and

           A30: ( len p) = n;

          set y = (p ^ <* 0 *>);

          ( rng <* 0 *>) c= { 0 , 1}

          proof

            let z be object;

            assume z in ( rng <* 0 *>);

            then z in { 0 } by FINSEQ_1: 38;

            then z = 0 by TARSKI:def 1;

            hence thesis by TARSKI:def 2;

          end;

          then <* 0 *> is FinSequence of { 0 , 1} by FINSEQ_1:def 4;

          then (p ^ <* 0 *>) is FinSequence of { 0 , 1} by Lm1;

          then

           A31: y in T by A1, FINSEQ_1:def 11;

          ( len y) = (n + 1) & (y . (n + 1)) = 0 by A30, FINSEQ_1: 42, FINSEQ_2: 16;

          then y in { t where t be Element of T : ( len t) = (n + 1) & (t . (n + 1)) = 0 } by A31;

          then

          reconsider y as Element of Tn10;

          take y, p;

          thus thesis by A29;

        end;

        consider f0 be Function of Tn, Tn10 such that

         A32: for x be Element of Tn holds P[x, (f0 . x)] from FUNCT_2:sch 3( A28);

        now

          let x1,x2 be object;

          assume that

           A33: x1 in ( dom f1) & x2 in ( dom f1) and

           A34: (f1 . x1) = (f1 . x2);

          reconsider x19 = x1, x29 = x2 as Element of Tn by A33, FUNCT_2:def 1;

          (ex p1 be FinSequence st p1 = x19 & (f1 . x19) = (p1 ^ <*1*>)) & ex p2 be FinSequence st p2 = x29 & (f1 . x29) = (p2 ^ <*1*>) by A20;

          hence x1 = x2 by A34, FINSEQ_2: 17;

        end;

        then Tn c= ( dom f1) & f1 is one-to-one by FUNCT_1:def 4, FUNCT_2:def 1;

        then (Tn,(f1 .: Tn)) are_equipotent by CARD_1: 33;

        then

         A35: (Tn,( rng f1)) are_equipotent by RELSET_1: 22;

        

         A36: (T -level (n + 1)) c= (Tn10 \/ Tn11)

        proof

          let x be object;

          assume x in (T -level (n + 1));

          then x in { w where w be Element of T : ( len w) = (n + 1) } by TREES_2:def 6;

          then

          consider p be Element of T such that

           A37: p = x and

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

          x in Tn10 or x in Tn11

          proof

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

            then (n + 1) in ( dom p) by A38, FINSEQ_1:def 3;

            then (p . (n + 1)) in BOOLEAN by FINSEQ_2: 11;

            then

             A39: (p . (n + 1)) = 0 or (p . (n + 1)) = 1 by TARSKI:def 2;

            assume not x in Tn10;

            hence thesis by A37, A38, A39;

          end;

          hence thesis by XBOOLE_0:def 3;

        end;

        now

          let y be object;

          assume y in Tn10;

          then

          consider t be Element of T such that

           A40: t = y and

           A41: ( len t) = (n + 1) and

           A42: (t . (n + 1)) = 0 ;

          consider p be FinSequence of BOOLEAN , d be Element of BOOLEAN such that

           A43: t = (p ^ <*d*>) by A41, FINSEQ_2: 19;

          reconsider x = p as object;

          take x;

          

           A44: (( len p) + 1) = (n + 1) by A41, A43, FINSEQ_2: 16;

          p in T by A1, FINSEQ_1:def 11;

          then

           A45: p in { w where w be Element of T : ( len w) = n } by A44;

          hence x in Tn by TREES_2:def 6;

          reconsider x9 = x as Element of Tn by A45, TREES_2:def 6;

          ex q be FinSequence st q = x9 & (f0 . x9) = (q ^ <* 0 *>) by A32;

          hence y = (f0 . x) by A40, A42, A43, A44, FINSEQ_1: 42;

        end;

        then

         A46: ( rng f0) = Tn10 by FUNCT_2: 10;

        now

          let x1,x2 be object;

          assume that

           A47: x1 in ( dom f0) & x2 in ( dom f0) and

           A48: (f0 . x1) = (f0 . x2);

          reconsider x19 = x1, x29 = x2 as Element of Tn by A47, FUNCT_2:def 1;

          (ex p1 be FinSequence st p1 = x19 & (f0 . x19) = (p1 ^ <* 0 *>)) & ex p2 be FinSequence st p2 = x29 & (f0 . x29) = (p2 ^ <* 0 *>) by A32;

          hence x1 = x2 by A48, FINSEQ_2: 17;

        end;

        then Tn c= ( dom f0) & f0 is one-to-one by FUNCT_1:def 4, FUNCT_2:def 1;

        then (Tn,(f0 .: Tn)) are_equipotent by CARD_1: 33;

        then (Tn,( rng f0)) are_equipotent by RELSET_1: 22;

        then

         A49: ( card Tn) = ( card Tn10) by A46, CARD_1: 5;

        

         A50: Tn10 misses Tn11

        proof

          assume (Tn10 /\ Tn11) <> {} ;

          then

          consider x be object such that

           A51: x in (Tn10 /\ Tn11) by XBOOLE_0:def 1;

          x in Tn11 by A51, XBOOLE_0:def 4;

          then

           A52: ex p2 be Element of T st p2 = x & ( len p2) = (n + 1) & (p2 . (n + 1)) = 1;

          x in Tn10 by A51, XBOOLE_0:def 4;

          then ex p1 be Element of T st p1 = x & ( len p1) = (n + 1) & (p1 . (n + 1)) = 0 ;

          hence contradiction by A52;

        end;

        

        thus (2 to_power (n + 1)) = ((2 to_power n) * (2 to_power 1)) by POWER: 27

        .= (2 * (2 to_power n)) by POWER: 25

        .= (( card Tn) + ( card Tn)) by A13

        .= (( card Tn10) + ( card Tn11)) by A49, A35, A27, CARD_1: 5

        .= ( card (Tn10 \/ Tn11)) by A50, CARD_2: 40

        .= ( card (T -level (n + 1))) by A15, A36, XBOOLE_0:def 10;

      end;

      ( card (T -level 0 )) = ( card { {} }) by TREES_9: 44

      .= 1 by CARD_1: 30

      .= (2 to_power 0 ) by POWER: 24;

      then

       A53: R[ 0 ];

      thus for n be Nat holds R[n] from NAT_1:sch 2( A53, A2);

    end;

    theorem :: BINTREE2:19

    

     Th19: for T be full Tree holds for n be non zero Nat holds ( len ( FinSeqLevel (n,T))) = (2 to_power n)

    proof

      let T be full Tree;

      let n be non zero Nat;

      ( rng ( FinSeqLevel (n,T))) = ( dom ( NumberOnLevel (n,T))) by FUNCT_1: 33

      .= (T -level n) by FUNCT_2:def 1;

      then

       A1: (( dom ( FinSeqLevel (n,T))),(T -level n)) are_equipotent by WELLORD2:def 4;

      ( card ( Seg ( len ( FinSeqLevel (n,T))))) = ( card ( dom ( FinSeqLevel (n,T)))) by FINSEQ_1:def 3

      .= ( card (T -level n)) by A1, CARD_1: 5

      .= (2 to_power n) by Th18;

      hence thesis by FINSEQ_1: 57;

    end;

    theorem :: BINTREE2:20

    

     Th20: for T be full Tree holds for n be non zero Nat holds ( dom ( FinSeqLevel (n,T))) = ( Seg (2 to_power n))

    proof

      let T be full Tree;

      let n be non zero Nat;

      

      thus ( dom ( FinSeqLevel (n,T))) = ( Seg ( len ( FinSeqLevel (n,T)))) by FINSEQ_1:def 3

      .= ( Seg (2 to_power n)) by Th19;

    end;

    theorem :: BINTREE2:21

    for T be full Tree holds for n be non zero Nat holds ( rng ( FinSeqLevel (n,T))) = (T -level n)

    proof

      let T be full Tree;

      let n be non zero Nat;

      reconsider Tln = (T -level n) as finite set;

      T = ( { 0 , 1} * ) by Def2;

      then (T -level n) is non empty by Th10;

      then

      reconsider p = ( FinSeqLevel (n,T)) as Function of ( dom ( FinSeqLevel (n,T))), (T -level n) by FINSEQ_2: 26;

      reconsider dp = ( dom p) as finite set;

      ( card dp) = ( card ( Seg (2 to_power n))) by Th20

      .= (2 to_power n) by FINSEQ_1: 57

      .= ( card Tln) by Th18;

      then p is onto by FINSEQ_4: 63;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: BINTREE2:22

    for T be full Tree holds (( FinSeqLevel (1,T)) . 1) = <* 0 *>

    proof

      let T be full Tree;

      

      thus (( FinSeqLevel (1,T)) . 1) = ( 0* 1) by Th15

      .= <* 0 *> by FINSEQ_2: 59;

    end;

    theorem :: BINTREE2:23

    for T be full Tree holds (( FinSeqLevel (1,T)) . 2) = <*1*>

    proof

      let T be full Tree;

      

       A1: ( 0* 1) = <* FALSE *> by FINSEQ_2: 59;

      reconsider t = <* FALSE *> as Element of (1 -tuples_on BOOLEAN ) by FINSEQ_2: 131;

      

      thus (( FinSeqLevel (1,T)) . 2) = (( FinSeqLevel (1,T)) . (2 to_power 1)) by POWER: 25

      .= ( 'not' t) by A1, Th16

      .= <*1*> by BINARI_3: 14;

    end;

    theorem :: BINTREE2:24

    for T be full Tree holds for n,i be non zero Nat st i <= (2 to_power (n + 1)) holds for F be Element of (n -tuples_on BOOLEAN ) st F = (( FinSeqLevel (n,T)) . ((i + 1) div 2)) holds (( FinSeqLevel ((n + 1),T)) . i) = (F ^ <*((i + 1) mod 2)*>)

    proof

      let T be full Tree;

      let n,i be non zero Nat;

      assume

       A1: i <= (2 to_power (n + 1));

       A2:

      now

        per cases ;

          suppose (i -' 1) is odd;

          then

           A3: ((i -' 1) mod 2) = 1 by NAT_2: 22;

          then (((i -' 1) + ((1 + 1) * 1)) mod 2) = 1 by NAT_D: 21;

          then ((((i -' 1) + 1) + 1) mod 2) = 1;

          hence ((i + 1) mod 2) = ((i -' 1) mod 2) by A3, NAT_1: 14, XREAL_1: 235;

        end;

          suppose (i -' 1) is even;

          then

           A4: ((i -' 1) mod 2) = 0 by NAT_2: 21;

          then (((i -' 1) + ((1 + 1) * 1)) mod 2) = 0 by NAT_D: 21;

          then ((((i -' 1) + 1) + 1) mod 2) = 0 ;

          hence ((i + 1) mod 2) = ((i -' 1) mod 2) by A4, NAT_1: 14, XREAL_1: 235;

        end;

      end;

      let F be Element of (n -tuples_on BOOLEAN );

      assume

       A5: F = (( FinSeqLevel (n,T)) . ((i + 1) div 2));

      

       A6: 1 <= i by NAT_1: 14;

      then (1 + 1) <= (i + 1) by XREAL_1: 6;

      then

       A7: 1 <= ((i + 1) div 2) by NAT_2: 13;

      (2 to_power (n + 1)) = ((2 to_power n) * (2 to_power 1)) by POWER: 27

      .= (2 * (2 to_power n)) by POWER: 25;

      then ((i + 1) div 2) <= (2 to_power n) by A1, NAT_2: 25;

      then

       A8: ((i + 1) div 2) in ( Seg (2 to_power n)) by A7, FINSEQ_1: 1;

      (i + 1) >= (1 + 1) by A6, XREAL_1: 6;

      then

       A9: 1 <= ((i + 1) div 2) by NAT_2: 13;

      

       A10: ((i -' 1) div 2) = ((((i -' 1) div 2) + 1) - 1)

      .= ((((i -' 1) + (1 + 1)) div 2) - 1) by NAT_2: 14

      .= (((((i -' 1) + 1) + 1) div 2) - 1)

      .= (((i + 1) div 2) - 1) by NAT_1: 14, XREAL_1: 235

      .= (((i + 1) div 2) -' 1) by A9, XREAL_1: 233;

      i in ( Seg (2 to_power (n + 1))) by A1, A6, FINSEQ_1: 1;

      

      hence (( FinSeqLevel ((n + 1),T)) . i) = ( Rev ((n + 1) -BinarySequence (i -' 1))) by Th17

      .= ( Rev ( <*((i -' 1) mod 2)*> ^ (n -BinarySequence ((i -' 1) div 2)))) by BINARI_3: 34

      .= (( Rev (n -BinarySequence (((i + 1) div 2) -' 1))) ^ <*((i + 1) mod 2)*>) by A2, A10, FINSEQ_6: 24

      .= (F ^ <*((i + 1) mod 2)*>) by A5, A8, Th17;

    end;