:: BINTREE1 semantic presentation

definition
let c1 be non empty set ;
let c2 be DecoratedTree of c1;
func root-label c2 -> Element of a1 equals :: BINTREE1:def 1
a2 . {} ;
coherence
c2 . {} is Element of c1
proof
reconsider c3 = {} as Node of c2 by TREES_1:47;
c2 . c3 is Element of c1 ;
hence c2 . {} is Element of c1 ;
end;
end;

:: deftheorem Def1 defines root-label BINTREE1:def 1 :
for b1 being non empty set
for b2 being DecoratedTree of b1 holds root-label b2 = b2 . {} ;

theorem Th1: :: BINTREE1:1
for b1 being non empty set
for b2 being DecoratedTree of b1 holds roots <*b2*> = <*(root-label b2)*> by DTCONSTR:4;

theorem Th2: :: BINTREE1:2
for b1 being non empty set
for b2, b3 being DecoratedTree of b1 holds roots <*b2,b3*> = <*(root-label b2),(root-label b3)*> by DTCONSTR:6;

definition
let c1 be Tree;
attr a1 is binary means :Def2: :: BINTREE1:def 2
for b1 being Element of a1 holds
( not b1 in Leaves a1 implies succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} );
end;

:: deftheorem Def2 defines binary BINTREE1:def 2 :
for b1 being Tree holds
( b1 is binary iff for b2 being Element of b1 holds
( not b2 in Leaves b1 implies succ b2 = {(b2 ^ <*0*>),(b2 ^ <*1*>)} ) );

theorem Th3: :: BINTREE1:3
canceled;

theorem Th4: :: BINTREE1:4
canceled;

theorem Th5: :: BINTREE1:5
for b1 being Tree
for b2 being Element of b1 holds
( succ b2 = {} iff b2 in Leaves b1 )
proof
let c1 be Tree;
let c2 be Element of c1;
hereby
assume succ c2 = {} ;
then not c2 ^ <*0*> in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } by TREES_2:def 5;
then not c2 ^ <*0*> in c1 ;
hence c2 in Leaves c1 by MODAL_1:53;
end;
assume c2 in Leaves c1 ;
then E2: not c2 ^ <*0*> in c1 by MODAL_1:53;
assume E3: succ c2 <> {} ;
consider c3 being Element of succ c2;
c3 in succ c2 by E3;
then c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } by TREES_2:def 5;
then consider c4 being Nat such that
E4: ( c3 = c2 ^ <*c4*> & c2 ^ <*c4*> in c1 ) ;
0 <= c4 by NAT_1:18;
hence not verum by E2, E4, TREES_1:def 5;
end;

theorem Th6: :: BINTREE1:6
elementary_tree 0 is binary
proof
set c1 = elementary_tree 0;
let c2 be Element of elementary_tree 0; :: according to BINTREE1:def 2
now
let c3 be FinSequence of NAT ;
assume c3 in elementary_tree 0 ;
then ( c3 = {} & c2 = {} ) by TARSKI:def 1, TREES_1:56;
hence not c2 is_a_proper_prefix_of c3 ;
end;
hence ( not c2 in Leaves (elementary_tree 0) implies succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} ) by TREES_1:def 8;
end;

