:: BINTREE2 semantic presentation

theorem E1: :: BINTREE2:1
for b1 being set
for b2 being FinSequence
for b3 being Nat holds
( b2 in b1 * implies b2 | (Seg b3) in b1 * )
proof
let c1 be set ;
let c2 be FinSequence;
let c3 be Nat;
assume c2 in c1 * ;
then c2 is FinSequence of c1 by FINSEQ_1:def 11;
then c2 | (Seg c3) is FinSequence of c1 by FINSEQ_1:23;
hence c2 | (Seg c3) in c1 * by FINSEQ_1:def 11;
end;

theorem E2: :: BINTREE2:2
for b1 being binary Tree
for b2 being Element of b1 holds
b2 is FinSequence of BOOLEAN
proof
let c1 be binary Tree;
let c2 be Element of c1;
defpred S1[ FinSequence] means ( a1 is Element of c1 implies rng a1 c= BOOLEAN );
rng (<*> NAT ) = {} by FINSEQ_1:27;
then E3: S1[ <*> NAT ] by XBOOLE_1:2;
E4: for b1 being FinSequence of NAT
for b2 being Element of NAT holds
( S1[b1] implies S1[b1 ^ <*b2*>] )
proof
let c3 be FinSequence of NAT ;
let c4 be Element of NAT ;
assume E5: S1[c3] ;
assume E6: c3 ^ <*c4*> is Element of c1 ;
then reconsider c5 = c3 as Element of c1 by TREES_1:46;
c3 ^ <*c4*> in { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in c1 } by E6;
then E7: c3 ^ <*c4*> in succ c5 by TREES_2:def 5;
then not c3 in Leaves c1 by BINTREE1:5;
then succ c5 = {(c3 ^ <*0*>),(c3 ^ <*1*>)} by BINTREE1:def 2;
then ( c3 ^ <*c4*> = c3 ^ <*0*> or c3 ^ <*c4*> = c3 ^ <*1*> ) by E7, TARSKI:def 2;
then ( c4 = 0 or c4 = 1 ) by FINSEQ_2:20;
then E8: c4 in {0,1} by TARSKI:def 2;
E9: {c4} c= BOOLEAN
proof
let c6 be set ; :: uses TARSKI:def 3
assume c6 in {c4} ;
hence c6 in BOOLEAN by E8, MARGREL1:def 12, TARSKI:def 1;
end;
rng <*c4*> = {c4} by FINSEQ_1:55;
then (rng c3) \/ (rng <*c4*>) c= BOOLEAN by E5, E6, E9, TREES_1:46, XBOOLE_1:8;
hence rng (c3 ^ <*c4*>) c= BOOLEAN by FINSEQ_1:44;
end;
for b1 being FinSequence of NAT holds
S1[b1] from FINSEQ_2:sch 2(E3, E4);
 then rng c2 c= BOOLEAN ;
hence c2 is FinSequence of BOOLEAN by FINSEQ_1:def 4;
end;

definition
let c1 be binary Tree;
redefine mode Element as Element of a1 -> FinSequence of BOOLEAN ;
coherence
for b1 being Element of c1 holds
b1 is FinSequence of BOOLEAN by E2;
end;

