set e = elementary_tree 2;
let Z be Tree; :: thesis: for x1, x2 being Element of Z st x1 = <*0*> & x2 = <*1*> & succ (Root Z) = {x1,x2} holds
Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
let x1, x2 be Element of Z; :: thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root Z) = {x1,x2} implies Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) )
assume that
A1: x1 = <*0*> and
A2: x2 = <*1*> and
A3: succ (Root Z) = {x1,x2} ; :: thesis: Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
set T1 = (elementary_tree 2) with-replacement (<*0*>,(Z | x1));
A4: <*0*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
A5: now :: thesis: for s being FinSequence of NAT holds
( ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) & ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) )
let s be FinSequence of NAT ; :: thesis: ( ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) & ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) )
thus ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) :: thesis: ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z )
proof
assume A6: s in Z ; :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
per cases ( s = {} or s <> {} ) ;
suppose s = {} ; :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by TREES_1:22; :: thesis: verum
end;
suppose s <> {} ; :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then consider w being FinSequence of NAT , n being Element of NAT such that
A7: s = <*n*> ^ w by FINSEQ_2:130;
<*n*> is_a_prefix_of s by A7, TREES_1:1;
then A8: <*n*> in Z by A6, TREES_1:20;
<*n*> = (Root Z) ^ <*n*> by FINSEQ_1:34;
then A9: <*n*> in succ (Root Z) by A8, TREES_2:12;
now :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
per cases ( <*n*> = <*0*> or <*n*> = <*1*> ) by A1, A2, A3, A9, TARSKI:def 2;
suppose A10: <*n*> = <*0*> ; :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then w in Z | x1 by A1, A6, A7, TREES_1:def 6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A4, A7, A10, Th2, TREES_1:def 9; :: thesis: verum
end;
suppose A11: <*n*> = <*1*> ; :: thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then w in Z | x2 by A2, A6, A7, TREES_1:def 6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A7, A11; :: thesis: verum
end;
end;
end;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis: verum
end;
end;
end;
assume A12: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis: s in Z
now :: thesis: s in Z
per cases ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A12;
suppose ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ; :: thesis: s in Z
hence s in Z by A2, TREES_1:def 6; :: thesis: verum
end;
end;
end;
hence s in Z ; :: thesis: verum
end;
A14: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:3;
<*1*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
then <*1*> in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) by A4, A14, TREES_1:def 9;
hence Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A5, TREES_1:def 9; :: thesis: verum