theorem Th7: :: BINTREE1:7
elementary_tree 2 is binary
proof
set c1 = elementary_tree 2;
let c2 be Element of elementary_tree 2; :: according to BINTREE1:def 2
assume E3: not c2 in Leaves (elementary_tree 2) ;
per cases not ( not c2 = {} & not c2 = <*0*> & not c2 = <*1*> ) by ENUMSET1:def 1, MODAL_1:10;
suppose E4: c2 = {} ;
E5: succ c2 = { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in elementary_tree 2 } by TREES_2:def 5;
for b1 being set holds
( b1 in { (c2 ^ <*b2*>) where B is Nat : c2 ^ <*b2*> in elementary_tree 2 } iff b1 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} )
proof
let c3 be set ;
hereby
assume c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in elementary_tree 2 } ;
then consider c4 being Nat such that
E6: ( c3 = c2 ^ <*c4*> & c2 ^ <*c4*> in elementary_tree 2 ) ;
E7: c3 = <*c4*> by E4, E6, FINSEQ_1:47;
reconsider c5 = c3 as FinSequence by E6;
per cases not ( not c3 = {} & not c3 = <*0*> & not c3 = <*1*> ) by E6, ENUMSET1:def 1, MODAL_1:10;
suppose c3 = {} ;
then ( len c5 = 0 & len c5 = 1 ) by E7;
hence c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} ;
end;
suppose c3 = <*0*> ;
then c5 = c2 ^ <*0*> by E4, FINSEQ_1:47;
hence c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} by TARSKI:def 2;
end;
suppose c3 = <*1*> ;
then c5 = c2 ^ <*1*> by E4, FINSEQ_1:47;
hence c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} by TARSKI:def 2;
end;
end;
end;
assume E6: c3 in {(c2 ^ <*0*>),(c2 ^ <*1*>)} ;
then E7: ( c3 = c2 ^ <*0*> or c3 = c2 ^ <*1*> ) by TARSKI:def 2;
reconsider c4 = c3 as FinSequence by E6, TARSKI:def 2;
( c4 = <*0*> or c4 = <*1*> ) by E4, E7, FINSEQ_1:47;
then c4 in elementary_tree 2 by ENUMSET1:def 1, MODAL_1:10;
hence c3 in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in elementary_tree 2 } by E7;
end;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E5, TARSKI:2;
end;
suppose E4: c2 = <*0*> ;
now
assume E5: c2 ^ <*0*> in elementary_tree 2 ;
per cases not ( not c2 ^ <*0*> = {} & not c2 ^ <*0*> = <*0*> & not c2 ^ <*0*> = <*1*> ) by E5, ENUMSET1:def 1, MODAL_1:10;
suppose c2 ^ <*0*> = {} ;
then len (c2 ^ <*0*>) = 0 ;
then (len c2) + (len <*0*>) = 0 by FINSEQ_1:35;
then 1 + (len <*0*>) = 0 by E4, FINSEQ_1:56;
then 1 + 1 = 0 by FINSEQ_1:56;
hence not verum ;
end;
suppose c2 ^ <*0*> = <*0*> ;
then (len <*0*>) + (len <*0*>) = len <*0*> by E4, FINSEQ_1:35;
then 1 + (len <*0*>) = len <*0*> by FINSEQ_1:56;
then 1 + 1 = len <*0*> ;
hence not verum by FINSEQ_1:56;
end;
suppose c2 ^ <*0*> = <*1*> ;
then (len <*0*>) + (len <*0*>) = len <*1*> by E4, FINSEQ_1:35;
then 1 + (len <*0*>) = len <*1*> by FINSEQ_1:56;
then 1 + 1 = len <*1*> by FINSEQ_1:56;
hence not verum by FINSEQ_1:56;
end;
end;
end;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E3, MODAL_1:53;
end;
suppose E4: c2 = <*1*> ;
now
assume E5: c2 ^ <*0*> in elementary_tree 2 ;
per cases not ( not c2 ^ <*0*> = {} & not c2 ^ <*0*> = <*0*> & not c2 ^ <*0*> = <*1*> ) by E5, ENUMSET1:def 1, MODAL_1:10;
suppose c2 ^ <*0*> = {} ;
then len (c2 ^ <*0*>) = 0 ;
then (len c2) + (len <*0*>) = 0 by FINSEQ_1:35;
then 1 + (len <*0*>) = 0 by E4, FINSEQ_1:56;
then 1 + 1 = 0 by FINSEQ_1:56;
hence not verum ;
end;
suppose c2 ^ <*0*> = <*0*> ;
then (len <*1*>) + (len <*0*>) = len <*0*> by E4, FINSEQ_1:35;
then 1 + (len <*0*>) = len <*0*> by FINSEQ_1:56;
then 1 + 1 = len <*0*> ;
hence not verum by FINSEQ_1:56;
end;
suppose c2 ^ <*0*> = <*1*> ;
then (len <*1*>) + (len <*0*>) = len <*1*> by E4, FINSEQ_1:35;
then 1 + (len <*0*>) = len <*1*> by FINSEQ_1:56;
then 1 + 1 = len <*1*> by FINSEQ_1:56;
hence not verum by FINSEQ_1:56;
end;
end;
end;
hence succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E3, MODAL_1:53;
end;
end;
end;

