let A, B be MP-wff; :: thesis: (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B is MP-wff
set y = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A;
set x = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B;
A1: <*0 *> in dom ((elementary_tree 2) --> [2,0 ])

proof

<*0 *> in elementary_tree 2 by TREES_1:55;
hence <*0 *> in dom ((elementary_tree 2) --> [2,0 ]) by FUNCOP_1:19; :: thesis: verum

end;

((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A is DecoratedTree of

proof

@ ((elementary_tree 2) --> [2,0 ]),<*0 *>,A = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A by A1, Def8;
hence ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A is DecoratedTree of ; :: thesis: verum

end;

then reconsider y = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A as DecoratedTree of ;
A2: dom y = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A) by A1, TREES_2:def 12;
A3: <*1*> in elementary_tree 2 by TREES_1:55;
A4: dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 by FUNCOP_1:19;
A5: <*1*> in dom ((elementary_tree 2) --> [2,0 ]) by A3, FUNCOP_1:19;
A6: not <*0 *> is_a_proper_prefix_of <*1*>

proof

assume <*0 *> is_a_proper_prefix_of <*1*> ; :: thesis: contradiction
then <*0 *> is_a_prefix_of <*1*> by XBOOLE_0:def 8;
hence contradiction by TREES_1:16; :: thesis: verum

end;

then A7: <*1*> in dom y by A1, A2, A5, TREES_1:def 12;
reconsider da = dom A as finite Tree ;
reconsider d = <*0 *> as Element of elementary_tree 2 by A1, FUNCOP_1:19;
dom y = (elementary_tree 2) with-replacement d,da by A4, TREES_2:def 12;
then reconsider dy = dom y as finite Tree ;
reconsider d1 = <*1*> as Element of dy by A1, A2, A5, A6, TREES_1:def 12;
reconsider db = dom B as finite Tree ;
A8: dom ((((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B) = dy with-replacement d1,db by TREES_2:def 12;
@ y,<*1*>,B = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B by A7, Def8;
then reconsider x = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B as finite DecoratedTree of by A8, Lm2;
A9: dom x = (dom y) with-replacement <*1*>,(dom B) by A7, TREES_2:def 12;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

proof

let v be Element of dom x; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
set e = (elementary_tree 2) --> [2,0 ];

now

per cases ( ( not <*1*> is_a_prefix_of v & x . v = y . v ) or ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ) by A7, A9, TREES_2:def 12;

suppose A10: ( not <*1*> is_a_prefix_of v & x . v = y . v ) ; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

then A11: for s being FinSequence of NAT holds
( not s in dom B or not v = <*1*> ^ s ) by TREES_1:8;
then A12: v in (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A) by A2, A7, A9, TREES_1:def 12;

now

per cases ( ( not <*0 *> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0 ]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0 *> ^ s & y . v = A . s ) ) by A1, A12, TREES_2:def 12;

suppose A13: ( not <*0 *> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0 ]) . v ) ; :: thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

then A14: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0 *> ^ s ) by TREES_1:8;
then A15: ( v in dom ((elementary_tree 2) --> [2,0 ]) & not <*0 *> is_a_proper_prefix_of v ) by A1, A12, TREES_1:def 12;
reconsider v' = v as Element of dom ((elementary_tree 2) --> [2,0 ]) by A1, A12, A14, TREES_1:def 12;
A16: dom ((elementary_tree 2) --> [2,0 ]) = {{} ,<*0 *>,<*1*>} by FUNCOP_1:19, TREES_1:90;
then A17: v = {} by A10, A13, A15, ENUMSET1:def 1;
A18: succ v' = {<*0 *>,<*1*>}

proof

now

let x be set ; :: thesis: ( ( x in succ v' implies x in {<*0 *>,<*1*>} ) & ( x in {<*0 *>,<*1*>} implies x in succ v' ) )
thus ( x in succ v' implies x in {<*0 *>,<*1*>} ) :: thesis: ( x in {<*0 *>,<*1*>} implies x in succ v' )

proof

assume x in succ v' ; :: thesis: x in {<*0 *>,<*1*>}
then x in { (v' ^ <*n*>) where n is Element of NAT : v' ^ <*n*> in dom ((elementary_tree 2) --> [2,0 ]) } by TREES_2:def 5;
then consider n being Element of NAT such that
A19: ( x = v' ^ <*n*> & v' ^ <*n*> in dom ((elementary_tree 2) --> [2,0 ]) ) ;
A20: ( x = <*n*> & <*n*> in dom ((elementary_tree 2) --> [2,0 ]) ) by A17, A19, FINSEQ_1:47;
then ( <*n*> = {} or <*n*> = <*0 *> or <*n*> = <*1*> ) by A16, ENUMSET1:def 1;
hence x in {<*0 *>,<*1*>} by A20, TARSKI:def 2; :: thesis: verum

end;

assume x in {<*0 *>,<*1*>} ; :: thesis: x in succ v'
then A21: ( x = <*0 *> or x = <*1*> ) by TARSKI:def 2;

now

per cases ( x = v' ^ <*0 *> or x = v' ^ <*1*> ) by A17, A21, FINSEQ_1:47;

suppose A22: x = v' ^ <*0 *> ; :: thesis: x in succ v'

then v' ^ <*0 *> in dom ((elementary_tree 2) --> [2,0 ]) by A16, A21, ENUMSET1:def 1;
then x in { (v' ^ <*n*>) where n is Element of NAT : v' ^ <*n*> in dom ((elementary_tree 2) --> [2,0 ]) } by A22;
hence x in succ v' by TREES_2:def 5; :: thesis: verum

end;

suppose A23: x = v' ^ <*1*> ; :: thesis: x in succ v'

then v' ^ <*1*> in dom ((elementary_tree 2) --> [2,0 ]) by A16, A21, ENUMSET1:def 1;
then x in { (v' ^ <*n*>) where n is Element of NAT : v' ^ <*n*> in dom ((elementary_tree 2) --> [2,0 ]) } by A23;
hence x in succ v' by TREES_2:def 5; :: thesis: verum

end;

end;

end;

hence x in succ v' ; :: thesis: verum

end;

hence succ v' = {<*0 *>,<*1*>} by TARSKI:2; :: thesis: verum

end;

A24: succ v = succ v'

proof

reconsider v'' = v as Element of dom y by A7, A9, A11, TREES_1:def 12;
succ v'' = succ v' by A1, A2, A17, Lm1, Th17;
hence succ v = succ v' by A7, A9, A17, Lm1, Th17; :: thesis: verum

end;

<*0 *> <> <*1*> by TREES_1:16;
then A25: 2 = card (succ v) by A18, A24, CARD_2:76;
hence branchdeg v <= 2 by TREES_2:def 13; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
x . v = [2,0 ]

proof

v in elementary_tree 2 by A15, FUNCOP_1:19;
hence x . v = [2,0 ] by A10, A13, FUNCOP_1:13; :: thesis: verum

end;

hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) by A25, TREES_2:def 13; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0 *> ^ s & y . v = A . s ) ; :: thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

then consider s being FinSequence of NAT such that
A26: ( s in dom A & v = <*0 *> ^ s & y . v = A . s ) ;
reconsider s = s as Element of dom A by A26;
A27: ( branchdeg s <= 2 & ( not branchdeg s = 0 or A . s = [0 ,0 ] or ex m being Element of NAT st A . s = [3,m] ) & ( not branchdeg s = 1 or A . s = [1,0 ] or A . s = [1,1] ) & ( branchdeg s = 2 implies A . s = [2,0 ] ) ) by Def6;
succ v, succ s are_equipotent

proof

reconsider v' = v as Element of dom y by A7, A9, A11, TREES_1:def 12;
succ v', succ s are_equipotent by A1, A2, A26, TREES_2:39;
hence succ v, succ s are_equipotent by A7, A9, A26, Th3, Th18; :: thesis: verum

end;

then card (succ v) = card (succ s) by CARD_1:21;
then A28: branchdeg v = card (succ s) by TREES_2:def 13;
hence branchdeg v <= 2 by A27, TREES_2:def 13; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
thus ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) by A10, A26, A27, A28, TREES_2:def 13; :: thesis: verum

end;

end;

end;

hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

then consider s being FinSequence of NAT such that
A29: ( s in dom B & v = <*1*> ^ s & x . v = B . s ) ;
reconsider s = s as Element of dom B by A29;
A30: ( branchdeg s <= 2 & ( not branchdeg s = 0 or B . s = [0 ,0 ] or ex m being Element of NAT st B . s = [3,m] ) & ( not branchdeg s = 1 or B . s = [1,0 ] or B . s = [1,1] ) & ( branchdeg s = 2 implies B . s = [2,0 ] ) ) by Def6;
succ v, succ s are_equipotent by A7, A9, A29, TREES_2:39;
then card (succ v) = card (succ s) by CARD_1:21;
then branchdeg v = card (succ s) by TREES_2:def 13;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) by A29, A30, TREES_2:def 13; :: thesis: verum

end;

end;

end;

hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ; :: thesis: verum

end;

hence (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) with-replacement <*1*>,B is MP-wff by Def6; :: thesis: verum