theorem E3: :: BINTREE2:3
for b1 being Tree holds
( b1 = {0,1} * implies b1 is binary )
proof
let c1 be Tree;
assume E4: c1 = {0,1} * ;
now
let c2 be Element of c1;
assume not c2 in Leaves c1 ;
{ (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } = {(c2 ^ <*0*>),(c2 ^ <*1*>)}
proof
thus { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } c= {(c2 ^ <*0*>),(c2 ^ <*1*>)} :: uses XBOOLE_0:def 10
proof
let c3 be set ; :: uses TARSKI:def 3
assume c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } ;
then consider c4 being Nat such that
E5: c3 = c2 ^ <*c4*>
and E6: c2 ^ <*c4*> in c1 ;
reconsider c5 = c2 ^ <*c4*> as FinSequence of {0,1} by E4, E6, FINSEQ_1:def 11;
(len c2) + 1 in Seg ((len c2) + 1) by FINSEQ_1:6;
then (len c2) + 1 in Seg (len c5) by FINSEQ_2:19;
then (len c2) + 1 in dom c5 by FINSEQ_1:def 3;
then c5 /. ((len c2) + 1) = (c2 ^ <*c4*>) . ((len c2) + 1) by FINSEQ_4:def 4
.= c4 by FINSEQ_1:59 ;
then ( c4 = 0 or c4 = 1 ) by TARSKI:def 2;
hence c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E5, TARSKI:def 2;
end;
let c3 be set ; :: uses TARSKI:def 3
E5: c2 is FinSequence of {0,1} by E4, FINSEQ_1:def 11;
rng <*0*> c= {0,1}
proof
let c4 be set ; :: uses TARSKI:def 3
assume c4 in rng <*0*> ;
then c4 in {0} by FINSEQ_1:55;
then c4 = 0 by TARSKI:def 1;
hence c4 in {0,1} by TARSKI:def 2;
end;
then E6: <*0*> is FinSequence of {0,1} by FINSEQ_1:def 4;
rng <*1*> c= {0,1}
proof
let c4 be set ; :: uses TARSKI:def 3
assume c4 in rng <*1*> ;
then c4 in {1} by FINSEQ_1:55;
then c4 = 1 by TARSKI:def 1;
hence c4 in {0,1} by TARSKI:def 2;
end;
then E7: <*1*> is FinSequence of {0,1} by FINSEQ_1:def 4;
c2 ^ <*0*> is FinSequence of {0,1} by E5, E6, SCMFSA_7:23;
then E8: c2 ^ <*0*> in c1 by E4, FINSEQ_1:def 11;
c2 ^ <*1*> is FinSequence of {0,1} by E5, E7, SCMFSA_7:23;
then E9: c2 ^ <*1*> in c1 by E4, FINSEQ_1:def 11;
assume c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} ;
then ( c3 = c2 ^ <*0*> or c3 = c2 ^ <*1*> ) by TARSKI:def 2;
hence c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } by E8, E9;
end;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by TREES_2:def 5;
end;
hence c1 is binary by BINTREE1:def 2;
end;

theorem E4: :: BINTREE2:4
for b1 being Tree holds
( b1 = {0,1} * implies Leaves b1 = {} )
proof
let c1 be Tree;
assume E5: c1 = {0,1} * ;
assume Leaves c1 <> {} ;
then consider c2 being set such that
E6: c2 in Leaves c1 by XBOOLE_0:def 1;
reconsider c3 = c2 as Element of c1 by E6;
c1 is binary by E5, E3;
then E7: c3 is FinSequence of BOOLEAN by E2;
then reconsider c4 = c2 as FinSequence of NAT ;
set c5 = c4 ^ <*0*>;
E8: 0 in {0} by TARSKI:def 1;
{0} c= BOOLEAN
proof
let c6 be set ; :: uses TARSKI:def 3
assume c6 in {0} ;
then c6 = 0 by TARSKI:def 1;
hence c6 in BOOLEAN by MARGREL1:def 13;
end;
then <*0*> is FinSequence of BOOLEAN by E8, SCMFSA_7:22;
then c4 ^ <*0*> is FinSequence of BOOLEAN by E7, SCMFSA_7:23;
then E9: c4 ^ <*0*> in c1 by E5, FINSEQ_1:def 11, MARGREL1:def 12;
c4 is_a_proper_prefix_of c4 ^ <*0*> by TREES_1:31;
hence not verum by E6, E9, TREES_1:def 8;
end;