registration
cluster finite binary set ;
existence
ex b1 being Tree st
( b1 is binary & b1 is finite ) by Th6;
end;

definition
let c1 be DecoratedTree;
attr a1 is binary means :Def3: :: BINTREE1:def 3
 dom a1 is binary;
end;

:: deftheorem Def3 defines binary BINTREE1:def 3 :
for b1 being DecoratedTree holds
( b1 is binary iff dom b1 is binary );

registration
let c1 be non empty set ;
cluster finite binary ParametrizedSubset of a1;
existence
ex b1 being DecoratedTree of c1 st
( b1 is binary & b1 is finite )
proof
consider c2 being finite binary Tree;
consider c3 being Function of c2,c1;
rng c3 c= c1 ;
then reconsider c4 = c3 as DecoratedTree of c1 by TREES_2:def 9;
take c4 ;
dom c4 = c2 by FUNCT_2:def 1;
hence ( dom c4 is binary & c4 is finite ) by FINSET_1:29; :: according to BINTREE1:def 3
end;
end;

registration
cluster finite binary set ;
existence
ex b1 being DecoratedTree st
( b1 is binary & b1 is finite )
proof
consider c1 being non empty set ;
consider c2 being finite binary DecoratedTree of c1;
take c2 ;
thus ( c2 is binary & c2 is finite ) ;
end;
end;

registration
cluster binary -> finite-order set ;
coherence
for b1 being Tree holds
( b1 is binary implies b1 is finite-order )
proof
let c1 be Tree;
assume E4: c1 is binary ;
now
let c2 be Element of c1;
assume E5: c2 ^ <*2*> in c1 ;
then E6: c2 ^ <*0*> in c1 by TREES_1:def 5;
per cases not ( not c2 in Leaves c1 & c2 in Leaves c1 ) ;
suppose c2 in Leaves c1 ;
hence not verum by E6, MODAL_1:53;
end;
suppose not c2 in Leaves c1 ;
then E7: succ c2 = {(c2 ^ <*0*>),(c2 ^ <*1*>)} by E4, Def2;
c2 ^ <*2*> in { (c2 ^ <*b1*>) where B is Nat : c2 ^ <*b1*> in c1 } by E5;
then c2 ^ <*2*> in succ c2 by TREES_2:def 5;
then E8: ( c2 ^ <*2*> = c2 ^ <*0*> or c2 ^ <*2*> = c2 ^ <*1*> ) by E7, TARSKI:def 2;
E9: now
assume <*2*> = <*0*> ;
then ( <*2*> . 1 = 2 & <*2*> . 1 = 0 ) by FINSEQ_1:57;
hence not verum ;
end;
now
assume <*2*> = <*1*> ;
then ( <*2*> . 1 = 2 & <*2*> . 1 = 1 ) by FINSEQ_1:57;
hence not verum ;
end;
hence not verum by E8, E9, FINSEQ_1:46;
end;
end;
end;
hence c1 is finite-order by TREES_2:def 2;
end;
end;

