let T0, T1 be Tree; :: thesis: for t being Element of tree (T0,T1) holds

( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

let t be Element of tree (T0,T1); :: thesis: ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

set RT = tree (T0,T1);

( sp in succ p iff <*1*> ^ sp in succ t ) )

assume A14: t = <*1*> ^ p ; :: thesis: for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t )

let sp be FinSequence; :: thesis: ( sp in succ p iff <*1*> ^ sp in succ t )

assume <*1*> ^ sp in succ t ; :: thesis: sp in succ p

then <*1*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;

then consider n being Nat such that

A17: <*1*> ^ sp = t ^ <*n*> and

A18: t ^ <*n*> in tree (T0,T1) ;

<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A14, A18, FINSEQ_1:32;

then p ^ <*n*> in T1 by TREES_3:70;

then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T1 } ;

then A19: p ^ <*n*> in succ p by TREES_2:def 5;

<*1*> ^ sp = <*1*> ^ (p ^ <*n*>) by A14, A17, FINSEQ_1:32;

hence sp in succ p by A19, FINSEQ_1:33; :: thesis: verum

( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

let t be Element of tree (T0,T1); :: thesis: ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

set RT = tree (T0,T1);

hereby :: thesis: ( ( for p being Element of T0 st t = <*0*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

for sp being FinSequence holds

( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t ) ) )

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

( {} in T1 & <*1*> = <*1*> ^ {} ) by FINSEQ_1:34, TREES_1:22;

then <*1*> in tree (T0,T1) by TREES_3:68;

then A2: t ^ <*1*> in tree (T0,T1) by A1, FINSEQ_1:34;

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

( {} in T0 & <*0*> = <*0*> ^ {} ) by FINSEQ_1:34, TREES_1:22;

then <*0*> in tree (T0,T1) by TREES_3:68;

then A4: t ^ <*0*> in tree (T0,T1) by A1, FINSEQ_1:34;

end;( {} in T1 & <*1*> = <*1*> ^ {} ) by FINSEQ_1:34, TREES_1:22;

then <*1*> in tree (T0,T1) by TREES_3:68;

then A2: t ^ <*1*> in tree (T0,T1) by A1, FINSEQ_1:34;

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

( {} in T0 & <*0*> = <*0*> ^ {} ) by FINSEQ_1:34, TREES_1:22;

then <*0*> in tree (T0,T1) by TREES_3:68;

then A4: t ^ <*0*> in tree (T0,T1) by A1, FINSEQ_1:34;

now :: thesis: for x1 being object holds

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

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

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

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

hence x1 in succ t by A3, A4, A2; :: thesis: verum

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

assume
x1 in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: x1 in succ tassume
x1 in succ t
; :: thesis: x1 in {(t ^ <*0*>),(t ^ <*1*>)}

then consider n being Nat such that

A5: x1 = t ^ <*n*> and

A6: t ^ <*n*> in tree (T0,T1) by A3;

reconsider x = x1 as FinSequence by A5;

ex p being FinSequence st

( ( p in T0 & x = <*0*> ^ p ) or ( p in T1 & x = <*1*> ^ p ) ) by A5, A6, TREES_3:68;

then A7: ( x . 1 = 0 or x . 1 = 1 ) by FINSEQ_1:41;

x1 = <*n*> by A1, A5, FINSEQ_1:34;

then ( x = <*0*> or x = <*1*> ) by A7, FINSEQ_1:40;

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

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

end;then consider n being Nat such that

A5: x1 = t ^ <*n*> and

A6: t ^ <*n*> in tree (T0,T1) by A3;

reconsider x = x1 as FinSequence by A5;

ex p being FinSequence st

( ( p in T0 & x = <*0*> ^ p ) or ( p in T1 & x = <*1*> ^ p ) ) by A5, A6, TREES_3:68;

then A7: ( x . 1 = 0 or x . 1 = 1 ) by FINSEQ_1:41;

x1 = <*n*> by A1, A5, FINSEQ_1:34;

then ( x = <*0*> or x = <*1*> ) by A7, FINSEQ_1:40;

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

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

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

hence x1 in succ t by A3, A4, A2; :: thesis: verum

hereby :: thesis: for p being Element of T1 st t = <*1*> ^ p holds

for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t )

let p be Element of T1; :: thesis: ( t = <*1*> ^ p implies for sp being FinSequence holds for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t )

let p be Element of T0; :: thesis: ( t = <*0*> ^ p implies for sp being FinSequence holds

( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) )

assume A8: t = <*0*> ^ p ; :: thesis: for sp being FinSequence holds

( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )

let sp be FinSequence; :: thesis: ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )

assume <*0*> ^ sp in succ t ; :: thesis: sp in succ p

then <*0*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;

then consider n being Nat such that

A11: <*0*> ^ sp = t ^ <*n*> and

A12: t ^ <*n*> in tree (T0,T1) ;

<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, A12, FINSEQ_1:32;

then p ^ <*n*> in T0 by TREES_3:69;

then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T0 } ;

then A13: p ^ <*n*> in succ p by TREES_2:def 5;

<*0*> ^ sp = <*0*> ^ (p ^ <*n*>) by A8, A11, FINSEQ_1:32;

hence sp in succ p by A13, FINSEQ_1:33; :: thesis: verum

end;( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) )

assume A8: t = <*0*> ^ p ; :: thesis: for sp being FinSequence holds

( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )

let sp be FinSequence; :: thesis: ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )

hereby :: thesis: ( <*0*> ^ sp in succ t implies sp in succ p )

set zsp = <*0*> ^ sp;assume
sp in succ p
; :: thesis: <*0*> ^ sp in succ t

then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T0 } by TREES_2:def 5;

then consider n being Nat such that

A9: sp = p ^ <*n*> and

A10: p ^ <*n*> in T0 ;

<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A10, TREES_3:69;

then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;

then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A8;

then t ^ <*n*> in succ t by TREES_2:def 5;

hence <*0*> ^ sp in succ t by A8, A9, FINSEQ_1:32; :: thesis: verum

end;then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T0 } by TREES_2:def 5;

then consider n being Nat such that

A9: sp = p ^ <*n*> and

A10: p ^ <*n*> in T0 ;

<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A10, TREES_3:69;

then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;

then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A8;

then t ^ <*n*> in succ t by TREES_2:def 5;

hence <*0*> ^ sp in succ t by A8, A9, FINSEQ_1:32; :: thesis: verum

assume <*0*> ^ sp in succ t ; :: thesis: sp in succ p

then <*0*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;

then consider n being Nat such that

A11: <*0*> ^ sp = t ^ <*n*> and

A12: t ^ <*n*> in tree (T0,T1) ;

<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, A12, FINSEQ_1:32;

then p ^ <*n*> in T0 by TREES_3:69;

then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T0 } ;

then A13: p ^ <*n*> in succ p by TREES_2:def 5;

<*0*> ^ sp = <*0*> ^ (p ^ <*n*>) by A8, A11, FINSEQ_1:32;

hence sp in succ p by A13, FINSEQ_1:33; :: thesis: verum

( sp in succ p iff <*1*> ^ sp in succ t ) )

assume A14: t = <*1*> ^ p ; :: thesis: for sp being FinSequence holds

( sp in succ p iff <*1*> ^ sp in succ t )

let sp be FinSequence; :: thesis: ( sp in succ p iff <*1*> ^ sp in succ t )

hereby :: thesis: ( <*1*> ^ sp in succ t implies sp in succ p )

set zsp = <*1*> ^ sp;assume
sp in succ p
; :: thesis: <*1*> ^ sp in succ t

then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T1 } by TREES_2:def 5;

then consider n being Nat such that

A15: sp = p ^ <*n*> and

A16: p ^ <*n*> in T1 ;

<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A16, TREES_3:70;

then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;

then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A14;

then t ^ <*n*> in succ t by TREES_2:def 5;

hence <*1*> ^ sp in succ t by A14, A15, FINSEQ_1:32; :: thesis: verum

end;then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T1 } by TREES_2:def 5;

then consider n being Nat such that

A15: sp = p ^ <*n*> and

A16: p ^ <*n*> in T1 ;

<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A16, TREES_3:70;

then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;

then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A14;

then t ^ <*n*> in succ t by TREES_2:def 5;

hence <*1*> ^ sp in succ t by A14, A15, FINSEQ_1:32; :: thesis: verum

assume <*1*> ^ sp in succ t ; :: thesis: sp in succ p

then <*1*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;

then consider n being Nat such that

A17: <*1*> ^ sp = t ^ <*n*> and

A18: t ^ <*n*> in tree (T0,T1) ;

<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A14, A18, FINSEQ_1:32;

then p ^ <*n*> in T1 by TREES_3:70;

then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T1 } ;

then A19: p ^ <*n*> in succ p by TREES_2:def 5;

<*1*> ^ sp = <*1*> ^ (p ^ <*n*>) by A14, A17, FINSEQ_1:32;

hence sp in succ p by A19, FINSEQ_1:33; :: thesis: verum