theorem :: BINTREE2:5
for b1 being binary Tree
for b2 being Nat
for b3 being Element of b1 holds
( b3 in b1 -level b2 implies b3 is Tuple of b2,BOOLEAN )
proof
let c1 be binary Tree;
let c2 be Nat;
let c3 be Element of c1;
assume c3 in c1 -level c2 ;
then c3 in { b1 where B is Element of c1 : len b1 = c2 } by TREES_2:def 6;
then ex b1 being Element of c1 st
( b1 = c3 & len b1 = c2 ) ;
hence c3 is Tuple of c2,BOOLEAN by FINSEQ_2:110;
end;

theorem :: BINTREE2:6
for b1 being Tree holds
( for b2 being Element of b1 holds succ b2 = {(b2 ^ <*0*>),(b2 ^ <*1*>)} implies Leaves b1 = {} )
proof
let c1 be Tree;
assume E5: for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ;
assume Leaves c1 <> {} ;
then consider c2 being set such that
E6: c2 in Leaves c1 by XBOOLE_0:def 1;
reconsider c3 = c2 as Element of c1 by E6;
succ c3 = {(c3 ^ <*0*>),(c3 ^ <*1*>)} by E5;
hence not verum by E6, BINTREE1:5;
end;

theorem E5: :: BINTREE2:7
for b1 being Tree holds
( for b2 being Element of b1 holds succ b2 = {(b2 ^ <*0*>),(b2 ^ <*1*>)} implies b1 is binary )
proof
let c1 be Tree;
assume for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ;
then for b1 being Element of c1 holds
( not b1 in Leaves c1 implies succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ) ;
hence c1 is binary by BINTREE1:def 2;
end;