theorem Th8: :: BINTREE1:8
for b1, b2 being Tree
for b3 being Element of tree b1,b2 holds
( ( for b4 being Element of b1 holds
( b3 = <*0*> ^ b4 implies ( b3 in Leaves (tree b1,b2) iff b4 in Leaves b1 ) ) ) & ( for b4 being Element of b2 holds
( b3 = <*1*> ^ b4 implies ( b3 in Leaves (tree b1,b2) iff b4 in Leaves b2 ) ) ) )
proof
let c1, c2 be Tree;
let c3 be Element of tree c1,c2;
set c4 = tree c1,c2;
hereby
let c5 be Element of c1;
assume E5: c3 = <*0*> ^ c5 ;
hereby
assume E6: c3 in Leaves (tree c1,c2) ;
assume not c5 in Leaves c1 ;
then consider c6 being Nat such that
E7: c5 ^ <*c6*> in c1 by MODAL_1:54;
<*0*> ^ (c5 ^ <*c6*>) in tree c1,c2 by E7, TREES_3:72;
then (<*0*> ^ c5) ^ <*c6*> in tree c1,c2 by FINSEQ_1:45;
hence not verum by E5, E6, MODAL_1:54;
end;
assume E6: c5 in Leaves c1 ;
assume not c3 in Leaves (tree c1,c2) ;
then consider c6 being Nat such that
E7: c3 ^ <*c6*> in tree c1,c2 by MODAL_1:54;
<*0*> ^ (c5 ^ <*c6*>) in tree c1,c2 by E5, E7, FINSEQ_1:45;
then c5 ^ <*c6*> in c1 by TREES_3:72;
hence not verum by E6, MODAL_1:54;
end;
let c5 be Element of c2;
assume E5: c3 = <*1*> ^ c5 ;
hereby
assume E6: c3 in Leaves (tree c1,c2) ;
assume not c5 in Leaves c2 ;
then consider c6 being Nat such that
E7: c5 ^ <*c6*> in c2 by MODAL_1:54;
<*1*> ^ (c5 ^ <*c6*>) in tree c1,c2 by E7, TREES_3:73;
then (<*1*> ^ c5) ^ <*c6*> in tree c1,c2 by FINSEQ_1:45;
hence not verum by E5, E6, MODAL_1:54;
end;
assume E6: c5 in Leaves c2 ;
assume not c3 in Leaves (tree c1,c2) ;
then consider c6 being Nat such that
E7: c3 ^ <*c6*> in tree c1,c2 by MODAL_1:54;
<*1*> ^ (c5 ^ <*c6*>) in tree c1,c2 by E5, E7, FINSEQ_1:45;
then c5 ^ <*c6*> in c2 by TREES_3:73;
hence not verum by E6, MODAL_1:54;
end;

