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

proof

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

end;

then A2: dom (((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement <*0 *>,(dom A) by TREES_2:def 12;
reconsider d = <*0 *> as Element of elementary_tree 1 by TREES_1:55;
A3: dom (((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,A) = (elementary_tree 1) with-replacement d,(dom A) by A2, FUNCOP_1:19;
@ ((elementary_tree 1) --> [1,1]),<*0 *>,A = ((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,A by A1, Def8;
then reconsider x = ((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,A as finite DecoratedTree of by A3, Lm2;
A4: dom x = (dom ((elementary_tree 1) --> [1,1])) with-replacement <*0 *>,(dom A) by A1, 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 1) --> [1,1];

now

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

suppose A5: ( not <*0 *> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . 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 A6: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0 *> ^ s ) by TREES_1:8;
then A7: ( v in dom ((elementary_tree 1) --> [1,1]) & not <*0 *> is_a_proper_prefix_of v ) by A1, A4, TREES_1:def 12;
reconsider v' = v as Element of dom ((elementary_tree 1) --> [1,1]) by A1, A4, A6, TREES_1:def 12;
A8: dom ((elementary_tree 1) --> [1,1]) = {{} ,<*0 *>} by FUNCOP_1:19, TREES_1:88;
then A9: v = {} by A5, A7, TARSKI:def 2;
A10: succ v' = {<*0 *>}

proof

now

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

proof

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

end;

assume x in {<*0 *>} ; :: thesis: x in succ v'
then A13: x = <*0 *> by TARSKI:def 1;
then A14: x = v' ^ <*0 *> by A9, FINSEQ_1:47;
then v' ^ <*0 *> in dom ((elementary_tree 1) --> [1,1]) by A8, A13, TARSKI:def 2;
then x in { (v' ^ <*n*>) where n is Element of NAT : v' ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by A14;
hence x in succ v' by TREES_2:def 5; :: thesis: verum

end;

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

end;

succ v = succ v' by A1, A4, A9, Lm1, Th17;
then 1 = card (succ v) by A10, CARD_1:50;
then A15: branchdeg v = 1 by TREES_2:def 13;
hence branchdeg v <= 2 ; :: 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 = [1,1]

proof

v in elementary_tree 1 by A7, FUNCOP_1:19;
hence x . v = [1,1] by A5, 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 A15; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0 *> ^ s & x . 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
A16: ( s in dom A & v = <*0 *> ^ s & x . v = A . s ) ;
reconsider s = s as Element of dom A by A16;
A17: ( 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 by A1, A4, A16, TREES_2:39;
then card (succ v) = card (succ s) by CARD_1:21;
then A18: branchdeg v = card (succ s) by TREES_2:def 13;
hence branchdeg v <= 2 by A17, 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 A16, A17, A18, 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 1) --> [1,1]) with-replacement <*0 *>,A is MP-wff by Def6; :: thesis: verum