let A, B be MP-wff; (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
reconsider d = <*0*> as Element of elementary_tree 2 by TREES_1:28;
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:
not <*0*> is_a_proper_prefix_of <*1*>
by TREES_1:3;
reconsider db = dom B as finite Tree ;
reconsider da = dom A as finite Tree ;
<*0*> in elementary_tree 2
by TREES_1:28;
then A2:
<*0*> in dom ((elementary_tree 2) --> [2,0])
by FUNCOP_1:13;
then
@ (((elementary_tree 2) --> [2,0]),<*0*>,A) = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)
by Def7;
then reconsider y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) as DecoratedTree of [:NAT,NAT:] ;
A3:
dom y = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A))
by A2, TREES_2:def 11;
dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2
by FUNCOP_1:13;
then
dom y = (elementary_tree 2) with-replacement (d,da)
by TREES_2:def 11;
then reconsider dy = dom y as finite Tree ;
<*1*> in elementary_tree 2
by TREES_1:28;
then A4:
<*1*> in dom ((elementary_tree 2) --> [2,0])
by FUNCOP_1:13;
then A5:
<*1*> in dom y
by A2, A3, A1, TREES_1:def 9;
reconsider d1 = <*1*> as Element of dy by A2, A3, A4, A1, TREES_1:def 9;
( dom ((((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B)) = dy with-replacement (d1,db) & @ (y,<*1*>,B) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) )
by A5, Def7, TREES_2:def 11;
then reconsider x = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) as finite DecoratedTree of [:NAT,NAT:] by Lm2;
A6:
dom x = (dom y) with-replacement (<*1*>,(dom B))
by A5, TREES_2:def 11;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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
set e =
(elementary_tree 2) --> [2,0];
let v be
Element of
dom x;
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )
now ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )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 A5, A6, TREES_2:def 11;
suppose A7:
( not
<*1*> is_a_prefix_of v &
x . v = y . v )
;
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 A8:
for
s being
FinSequence of
NAT holds
( not
s in dom B or not
v = <*1*> ^ s )
by TREES_1:1;
then A9:
v in (dom ((elementary_tree 2) --> [2,0])) with-replacement (
<*0*>,
(dom A))
by A3, A5, A6, TREES_1:def 9;
now ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )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 A2, A9, TREES_2:def 11;
suppose A10:
( not
<*0*> is_a_prefix_of v &
y . v = ((elementary_tree 2) --> [2,0]) . v )
;
( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )A11:
dom ((elementary_tree 2) --> [2,0]) = {{},<*0*>,<*1*>}
by FUNCOP_1:13, TREES_1:53;
A12:
for
s being
FinSequence of
NAT holds
( not
s in dom A or not
v = <*0*> ^ s )
by A10, TREES_1:1;
then A13:
v in dom ((elementary_tree 2) --> [2,0])
by A2, A9, TREES_1:def 9;
then A14:
v = {}
by A7, A10, A11, ENUMSET1:def 1;
reconsider v9 =
v as
Element of
dom ((elementary_tree 2) --> [2,0]) by A2, A9, A12, TREES_1:def 9;
A15:
succ v = succ v9
proof
reconsider v99 =
v as
Element of
dom y by A5, A6, A8, TREES_1:def 9;
succ v99 = succ v9
by A2, A3, A14, Lm1, Th8;
hence
succ v = succ v9
by A5, A6, A14, Lm1, Th8;
verum
end; now for x being object holds
( ( x in succ v9 implies x in {<*0*>,<*1*>} ) & ( x in {<*0*>,<*1*>} implies x in succ v9 ) )let x be
object ;
( ( x in succ v9 implies x in {<*0*>,<*1*>} ) & ( x in {<*0*>,<*1*>} implies x in succ v9 ) )thus
(
x in succ v9 implies
x in {<*0*>,<*1*>} )
( x in {<*0*>,<*1*>} implies x in succ v9 )proof
assume
x in succ v9
;
x in {<*0*>,<*1*>}
then
x in { (v9 ^ <*n*>) where n is Nat : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) }
by TREES_2:def 5;
then consider n being
Nat such that A16:
x = v9 ^ <*n*>
and A17:
v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0])
;
<*n*> in dom ((elementary_tree 2) --> [2,0])
by A14, A17, FINSEQ_1:34;
then A18:
(
<*n*> = {} or
<*n*> = <*0*> or
<*n*> = <*1*> )
by A11, ENUMSET1:def 1;
x = <*n*>
by A14, A16, FINSEQ_1:34;
hence
x in {<*0*>,<*1*>}
by A18, TARSKI:def 2;
verum
end; assume
x in {<*0*>,<*1*>}
;
x in succ v9then A19:
(
x = <*0*> or
x = <*1*> )
by TARSKI:def 2;
hence
x in succ v9
;
verum end; then A22:
succ v9 = {<*0*>,<*1*>}
by TARSKI:2;
<*0*> <> <*1*>
by TREES_1:3;
then A23:
2
= card (succ v)
by A22, A15, CARD_2:57;
hence
branchdeg v <= 2
by TREES_2:def 12;
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )
v in elementary_tree 2
by A13;
hence
(
branchdeg v <= 2 & ( not
branchdeg v = 0 or
x . v = [0,0] or ex
k being
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 A7, A10, A23, FUNCOP_1:7, TREES_2:def 12;
verum end; suppose
ex
s being
FinSequence of
NAT st
(
s in dom A &
v = <*0*> ^ s &
y . v = A . s )
;
( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 A24:
s in dom A
and A25:
v = <*0*> ^ s
and A26:
y . v = A . s
;
reconsider s =
s as
Element of
dom A by A24;
succ v,
succ s are_equipotent
proof
reconsider v9 =
v as
Element of
dom y by A5, A6, A8, TREES_1:def 9;
succ v9,
succ s are_equipotent
by A2, A3, A25, TREES_2:37;
hence
succ v,
succ s are_equipotent
by A5, A6, A25, Th1, Th9;
verum
end; then
card (succ v) = card (succ s)
by CARD_1:5;
then A27:
branchdeg v = card (succ s)
by TREES_2:def 12;
A28:
branchdeg s <= 2
by Def5;
hence
branchdeg v <= 2
by A27, TREES_2:def 12;
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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] ) )A29:
( not
branchdeg s = 1 or
A . s = [1,0] or
A . s = [1,1] )
by Def5;
A30:
(
branchdeg s = 2 implies
A . s = [2,0] )
by Def5;
( not
branchdeg s = 0 or
A . s = [0,0] or ex
m being
Nat st
A . s = [3,m] )
by Def5;
hence
(
branchdeg v <= 2 & ( not
branchdeg v = 0 or
x . v = [0,0] or ex
k being
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 A7, A26, A28, A29, A30, A27, TREES_2:def 12;
verum end; end; end; hence
(
branchdeg v <= 2 & ( not
branchdeg v = 0 or
x . v = [0,0] or ex
k being
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] ) )
;
verum end; suppose
ex
s being
FinSequence of
NAT st
(
s in dom B &
v = <*1*> ^ s &
x . v = B . s )
;
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 A31:
s in dom B
and A32:
v = <*1*> ^ s
and A33:
x . v = B . s
;
reconsider s =
s as
Element of
dom B by A31;
succ v,
succ s are_equipotent
by A5, A6, A32, TREES_2:37;
then
card (succ v) = card (succ s)
by CARD_1:5;
then A34:
branchdeg v = card (succ s)
by TREES_2:def 12;
A35:
(
branchdeg s = 2 implies
B . s = [2,0] )
by Def5;
A36:
( not
branchdeg s = 1 or
B . s = [1,0] or
B . s = [1,1] )
by Def5;
A37:
( not
branchdeg s = 0 or
B . s = [0,0] or ex
m being
Nat st
B . s = [3,m] )
by Def5;
branchdeg s <= 2
by Def5;
hence
(
branchdeg v <= 2 & ( not
branchdeg v = 0 or
x . v = [0,0] or ex
k being
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 A33, A37, A36, A35, A34, TREES_2:def 12;
verum end; end; end;
hence
(
branchdeg v <= 2 & ( not
branchdeg v = 0 or
x . v = [0,0] or ex
k being
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] ) )
;
verum
end;
hence
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
by Def5; verum