theorem Th9: :: BINTREE1:9
for b1, b2 being Tree
for b3 being Element of tree b1,b2 holds
( ( b3 = {} implies succ b3 = {(b3 ^ <*0*>),(b3 ^ <*1*>)} ) & ( for b4 being Element of b1 holds
( b3 = <*0*> ^ b4 implies for b5 being FinSequence holds
( b5 in succ b4 iff <*0*> ^ b5 in succ b3 ) ) ) & ( for b4 being Element of b2 holds
( b3 = <*1*> ^ b4 implies for b5 being FinSequence holds
( b5 in succ b4 iff <*1*> ^ b5 in succ b3 ) ) ) )
proof
let c1, c2 be Tree;
let c3 be Element of tree c1,c2;
set c4 = tree c1,c2;
hereby
assume E6: c3 = {} ;
E7: succ c3 = { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in tree c1,c2 } by TREES_2:def 5;
( {} in c1 & <*0*> = <*0*> ^ {} ) by FINSEQ_1:47, TREES_1:47;
then <*0*> in tree c1,c2 by TREES_3:71;
then E8: c3 ^ <*0*> in tree c1,c2 by E6, FINSEQ_1:47;
( {} in c2 & <*1*> = <*1*> ^ {} ) by FINSEQ_1:47, TREES_1:47;
then <*1*> in tree c1,c2 by TREES_3:71;
then E9: c3 ^ <*1*> in tree c1,c2 by E6, FINSEQ_1:47;
now
let c5 be set ;
hereby
assume c5 in succ c3 ;
then consider c6 being Nat such that
E10: ( c5 = c3 ^ <*c6*> & c3 ^ <*c6*> in tree c1,c2 ) by E7;
E11: c5 = <*c6*> by E6, E10, FINSEQ_1:47;
reconsider c7 = c5 as FinSequence by E10;
consider c8 being FinSequence such that
E12: ( ( c8 in c1 & c7 = <*0*> ^ c8 ) or ( c8 in c2 & c7 = <*1*> ^ c8 ) ) by E10, TREES_3:71;
( c7 . 1 = 0 or c7 . 1 = 1 ) by E12, FINSEQ_1:58;
then ( c7 = <*0*> or c7 = <*1*> ) by E11, FINSEQ_1:57;
then ( c7 = c3 ^ <*0*> or c7 = c3 ^ <*1*> ) by E6, FINSEQ_1:47;
hence c5 in {(c3 ^ <*0*>),(c3 ^ <*1*>)} by TARSKI:def 2;
end;
assume c5 in {(c3 ^ <*0*>),(c3 ^ <*1*>)} ;
then ( c5 = c3 ^ <*0*> or c5 = c3 ^ <*1*> ) by TARSKI:def 2;
hence c5 in succ c3 by E7, E8, E9;
end;
hence succ c3 = {(c3 ^ <*0*>),(c3 ^ <*1*>)} by TARSKI:2;
end;
hereby
let c5 be Element of c1;
assume E6: c3 = <*0*> ^ c5 ;
let c6 be FinSequence;
hereby
assume c6 in succ c5 ;
then c6 in { (c5 ^ <*b1*>) where B is Nat : c5 ^ <*b1*> in c1 } by TREES_2:def 5;
then consider c7 being Nat such that
E7: ( c6 = c5 ^ <*c7*> & c5 ^ <*c7*> in c1 ) ;
<*0*> ^ (c5 ^ <*c7*>) in tree c1,c2 by E7, TREES_3:72;
then (<*0*> ^ c5) ^ <*c7*> in tree c1,c2 by FINSEQ_1:45;
then c3 ^ <*c7*> in { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in tree c1,c2 } by E6;
then c3 ^ <*c7*> in succ c3 by TREES_2:def 5;
hence <*0*> ^ c6 in succ c3 by E6, E7, FINSEQ_1:45;
end;
set c7 = <*0*> ^ c6;
assume <*0*> ^ c6 in succ c3 ;
then <*0*> ^ c6 in { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in tree c1,c2 } by TREES_2:def 5;
then consider c8 being Nat such that
E7: ( <*0*> ^ c6 = c3 ^ <*c8*> & c3 ^ <*c8*> in tree c1,c2 ) ;
<*0*> ^ (c5 ^ <*c8*>) in tree c1,c2 by E6, E7, FINSEQ_1:45;
then c5 ^ <*c8*> in c1 by TREES_3:72;
then c5 ^ <*c8*> in { (c5 ^ <*b1*>) where B is Nat : c5 ^ <*b1*> in c1 } ;
then E8: c5 ^ <*c8*> in succ c5 by TREES_2:def 5;
<*0*> ^ c6 = <*0*> ^ (c5 ^ <*c8*>) by E6, E7, FINSEQ_1:45;
hence c6 in succ c5 by E8, FINSEQ_1:46;
end;
let c5 be Element of c2;
assume E6: c3 = <*1*> ^ c5 ;
let c6 be FinSequence;
hereby
assume c6 in succ c5 ;
then c6 in { (c5 ^ <*b1*>) where B is Nat : c5 ^ <*b1*> in c2 } by TREES_2:def 5;
then consider c7 being Nat such that
E7: ( c6 = c5 ^ <*c7*> & c5 ^ <*c7*> in c2 ) ;
<*1*> ^ (c5 ^ <*c7*>) in tree c1,c2 by E7, TREES_3:73;
then (<*1*> ^ c5) ^ <*c7*> in tree c1,c2 by FINSEQ_1:45;
then c3 ^ <*c7*> in { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in tree c1,c2 } by E6;
then c3 ^ <*c7*> in succ c3 by TREES_2:def 5;
hence <*1*> ^ c6 in succ c3 by E6, E7, FINSEQ_1:45;
end;
set c7 = <*1*> ^ c6;
assume <*1*> ^ c6 in succ c3 ;
then <*1*> ^ c6 in { (c3 ^ <*b1*>) where B is Nat : c3 ^ <*b1*> in tree c1,c2 } by TREES_2:def 5;
then consider c8 being Nat such that
E7: ( <*1*> ^ c6 = c3 ^ <*c8*> & c3 ^ <*c8*> in tree c1,c2 ) ;
<*1*> ^ (c5 ^ <*c8*>) in tree c1,c2 by E6, E7, FINSEQ_1:45;
then c5 ^ <*c8*> in c2 by TREES_3:73;
then c5 ^ <*c8*> in { (c5 ^ <*b1*>) where B is Nat : c5 ^ <*b1*> in c2 } ;
then E8: c5 ^ <*c8*> in succ c5 by TREES_2:def 5;
<*1*> ^ c6 = <*1*> ^ (c5 ^ <*c8*>) by E6, E7, FINSEQ_1:45;
hence c6 in succ c5 by E8, FINSEQ_1:46;
end;