theorem E6: :: BINTREE2:8
for b1 being Tree holds
( b1 = {0,1} * iff for b2 being Element of b1 holds succ b2 = {(b2 ^ <*0*>),(b2 ^ <*1*>)} )
proof
let c1 be Tree;
thus ( c1 = {0,1} * implies for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} )
proof
assume E7: c1 = {0,1} * ;
then E8: c1 is binary by E3;
let c2 be Element of c1;
not c2 in Leaves c1 by E7, E4;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E8, BINTREE1:def 2;
end;
assume E7: for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ;
thus c1 = {0,1} *
proof
thus c1 c= {0,1} * :: uses XBOOLE_0:def 10
proof
let c2 be set ; :: uses TARSKI:def 3
E8: c1 is binary by E7, E5;
assume c2 in c1 ;
then c2 is FinSequence of {0,1} by E8, E2, MARGREL1:def 12;
hence c2 in {0,1} * by FINSEQ_1:def 11;
end;
let c2 be set ; :: uses TARSKI:def 3
assume c2 in {0,1} * ;
then E8: c2 is FinSequence of {0,1} by FINSEQ_1:def 11;
defpred S1[ FinSequence] means a1 in c1;
E9: S1[ <*> {0,1}] by TREES_1:47;
E10: for b1 being FinSequence of {0,1}
for b2 being Element of {0,1} holds
( S1[b1] implies S1[b1 ^ <*b2*>] )
proof
let c3 be FinSequence of {0,1};
let c4 be Element of {0,1};
assume c3 in c1 ;
then reconsider c5 = c3 as Element of c1 ;
E11: succ c5 = {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E7;
( c4 = 0 or c4 = 1 ) by TARSKI:def 2;
then c3 ^ <*c4*> in succ c5 by E11, TARSKI:def 2;
hence c3 ^ <*c4*> in c1 ;
end;
for b1 being FinSequence of {0,1} holds
S1[b1] from FINSEQ_2:sch 2(E9, E10);
 hence c2 in c1 by E8;
end;
end;

scheme :: BINTREE2:sch 1
s1{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } :
ex b1 being binary DecoratedTree of F1() st
( dom b1 = {0,1} * & b1 . {} = F2() & for b2 being Node of b1 holds P1[b1 . b2,b1 . (b2 ^ <*0*>),b1 . (b2 ^ <*1*>)] )
provided
E7: for b1 being Element of F1() holds
ex b2, b3 being Element of F1() st P1[b1,b2,b3]
proof
defpred S1[ set , set ] means ex b1, b2 being Element of F1() st
( P1[a1,b1,b2] & a2 = [b1,b2] );
E8: for b1 being set holds
not ( b1 in F1() & for b2 being set holds
not ( b2 in [:F1(),F1():] & S1[b1,b2] ) )
proof
let c1 be set ;
assume c1 in F1() ;
then consider c2, c3 being Element of F1() such that
E9: P1[c1,c2,c3] by E7;
take c4 = [c2,c3];
thus c4 in [:F1(),F1():] ;
thus S1[c1,c4] by E9;
end;
consider c1 being Function such that
E9: dom c1 = F1()
and E10: rng c1 c= [:F1(),F1():]
and E11: for b1 being set holds
( b1 in F1() implies S1[b1,c1 . b1] ) from WELLORD2:sch 1(E8);
 deffunc H1( set ) -> set = IFEQ (a1 `2 ),0,((c1 . (a1 `1 )) `1 ),((c1 . (a1 `1 )) `2 );
E12: for b1 being set holds
( b1 in [:F1(),NAT :] implies H1(b1) in F1() )
proof
let c2 be set ;
assume c2 in [:F1(),NAT :] ;
then c2 `1 in F1() by MCART_1:10;
then c1 . (c2 `1 ) in rng c1 by E9, FUNCT_1:def 5;
then E13: ( (c1 . (c2 `1 )) `1 in F1() & (c1 . (c2 `1 )) `2 in F1() ) by E10, MCART_1:10;
now
per cases not ( not c2 `2 = 0 & not c2 `2 <> 0 ) ;
suppose c2 `2 = 0 ;
hence IFEQ (c2 `2 ),0,((c1 . (c2 `1 )) `1 ),((c1 . (c2 `1 )) `2 ) in F1() by E13, CQC_LANG:def 1;
end;
suppose c2 `2 <> 0 ;
hence IFEQ (c2 `2 ),0,((c1 . (c2 `1 )) `1 ),((c1 . (c2 `1 )) `2 ) in F1() by E13, CQC_LANG:def 1;
end;
end;
end;
hence IFEQ (c2 `2 ),0,((c1 . (c2 `1 )) `1 ),((c1 . (c2 `1 )) `2 ) in F1() ;
end;
consider c2 being Function of [:F1(),NAT :],F1() such that
E13: for b1 being set holds
( b1 in [:F1(),NAT :] implies c2 . b1 = H1(b1) ) from FUNCT_2:sch 2(E12);
 E14: for b1 being set holds
( b1 in F1() implies P1[b1,c2 . [b1,0],c2 . [b1,1]] )
proof
let c3 be set ;
assume E15: c3 in F1() ;
then consider c4, c5 being Element of F1() such that
E16: P1[c3,c4,c5]
and E17: c1 . c3 = [c4,c5] by E11;
E18: [c3,0] `2 = 0 by MCART_1:7;
[c3,0] in [:F1(),NAT :] by E15, ZFMISC_1:106;
then E19: c2 . [c3,0] = IFEQ ([c3,0] `2 ),0,((c1 . ([c3,0] `1 )) `1 ),((c1 . ([c3,0] `1 )) `2 ) by E13
.= (c1 . ([c3,0] `1 )) `1 by E18, CQC_LANG:def 1
.= (c1 . c3) `1 by MCART_1:7
.= c4 by E17, MCART_1:7 ;
E20: ( [c3,1] `2 = 1 & 1 <> 0 ) by MCART_1:7;
[c3,1] in [:F1(),NAT :] by E15, ZFMISC_1:106;
then c2 . [c3,1] = IFEQ ([c3,1] `2 ),0,((c1 . ([c3,1] `1 )) `1 ),((c1 . ([c3,1] `1 )) `2 ) by E13
.= (c1 . ([c3,1] `1 )) `2 by E20, CQC_LANG:def 1
.= (c1 . c3) `2 by MCART_1:7
.= c5 by E17, MCART_1:7 ;
hence P1[c3,c2 . [c3,0],c2 . [c3,1]] by E16, E19;
end;
deffunc H2( set ) -> Element of NAT = 2;
consider c3 being DecoratedTree of F1() such that
E15: c3 . {} = F2()
and E16: for b1 being Element of dom c3 holds
( succ b1 = { (b1 ^ <*b2*>) where B is Nat : b2 < H2(c3 . b1) } & for b2 being Nat holds
( b2 < H2(c3 . b1) implies c3 . (b1 ^ <*b2*>) = c2 . [(c3 . b1),b2] ) ) from TREES_2:sch 9();
now
let c4 be Element of dom c3;
assume not c4 in Leaves (dom c3) ;
{ (c4 ^ <*b1*>) where B is Nat : b1 < 2 } = {(c4 ^ <*0*>),(c4 ^ <*1*>)}
proof
thus { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } c= {(c4 ^ <*0*>),(c4 ^ <*1*>)} :: uses XBOOLE_0:def 10
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c6 being Nat such that
E17: c5 = c4 ^ <*c6*>
and E18: c6 < 2 ;
( c6 = 0 or c6 = 1 ) by E18, NAT_1:71;
hence c5 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E17, TARSKI:def 2;
end;
let c5 be set ; :: uses TARSKI:def 3
assume c5 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} ;
then ( c5 = c4 ^ <*0*> or c5 = c4 ^ <*1*> ) by TARSKI:def 2;
hence c5 in { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } ;
end;
hence succ c4 = {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E16;
end;
then dom c3 is binary by BINTREE1:def 2;
then reconsider c4 = c3 as binary DecoratedTree of F1() by BINTREE1:def 3;
take c4 ;
now
let c5 be Element of dom c4;
{ (c5 ^ <*b1*>) where B is Nat : b1 < 2 } = {(c5 ^ <*0*>),(c5 ^ <*1*>)}
proof
thus { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } c= {(c5 ^ <*0*>),(c5 ^ <*1*>)} :: uses XBOOLE_0:def 10
proof
let c6 be set ; :: uses TARSKI:def 3
assume c6 in { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c7 being Nat such that
E17: c6 = c5 ^ <*c7*>
and E18: c7 < 2 ;
( c7 = 0 or c7 = 1 ) by E18, NAT_1:71;
hence c6 in {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E17, TARSKI:def 2;
end;
let c6 be set ; :: uses TARSKI:def 3
assume c6 in {(c5 ^ <*0*>),(c5 ^ <*1*>)} ;
then ( c6 = c5 ^ <*0*> or c6 = c5 ^ <*1*> ) by TARSKI:def 2;
hence c6 in { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } ;
end;
hence succ c5 = {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E16;
end;
hence dom c4 = {0,1} * by E6;
thus c4 . {} = F2() by E15;
let c5 be Node of c4;
P1[c4 . c5,c2 . [(c4 . c5),0],c2 . [(c4 . c5),1]] by E14;
then P1[c4 . c5,c4 . (c5 ^ <*0*>),c2 . [(c4 . c5),1]] by E16;
hence P1[c4 . c5,c4 . (c5 ^ <*0*>),c4 . (c5 ^ <*1*>)] by E16;
end;

scheme :: BINTREE2:sch 2
s2{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set ], P2[ set , set ] } :
ex b1 being binary DecoratedTree of F1() st
( dom b1 = {0,1} * & b1 . {} = F2() & for b2 being Node of b1 holds
( P1[b1 . b2,b1 . (b2 ^ <*0*>)] & P2[b1 . b2,b1 . (b2 ^ <*1*>)] ) )
provided
E7: for b1 being Element of F1() holds
ex b2 being Element of F1() st P1[b1,b2] and E8: for b1 being Element of F1() holds
ex b2 being Element of F1() st P2[b1,b2]
proof
defpred S1[ set , set ] means ( ( a1 `2 = 0 implies P1[a1 `1 ,a2] ) & ( a1 `2 = 1 implies P2[a1 `1 ,a2] ) );
E9: for b1 being set holds
not ( b1 in [:F1(),NAT :] & for b2 being set holds
not ( b2 in F1() & S1[b1,b2] ) )
proof
let c1 be set ;
assume c1 in [:F1(),NAT :] ;
then reconsider c2 = c1 `1 as Element of F1() by MCART_1:10;
consider c3 being Element of F1() such that
E10: P1[c2,c3] by E7;
consider c4 being Element of F1() such that
E11: P2[c2,c4] by E8;
take c5 = IFEQ (c1 `2 ),0,c3,c4;
thus c5 in F1() ;
thus ( c1 `2 = 0 implies P1[c1 `1 ,c5] ) by E10, CQC_LANG:def 1;
thus ( c1 `2 = 1 implies P2[c1 `1 ,c5] ) by E11, CQC_LANG:def 1;
end;
consider c1 being Function such that
E10: dom c1 = [:F1(),NAT :]
and E11: rng c1 c= F1()
and E12: for b1 being set holds
( b1 in [:F1(),NAT :] implies S1[b1,c1 . b1] ) from WELLORD2:sch 1(E9);
 reconsider c2 = c1 as Function of [:F1(),NAT :],F1() by E10, E11, FUNCT_2:4;
