let T1, T2 be Tree; :: thesis: ( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary )

set RT = tree (T1,T2);

set RT = tree (T1,T2);

hereby :: thesis: ( tree (T1,T2) is binary implies ( T1 is binary & T2 is binary ) )

assume A22:
tree (T1,T2) is binary
; :: thesis: ( T1 is binary & T2 is binary )assume that

A1: T1 is binary and

A2: T2 is binary ; :: thesis: tree (T1,T2) is binary

end;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 ^ <*0*>),(t ^ <*1*>)}

hence
tree (T1,T2) is binary
; :: thesis: verumsucc t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of tree (T1,T2); :: thesis: ( not t in Leaves (tree (T1,T2)) implies succ b_{1} = {(b_{1} ^ <*0*>),(b_{1} ^ <*1*>)} )

assume A3: not t in Leaves (tree (T1,T2)) ; :: thesis: succ b_{1} = {(b_{1} ^ <*0*>),(b_{1} ^ <*1*>)}

end;assume A3: not t in Leaves (tree (T1,T2)) ; :: thesis: succ b

per cases
( t = {} or ex p being FinSequence st

( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ) by TREES_3:68;

end;

( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ) by TREES_3:68;

suppose
ex p being FinSequence st

( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; :: thesis: succ b_{1} = {(b_{1} ^ <*0*>),(b_{1} ^ <*1*>)}

( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; :: thesis: succ b

then consider p being FinSequence such that

A4: ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ;

end;A4: ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ;

A5: now :: thesis: ( p in T2 & t = <*1*> ^ p implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

assume that

A6: p in T2 and

A7: t = <*1*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

reconsider p = p as Element of T2 by A6;

end;A6: p in T2 and

A7: t = <*1*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

reconsider p = p as Element of T2 by A6;

per cases
( p in Leaves T2 or not p in Leaves T2 )
;

end;

suppose
not p in Leaves T2
; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then A8:
succ p = {(p ^ <*0*>),(p ^ <*1*>)}
by A2;

end;now :: thesis: for x being object holds

( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TARSKI:2; :: thesis: verum( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

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

then A13: ( x = <*1*> ^ (p ^ <*0*>) or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;

( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A8, TARSKI:def 2;

hence x in succ t by A7, A13, Th7; :: thesis: verum

end;hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume
x in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: x in succ tassume A9:
x in succ t
; :: thesis: x in {(t ^ <*0*>),(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 A7, A10, FINSEQ_1:32;

then reconsider pn = p ^ <*n*> as Element of T2 by A10, A11, TREES_3:70;

pn in succ p by A7, A9, A12, Th7;

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

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A10, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;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 A7, A10, FINSEQ_1:32;

then reconsider pn = p ^ <*n*> as Element of T2 by A10, A11, TREES_3:70;

pn in succ p by A7, A9, A12, Th7;

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

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A10, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

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

then A13: ( x = <*1*> ^ (p ^ <*0*>) or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;

( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A8, TARSKI:def 2;

hence x in succ t by A7, A13, Th7; :: thesis: verum

now :: thesis: ( p in T1 & t = <*0*> ^ p implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by A4, A5; :: thesis: verumassume that

A14: p in T1 and

A15: t = <*0*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

reconsider p = p as Element of T1 by A14;

end;A14: p in T1 and

A15: t = <*0*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

reconsider p = p as Element of T1 by A14;

per cases
( p in Leaves T1 or not p in Leaves T1 )
;

end;

suppose
not p in Leaves T1
; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then A16:
succ p = {(p ^ <*0*>),(p ^ <*1*>)}
by A1;

end;now :: thesis: for x being object holds

( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TARSKI:2; :: thesis: verum( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

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

then A21: ( x = <*0*> ^ (p ^ <*0*>) or x = <*0*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;

( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A16, TARSKI:def 2;

hence x in succ t by A15, A21, Th7; :: thesis: verum

end;hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume
x in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: x in succ tassume A17:
x in succ t
; :: thesis: x in {(t ^ <*0*>),(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 = <*0*> ^ (p ^ <*n*>) by A15, A18, FINSEQ_1:32;

then reconsider pn = p ^ <*n*> as Element of T1 by A18, A19, TREES_3:69;

pn in succ p by A15, A17, A20, Th7;

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

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A18, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;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 = <*0*> ^ (p ^ <*n*>) by A15, A18, FINSEQ_1:32;

then reconsider pn = p ^ <*n*> as Element of T1 by A18, A19, TREES_3:69;

pn in succ p by A15, A17, A20, Th7;

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

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A18, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

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

then A21: ( x = <*0*> ^ (p ^ <*0*>) or x = <*0*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;

( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A16, TARSKI:def 2;

hence x in succ t by A15, A21, Th7; :: thesis: verum

now :: thesis: for t being Element of T1 st not t in Leaves T1 holds

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

hence
T1 is binary
; :: thesis: T2 is binary succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of T1; :: thesis: ( not t in Leaves T1 implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

reconsider zt = <*0*> ^ t as Element of tree (T1,T2) by TREES_3:69;

assume not t in Leaves T1 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then not zt in Leaves (tree (T1,T2)) by Th6;

then A23: succ zt = {((<*0*> ^ t) ^ <*0*>),((<*0*> ^ t) ^ <*1*>)} by A22;

A24: succ zt = { (zt ^ <*n*>) where n is Nat : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;

end;reconsider zt = <*0*> ^ t as Element of tree (T1,T2) by TREES_3:69;

assume not t in Leaves T1 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then not zt in Leaves (tree (T1,T2)) by Th6;

then A23: succ zt = {((<*0*> ^ t) ^ <*0*>),((<*0*> ^ t) ^ <*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 ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TARSKI:2; :: thesis: verum( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

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

(<*0*> ^ t) ^ <*1*> in succ zt by A23, TARSKI:def 2;

then A28: <*0*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;

(<*0*> ^ t) ^ <*0*> in succ zt by A23, TARSKI:def 2;

then <*0*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;

hence x in succ t by A27, A28, Th7; :: thesis: verum

end;hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume
x in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: x in succ tassume
x in succ t
; :: thesis: x in {(t ^ <*0*>),(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 A26, TREES_3:69;

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 ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A23, A24, TARSKI:def 2;

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A25, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;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 A26, TREES_3:69;

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 ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A23, A24, TARSKI:def 2;

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A25, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

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

(<*0*> ^ t) ^ <*1*> in succ zt by A23, TARSKI:def 2;

then A28: <*0*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;

(<*0*> ^ t) ^ <*0*> in succ zt by A23, TARSKI:def 2;

then <*0*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;

hence x in succ t by A27, A28, Th7; :: thesis: verum

now :: thesis: for t being Element of T2 st not t in Leaves T2 holds

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

hence
T2 is binary
; :: thesis: verumsucc t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of T2; :: thesis: ( not t in Leaves T2 implies succ t = {(t ^ <*0*>),(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 ^ <*0*>),(t ^ <*1*>)}

then not zt in Leaves (tree (T1,T2)) by Th6;

then A29: succ zt = {((<*1*> ^ t) ^ <*0*>),((<*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;

end;reconsider zt = <*1*> ^ t as Element of tree (T1,T2) by TREES_3:70;

assume not t in Leaves T2 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then not zt in Leaves (tree (T1,T2)) by Th6;

then A29: succ zt = {((<*1*> ^ t) ^ <*0*>),((<*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 ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TARSKI:2; :: thesis: verum( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

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

(<*1*> ^ t) ^ <*1*> in succ zt by A29, TARSKI:def 2;

then A34: <*1*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;

(<*1*> ^ t) ^ <*0*> in succ zt by A29, TARSKI:def 2;

then <*1*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;

hence x in succ t by A33, A34, Th7; :: thesis: verum

end;hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume
x in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: x in succ tassume
x in succ t
; :: thesis: x in {(t ^ <*0*>),(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 A32, TREES_3:70;

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 ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A29, A30, TARSKI:def 2;

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A31, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;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 A32, TREES_3:70;

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 ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A29, A30, TARSKI:def 2;

then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A31, FINSEQ_1:33;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

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

(<*1*> ^ t) ^ <*1*> in succ zt by A29, TARSKI:def 2;

then A34: <*1*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;

(<*1*> ^ t) ^ <*0*> in succ zt by A29, TARSKI:def 2;

then <*1*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;

hence x in succ t by A33, A34, Th7; :: thesis: verum