:: BINTREE2 semantic presentation

Lemma1: for b1 being set
for b2, b3 being FinSequence of b1 holds
b2 ^ b3 is FinSequence of b1
;

Lemma2: for b1 being non empty set
for b2 being Element of b1 holds
<*b2*> is FinSequence of b1
;

theorem Th1: :: 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 Th2: :: 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 E5: S1[ <*> NAT ] by XBOOLE_1:2;
E6: 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 E7: S1[c3] ;
assume E8: 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 E8;
then E9: 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 E9, TARSKI:def 2;
then ( c4 = 0 or c4 = 1 ) by FINSEQ_2:20;
then E10: c4 in {0,1} by TARSKI:def 2;
E11: {c4} c= BOOLEAN
proof
let c6 be set ; :: according to TARSKI:def 3
assume c6 in {c4} ;
hence c6 in BOOLEAN by E10, MARGREL1:def 12, TARSKI:def 1;
end;
rng <*c4*> = {c4} by FINSEQ_1:55;
then (rng c3) \/ (rng <*c4*>) c= BOOLEAN by E7, E8, E11, 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(E5, E6);
 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 c1 -> FinSequence of BOOLEAN ;
coherence
for b1 being Element of c1 holds
b1 is FinSequence of BOOLEAN by Th2;
end;

theorem Th3: :: BINTREE2:3
for b1 being Tree holds
( b1 = {0,1} * implies b1 is binary )
proof
let c1 be Tree;
assume E6: 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*>)} :: according to XBOOLE_0:def 10
proof
let c3 be set ; :: according to TARSKI:def 3
assume c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } ;
then consider c4 being Nat such that
E7: c3 = c2 ^ <*c4*> and
E8: c2 ^ <*c4*> in c1 ;
reconsider c5 = c2 ^ <*c4*> as FinSequence of {0,1} by E6, E8, 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 E7, TARSKI:def 2;
end;
let c3 be set ; :: according to TARSKI:def 3
E7: c2 is FinSequence of {0,1} by E6, FINSEQ_1:def 11;
rng <*0*> c= {0,1}
proof
let c4 be set ; :: according to 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 E8: <*0*> is FinSequence of {0,1} by FINSEQ_1:def 4;
rng <*1*> c= {0,1}
proof
let c4 be set ; :: according to 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 E9: <*1*> is FinSequence of {0,1} by FINSEQ_1:def 4;
c2 ^ <*0*> is FinSequence of {0,1} by E7, E8, Lemma1;
then E10: c2 ^ <*0*> in c1 by E6, FINSEQ_1:def 11;
c2 ^ <*1*> is FinSequence of {0,1} by E7, E9, Lemma1;
then E11: c2 ^ <*1*> in c1 by E6, 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 E10, E11;
end;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by TREES_2:def 5;
end;
hence c1 is binary by BINTREE1:def 2;
end;

theorem Th4: :: BINTREE2:4
for b1 being Tree holds
( b1 = {0,1} * implies Leaves b1 = {} )
proof
let c1 be Tree;
assume E7: c1 = {0,1} * ;
assume Leaves c1 <> {} ;
then consider c2 being set such that
E8: c2 in Leaves c1 by XBOOLE_0:def 1;
reconsider c3 = c2 as Element of c1 by E8;
c1 is binary by E7, Th3;
then E9: c3 is FinSequence of BOOLEAN by Th2;
then reconsider c4 = c2 as FinSequence of NAT ;
set c5 = c4 ^ <*0*>;
E10: 0 in {0} by TARSKI:def 1;
{0} c= BOOLEAN
proof
let c6 be set ; :: according to 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 E10, Lemma2;
then c4 ^ <*0*> is FinSequence of BOOLEAN by E9, Lemma1;
then E11: c4 ^ <*0*> in c1 by E7, FINSEQ_1:def 11, MARGREL1:def 12;
c4 is_a_proper_prefix_of c4 ^ <*0*> by TREES_1:31;
hence not verum by E8, E11, TREES_1:def 8;
end;

theorem Th5: :: 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 Th6: :: 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 E7: for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ;
assume Leaves c1 <> {} ;
then consider c2 being set such that
E8: c2 in Leaves c1 by XBOOLE_0:def 1;
reconsider c3 = c2 as Element of c1 by E8;
succ c3 = {(c3 ^ <*0*>),(c3 ^ <*1*>)} by E7;
hence not verum by E8, BINTREE1:5;
end;

