let T1, T2 be Tree; :: thesis: ( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary )
set RT = tree (T1,T2);
hereby :: thesis: ( tree (T1,T2) is binary implies ( T1 is binary & T2 is binary ) )
assume that
A1: T1 is binary and
A2: T2 is binary ; :: thesis: tree (T1,T2) is binary
now :: thesis: for t being Element of tree (T1,T2) st not t in Leaves (tree (T1,T2)) holds
succ t = {(),(t ^ <*1*>)}
let t be Element of tree (T1,T2); :: thesis: ( not t in Leaves (tree (T1,T2)) implies succ b1 = {(b1 ^ ),(b1 ^ <*1*>)} )
assume A3: not t in Leaves (tree (T1,T2)) ; :: thesis: succ b1 = {(b1 ^ ),(b1 ^ <*1*>)}
per cases ( t = {} or ex p being FinSequence st
( ( p in T1 & t = ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) )
by TREES_3:68;
suppose t = {} ; :: thesis: succ b1 = {(b1 ^ ),(b1 ^ <*1*>)}
hence succ t = {(),(t ^ <*1*>)} by Th7; :: thesis: verum
end;
suppose ex p being FinSequence st
( ( p in T1 & t = ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; :: thesis: succ b1 = {(b1 ^ ),(b1 ^ <*1*>)}
then consider p being FinSequence such that
A4: ( ( p in T1 & t = ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ;
A5: now :: thesis: ( p in T2 & t = <*1*> ^ p implies succ t = {(),(t ^ <*1*>)} )
assume that
A6: p in T2 and
A7: t = <*1*> ^ p ; :: thesis: succ t = {(),(t ^ <*1*>)}
reconsider p = p as Element of T2 by A6;
per cases ( p in Leaves T2 or not p in Leaves T2 ) ;
suppose p in Leaves T2 ; :: thesis: succ t = {(),(t ^ <*1*>)}
hence succ t = {(),(t ^ <*1*>)} by A3, A7, Th6; :: thesis: verum
end;
suppose not p in Leaves T2 ; :: thesis: succ t = {(),(t ^ <*1*>)}
then A8: succ p = {(),(p ^ <*1*>)} by A2;
now :: thesis: for x being object holds
( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
let x be object ; :: thesis: ( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
hereby :: thesis: ( x in {(),(t ^ <*1*>)} implies x in succ t )
assume A9: x in succ t ; :: thesis: x in {(),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
then consider n being Nat such that
A10: x = t ^ <*n*> and
A11: t ^ <*n*> in tree (T1,T2) ;
A12: x = <*1*> ^ (p ^ <*n*>) by ;
then reconsider pn = p ^ <*n*> as Element of T2 by ;
pn in succ p by A7, A9, A12, Th7;
then ( pn = p ^ or pn = p ^ <*1*> ) by ;
then ( x = t ^ or x = t ^ <*1*> ) by ;
hence x in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
assume x in {(),(t ^ <*1*>)} ; :: thesis: x in succ t
then ( x = (<*1*> ^ p) ^ or x = (<*1*> ^ p) ^ <*1*> ) by ;
then A13: ( x = <*1*> ^ () or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;
( p ^ in succ p & p ^ <*1*> in succ p ) by ;
hence x in succ t by A7, A13, Th7; :: thesis: verum
end;
hence succ t = {(),(t ^ <*1*>)} by TARSKI:2; :: thesis: verum
end;
end;
end;
now :: thesis: ( p in T1 & t = ^ p implies succ t = {(),(t ^ <*1*>)} )
assume that
A14: p in T1 and
A15: t = ^ p ; :: thesis: succ t = {(),(t ^ <*1*>)}
reconsider p = p as Element of T1 by A14;
per cases ( p in Leaves T1 or not p in Leaves T1 ) ;
suppose p in Leaves T1 ; :: thesis: succ t = {(),(t ^ <*1*>)}
hence succ t = {(),(t ^ <*1*>)} by A3, A15, Th6; :: thesis: verum
end;
suppose not p in Leaves T1 ; :: thesis: succ t = {(),(t ^ <*1*>)}
then A16: succ p = {(),(p ^ <*1*>)} by A1;
now :: thesis: for x being object holds
( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
let x be object ; :: thesis: ( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
hereby :: thesis: ( x in {(),(t ^ <*1*>)} implies x in succ t )
assume A17: x in succ t ; :: thesis: x in {(),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
then consider n being Nat such that
A18: x = t ^ <*n*> and
A19: t ^ <*n*> in tree (T1,T2) ;
A20: x = ^ (p ^ <*n*>) by ;
then reconsider pn = p ^ <*n*> as Element of T1 by ;
pn in succ p by A15, A17, A20, Th7;
then ( pn = p ^ or pn = p ^ <*1*> ) by ;
then ( x = t ^ or x = t ^ <*1*> ) by ;
hence x in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
assume x in {(),(t ^ <*1*>)} ; :: thesis: x in succ t
then ( x = () ^ or x = () ^ <*1*> ) by ;
then A21: ( x = ^ () or x = ^ (p ^ <*1*>) ) by FINSEQ_1:32;
( p ^ in succ p & p ^ <*1*> in succ p ) by ;
hence x in succ t by ; :: thesis: verum
end;
hence succ t = {(),(t ^ <*1*>)} by TARSKI:2; :: thesis: verum
end;
end;
end;
hence succ t = {(),(t ^ <*1*>)} by A4, A5; :: thesis: verum
end;
end;
end;
hence tree (T1,T2) is binary ; :: thesis: verum
end;
assume A22: tree (T1,T2) is binary ; :: thesis: ( T1 is binary & T2 is binary )
now :: thesis: for t being Element of T1 st not t in Leaves T1 holds
succ t = {(),(t ^ <*1*>)}
let t be Element of T1; :: thesis: ( not t in Leaves T1 implies succ t = {(),(t ^ <*1*>)} )
reconsider zt = ^ t as Element of tree (T1,T2) by TREES_3:69;
assume not t in Leaves T1 ; :: thesis: succ t = {(),(t ^ <*1*>)}
then not zt in Leaves (tree (T1,T2)) by Th6;
then A23: succ zt = {(() ^ ),(() ^ <*1*>)} by A22;
A24: succ zt = { (zt ^ <*n*>) where n is Nat : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
now :: thesis: for x being object holds
( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
let x be object ; :: thesis: ( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
hereby :: thesis: ( x in {(),(t ^ <*1*>)} implies x in succ t )
assume x in succ t ; :: thesis: x in {(),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T1 } by TREES_2:def 5;
then consider n being Nat such that
A25: x = t ^ <*n*> and
A26: t ^ <*n*> in T1 ;
<*0*> ^ (t ^ <*n*>) in tree (T1,T2) by ;
then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Nat : zt ^ <*k*> in tree (T1,T2) } ;
then ( zt ^ <*n*> = zt ^ or zt ^ <*n*> = zt ^ <*1*> ) by ;
then ( x = t ^ or x = t ^ <*1*> ) by ;
hence x in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
assume x in {(),(t ^ <*1*>)} ; :: thesis: x in succ t
then A27: ( x = t ^ or x = t ^ <*1*> ) by TARSKI:def 2;
(<*0*> ^ t) ^ <*1*> in succ zt by ;
then A28: <*0*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;
(<*0*> ^ t) ^ in succ zt by ;
then <*0*> ^ () in succ zt by FINSEQ_1:32;
hence x in succ t by ; :: thesis: verum
end;
hence succ t = {(),(t ^ <*1*>)} by TARSKI:2; :: thesis: verum
end;
hence T1 is binary ; :: thesis: T2 is binary
now :: thesis: for t being Element of T2 st not t in Leaves T2 holds
succ t = {(),(t ^ <*1*>)}
let t be Element of T2; :: thesis: ( not t in Leaves T2 implies succ t = {(),(t ^ <*1*>)} )
reconsider zt = <*1*> ^ t as Element of tree (T1,T2) by TREES_3:70;
assume not t in Leaves T2 ; :: thesis: succ t = {(),(t ^ <*1*>)}
then not zt in Leaves (tree (T1,T2)) by Th6;
then A29: succ zt = {((<*1*> ^ t) ^ ),((<*1*> ^ t) ^ <*1*>)} by A22;
A30: succ zt = { (zt ^ <*n*>) where n is Nat : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
now :: thesis: for x being object holds
( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
let x be object ; :: thesis: ( ( x in succ t implies x in {(),(t ^ <*1*>)} ) & ( x in {(),(t ^ <*1*>)} implies x in succ t ) )
hereby :: thesis: ( x in {(),(t ^ <*1*>)} implies x in succ t )
assume x in succ t ; :: thesis: x in {(),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T2 } by TREES_2:def 5;
then consider n being Nat such that
A31: x = t ^ <*n*> and
A32: t ^ <*n*> in T2 ;
<*1*> ^ (t ^ <*n*>) in tree (T1,T2) by ;
then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Nat : zt ^ <*k*> in tree (T1,T2) } ;
then ( zt ^ <*n*> = zt ^ or zt ^ <*n*> = zt ^ <*1*> ) by ;
then ( x = t ^ or x = t ^ <*1*> ) by ;
hence x in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
assume x in {(),(t ^ <*1*>)} ; :: thesis: x in succ t
then A33: ( x = t ^ or x = t ^ <*1*> ) by TARSKI:def 2;
(<*1*> ^ t) ^ <*1*> in succ zt by ;
then A34: <*1*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;
(<*1*> ^ t) ^ in succ zt by ;
then <*1*> ^ () in succ zt by FINSEQ_1:32;
hence x in succ t by ; :: thesis: verum
end;
hence succ t = {(),(t ^ <*1*>)} by TARSKI:2; :: thesis: verum
end;
hence T2 is binary ; :: thesis: verum