deffunc H1( set ) -> Element of NAT = 2;
consider c3 being DecoratedTree of F1() such that
E13: c3 . {} = F2()
and E14: for b1 being Element of dom c3 holds
( succ b1 = { (b1 ^ <*b2*>) where B is Nat : b2 < H1(c3 . b1) } & for b2 being Nat holds
( b2 < H1(c3 . b1) implies c3 . (b1 ^ <*b2*>) = c2 . [(c3 . b1),b2] ) ) from TREES_2:sch 9();
now
let c4 be Element of dom c3;
assume not c4 in Leaves (dom c3) ;
{ (c4 ^ <*b1*>) where B is Nat : b1 < 2 } = {(c4 ^ <*0*>),(c4 ^ <*1*>)}
proof
thus { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } c= {(c4 ^ <*0*>),(c4 ^ <*1*>)} :: uses XBOOLE_0:def 10
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c6 being Nat such that
E15: c5 = c4 ^ <*c6*>
and E16: c6 < 2 ;
( c6 = 0 or c6 = 1 ) by E16, NAT_1:71;
hence c5 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E15, TARSKI:def 2;
end;
let c5 be set ; :: uses TARSKI:def 3
assume c5 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} ;
then ( c5 = c4 ^ <*0*> or c5 = c4 ^ <*1*> ) by TARSKI:def 2;
hence c5 in { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } ;
end;
hence succ c4 = {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E14;
end;
then dom c3 is binary by BINTREE1:def 2;
then reconsider c4 = c3 as binary DecoratedTree of F1() by BINTREE1:def 3;
take c4 ;
now
let c5 be Element of dom c4;
{ (c5 ^ <*b1*>) where B is Nat : b1 < 2 } = {(c5 ^ <*0*>),(c5 ^ <*1*>)}
proof
thus { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } c= {(c5 ^ <*0*>),(c5 ^ <*1*>)} :: uses XBOOLE_0:def 10
proof
let c6 be set ; :: uses TARSKI:def 3
assume c6 in { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c7 being Nat such that
E15: c6 = c5 ^ <*c7*>
and E16: c7 < 2 ;
( c7 = 0 or c7 = 1 ) by E16, NAT_1:71;
hence c6 in {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E15, TARSKI:def 2;
end;
let c6 be set ; :: uses TARSKI:def 3
assume c6 in {(c5 ^ <*0*>),(c5 ^ <*1*>)} ;
then ( c6 = c5 ^ <*0*> or c6 = c5 ^ <*1*> ) by TARSKI:def 2;
hence c6 in { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } ;
end;
hence succ c5 = {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E14;
end;
hence dom c4 = {0,1} * by E6;
thus c4 . {} = F2() by E13;
let c5 be Node of c4;
[(c4 . c5),0] `2 = 0 by MCART_1:7;
then P1[[(c4 . c5),0] `1 ,c2 . [(c4 . c5),0]] by E12;
then P1[c4 . c5,c2 . [(c4 . c5),0]] by MCART_1:7;
hence P1[c4 . c5,c4 . (c5 ^ <*0*>)] by E14;
[(c4 . c5),1] `2 = 1 by MCART_1:7;
then P2[[(c4 . c5),1] `1 ,c2 . [(c4 . c5),1]] by E12;
then P2[c4 . c5,c2 . [(c4 . c5),1]] by MCART_1:7;
hence P2[c4 . c5,c4 . (c5 ^ <*1*>)] by E14;
end;

E7: for b1 being non empty set
for b2 being FinSequence of b1 holds
Rev b2 is FinSequence of b1
;

definition
let c1 be binary Tree;
let c2 be non empty Nat;
func NumberOnLevel a2,a1 -> Function of a1 -level a2, NAT means :E8: :: BINTREE2:def 1
for b1 being Element of a1 holds
( b1 in a1 -level a2 implies for b2 being Tuple of a2,BOOLEAN holds
( b2 = Rev b1 implies a3 . b1 = (Absval b2) + 1 ) );
existence
ex b1 being Function of c1 -level c2, NAT st
for b2 being Element of c1 holds
( b2 in c1 -level c2 implies for b3 being Tuple of c2,BOOLEAN holds
( b3 = Rev b2 implies b1 . b2 = (Absval b3) + 1 ) )
proof
defpred S1[ set , set ] means ex b1 being Element of c1 st
( b1 = a1 & for b2 being Tuple of c2,BOOLEAN holds
( b2 = Rev b1 implies a2 = (Absval b2) + 1 ) );
E8: for b1 being set holds
not ( b1 in c1 -level c2 & for b2 being set holds
not ( b2 in NAT & S1[b1,b2] ) )
proof
let c3 be set ;
assume c3 in c1 -level c2 ;
then c3 in { b1 where B is Element of c1 : len b1 = c2 } by TREES_2:def 6;
then consider c4 being Element of c1 such that
E9: c4 = c3
and E10: len c4 = c2 ;
len (Rev c4) = c2 by E10, FINSEQ_5:def 3;
then reconsider c5 = Rev c4 as Tuple of c2,BOOLEAN by FINSEQ_2:110;
take c6 = (Absval c5) + 1;
thus c6 in NAT ;
take c4 ;
thus c4 = c3 by E9;
let c7 be Tuple of c2,BOOLEAN ;
assume c7 = Rev c4 ;
hence c6 = (Absval c7) + 1 ;
end;
consider c3 being Function such that
E9: dom c3 = c1 -level c2
and E10: rng c3 c= NAT
and E11: for b1 being set holds
( b1 in c1 -level c2 implies S1[b1,c3 . b1] ) from WELLORD2:sch 1(E8);
 reconsider c4 = c3 as Function of c1 -level c2, NAT by E9, E10, FUNCT_2:4;
take c4 ;
let c5 be Element of c1;
assume c5 in c1 -level c2 ;
then consider c6 being Element of c1 such that
E12: c6 = c5
and E13: for b1 being Tuple of c2,BOOLEAN holds
( b1 = Rev c6 implies c4 . c5 = (Absval b1) + 1 ) by E11;
let c7 be Tuple of c2,BOOLEAN ;
assume c7 = Rev c5 ;
hence c4 . c5 = (Absval c7) + 1 by E12, E13;
end;
uniqueness
for b1, b2 being Function of c1 -level c2, NAT holds
( ( for b