theorem Th7: :: 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 Th8: :: 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 E9: c1 = {0,1} * ;
then E10: c1 is binary by Th3;
let c2 be Element of c1;
not c2 in Leaves c1 by E9, Th4;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E10, BINTREE1:def 2;
end;
assume E9: for b1 being Element of c1 holds succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ;
thus c1 = {0,1} *
proof
thus c1 c= {0,1} * :: according to XBOOLE_0:def 10
proof
let c2 be set ; :: according to TARSKI:def 3
E10: c1 is binary by E9, Th7;
assume c2 in c1 ;
then c2 is FinSequence of {0,1} by E10, Th2, MARGREL1:def 12;
hence c2 in {0,1} * by FINSEQ_1:def 11;
end;
let c2 be set ; :: according to TARSKI:def 3
assume c2 in {0,1} * ;
then E10: c2 is FinSequence of {0,1} by FINSEQ_1:def 11;
defpred S1[ FinSequence] means a1 in c1;
E11: S1[ <*> {0,1}] by TREES_1:47;
E12: 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 ;
E13: succ c5 = {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E9;
( c4 = 0 or c4 = 1 ) by TARSKI:def 2;
then c3 ^ <*c4*> in succ c5 by E13, TARSKI:def 2;
hence c3 ^ <*c4*> in c1 ;
end;
for b1 being FinSequence of {0,1} holds
S1[b1] from FINSEQ_2:sch 2(E11, E12);
 hence c2 in c1 by E10;
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
E9: 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] );
E10: 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
E11: P1[c1,c2,c3] by E9;
take c4 = [c2,c3];
thus c4 in [:F1(),F1():] ;
thus S1[c1,c4] by E11;
end;
consider c1 being Function such that
E11: dom c1 = F1() and
E12: rng c1 c= [:F1(),F1():] and
E13: for b1 being set holds
( b1 in F1() implies S1[b1,c1 . b1] ) from WELLORD2:sch 1(E10);
 deffunc H1( set ) -> set = IFEQ (a1 `2 ),0,((c1 . (a1 `1 )) `1 ),((c1 . (a1 `1 )) `2 );
E14: 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 E11, FUNCT_1:def 5;
then E15: ( (c1 . (c2 `1 )) `1 in F1() & (c1 . (c2 `1 )) `2 in F1() ) by E12, 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 E15, 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 E15, 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
E15: for b1 being set holds
( b1 in [:F1(),NAT :] implies c2 . b1 = H1(b1) ) from FUNCT_2:sch 2(E14);
 E16: for b1 being set holds
( b1 in F1() implies P1[b1,c2 . [b1,0],c2 . [b1,1]] )
proof
let c3 be set ;
assume E17: c3 in F1() ;
then consider c4, c5 being Element of F1() such that
E18: P1[c3,c4,c5] and
E19: c1 . c3 = [c4,c5] by E13;
E20: [c3,0] `2 = 0 by MCART_1:7;
[c3,0] in [:F1(),NAT :] by E17, ZFMISC_1:106;
then E21: c2 . [c3,0] = IFEQ ([c3,0] `2 ),0,((c1 . ([c3,0] `1 )) `1 ),((c1 . ([c3,0] `1 )) `2 ) by E15
.= (c1 . ([c3,0] `1 )) `1 by E20, CQC_LANG:def 1
.= (c1 . c3) `1 by MCART_1:7
.= c4 by E19, MCART_1:7 ;
E22: ( [c3,1] `2 = 1 & 1 <> 0 ) by MCART_1:7;
[c3,1] in [:F1(),NAT :] by E17, ZFMISC_1:106;
then c2 . [c3,1] = IFEQ ([c3,1] `2 ),0,((c1 . ([c3,1] `1 )) `1 ),((c1 . ([c3,1] `1 )) `2 ) by E15
.= (c1 . ([c3,1] `1 )) `2 by E22, CQC_LANG:def 1
.= (c1 . c3) `2 by MCART_1:7
.= c5 by E19, MCART_1:7 ;
hence P1[c3,c2 . [c3,0],c2 . [c3,1]] by E18, E21;
end;
deffunc H2( set ) -> Element of NAT = 2;
consider c3 being DecoratedTree of F1() such that
E17: c3 . {} = F2() and
E18: 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*>)} :: according to XBOOLE_0:def 10
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { (c4 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c6 being Nat such that
E19: c5 = c4 ^ <*c6*> and
E20: c6 < 2 ;
( c6 = 0 or c6 = 1 ) by E20, NAT_1:71;
hence c5 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E19, TARSKI:def 2;
end;
let c5 be set ; :: according to 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 E18;
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*>)} :: according to XBOOLE_0:def 10
proof
let c6 be set ; :: according to TARSKI:def 3
assume c6 in { (c5 ^ <*b1*>) where B is Nat : b1 < 2 } ;
then consider c7 being Nat such that
E19: c6 = c5 ^ <*c7*> and
E20: c7 < 2 ;
( c7 = 0 or c7 = 1 ) by E20, NAT_1:71;
hence c6 in {(c5 ^ <*0*>),(c5 ^ <*1*>)} by E19, TARSKI:def 2;
end;
let c6 be set ; :: according to 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 E18;
end;
hence dom c4 = {0,1} * by Th8;
thus c4 . {} = F2() by E17;
let c5 be Node of c4;
P1[c4 . c5,c2 . [(c4 . c5),0],c2 . [(c4 . c5),1]] by E16;
then P1[c4 . c5,c4 . (c5 ^ <*0*>),c2 . [(c4 . c5),1]] by E18;
hence P1[c4 . c5,c4 . (c5 ^ <*0*>),c4 . (c5 ^ <*1*>)] by E18;
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
E9: for b1 being Element of F1() holds
ex b2 being Element of F1() st P1[b1,b2] and E10: 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] ) );
E11: 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
E12: P1[c2,c3] by E9;
consider c4 being Element of F1() such that
E13: P2[c2,c4] by E10;
take c5 = IFEQ (c1 `2 ),0,c3,c4;
thus c5 in F1() ;
thus ( c1 `2 = 0 implies P1[c1 `1 ,c5] ) by E12, CQC_LANG:def 1;
thus ( c1 `2 = 1 implies P2[c1 `1 ,c5] ) by E13, CQC_LANG:def 1;
end;
consider c1 being Function such that
E12: dom c1 = [:F1(),NAT :] and
E13: rng c1 c= F1() and
E14: for b1 being set holds
( b1 in [:F1(),NAT :] implies S1[b1,c1 . b1] ) from WELLORD2:sch 1(E11);
 reconsider c2 = c1 as Function of [:F1(),NAT :],F1() by E12, E13, FUNCT_2:4;
deffunc H1( 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 < 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*>)} :: according to XBOOLE_0:def 10
proof
let c5 be set ; :: according to 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 ; :: according to 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*>)} :: according to XBOOLE_0:def 10
proof
let c6 be set ; :: according to 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 ; :: according to 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 = {