theorem Th10: :: BINTREE1:10
for b1, b2 being Tree holds
( ( b1 is binary & b2 is binary ) iff tree b1,b2 is binary )
proof
let c1, c2 be Tree;
set c3 = tree c1,c2;
hereby
assume E7: ( c1 is binary & c2 is binary ) ;
now
let c4 be Element of tree c1,c2;
assume E8: not c4 in Leaves (tree c1,c2) ;
per cases not ( not c4 = {} & ( for b1 being FinSequence holds
( not ( b1 in c1 & c4 = <*0*> ^ b1 ) & not ( b1 in c2 & c4 = <*1*> ^ b1 ) ) ) ) by TREES_3:71;
suppose c4 = {} ;
hence succ c4 = {(c4 ^ <*0*>),(c4 ^ <*1*>)} by Th9;
end;
suppose not for b1 being FinSequence holds
( not ( b1 in c1 & c4 = <*0*> ^ b1 ) & not ( b1 in c2 & c4 = <*1*> ^ b1 ) ) ;
then consider c5 being FinSequence such that
E9: ( ( c5 in c1 & c4 = <*0*> ^ c5 ) or ( c5 in c2 & c4 = <*1*> ^ c5 ) ) ;
E10: now
assume E11: ( c5 in c1 & c4 = <*0*> ^ c5 ) ;
then reconsider c6 = c5 as Element of c1 ;
per cases not ( not c6 in Leaves c1 & c6 in Leaves c1 ) ;
suppose c6 in Leaves c1 ;
hence succ c4 = {(c4 ^ <*0*>),(c4 ^ <*1*>)} by E8, E11, Th8;
end;
suppose not c6 in Leaves c1 ;
then E12: succ c6 = {(c6 ^ <*0*>),(c6 ^ <*1*>)} by E7, Def2;
now
let c7 be set ;
hereby
assume E13: c7 in succ c4 ;
then c7 in { (c4 ^ <*b1*>) where B is Nat : c4 ^ <*b1*> in tree c1,c2 } by TREES_2:def 5;
then consider c8 being Nat such that
E14: ( c7 = c4 ^ <*c8*> & c4 ^ <*c8*> in tree c1,c2 ) ;
E15: c7 = <*0*> ^ (c6 ^ <*c8*>) by E11, E14, FINSEQ_1:45;
then reconsider c9 = c6 ^ <*c8*> as Element of c1 by E14, TREES_3:72;
c9 in succ c6 by E11, E13, E15, Th9;
then ( c9 = c6 ^ <*0*> or c9 = c6 ^ <*1*> ) by E12, TARSKI:def 2;
then ( c7 = c4 ^ <*0*> or c7 = c4 ^ <*1*> ) by E14, FINSEQ_1:46;
hence c7 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} by TARSKI:def 2;
end;
assume c7 in {(c4 ^ <*0*>),(c4 ^ <*1*>)} ;
then ( c7 = (<*0*> ^ c6) ^ <*0*> or c7 = (<*0*> ^ c6) ^ <*1*> ) by E11, TARSKI:def 2;
then E13: ( c7 = <*0*> ^ (c6 ^ <*0*>) or c7 = <*0*> ^ (c6 ^ <*1*>) ) by FINSEQ_1:45;
( c6 ^ <*0*> in succ c6 & c6 ^ <*1*> in succ c6 ) by E12, TARSKI:def 2;
hence c7 in succ c4 by E11, E13, Th9;
end;
hence succ c4 = {(c4 ^ <*0*>),(c4 ^ <*1*>)} by TARSKI:2;
end;
end;
end; <