let T1, T2 be Tree; tree (T1,T2) = ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
let p be FinSequence of NAT ; TREES_2:def 1 ( ( not p in tree (T1,T2) or p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) ) & ( not p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) or p in tree (T1,T2) ) )
A1:
<*T1,T2*> . 1 = T1
;
A2:
<*T1,T2*> . 2 = T2
;
A3:
len <*T1,T2*> = 2
by FINSEQ_1:44;
A4:
1 + 1 = 2
;
A5:
0 + 1 = 1
;
A6:
{} in T1
by TREES_1:22;
A7:
{} in T2
by TREES_1:22;
A8:
<*0*> in elementary_tree 2
by ENUMSET1:def 1, TREES_1:53;
A9:
<*1*> in elementary_tree 2
by ENUMSET1:def 1, TREES_1:53;
not <*0*> is_a_proper_prefix_of <*1*>
by TREES_1:52;
then A10:
<*1*> in (elementary_tree 2) with-replacement (<*0*>,T1)
by A8, A9, TREES_1:def 9;
thus
( p in tree (T1,T2) implies p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) )
( not p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) or p in tree (T1,T2) )proof
assume A11:
p in tree (
T1,
T2)
;
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
now ( p <> {} implies p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) )assume
p <> {}
;
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)then consider n being
Nat,
q being
FinSequence such that A12:
n < len <*T1,T2*>
and A13:
q in <*T1,T2*> . (n + 1)
and A14:
p = <*n*> ^ q
by A11, Def15;
reconsider q =
q as
FinSequence of
NAT by A14, FINSEQ_1:36;
A15:
not
<*1*> is_a_prefix_of <*0*> ^ q
by TREES_1:50;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
A16:
now ( n = 0 implies p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) )assume A17:
n = 0
;
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)then A18:
not
<*1*> is_a_proper_prefix_of <*n*> ^ q
by A15;
<*n*> ^ q in (elementary_tree 2) with-replacement (
<*0*>,
T1)
by A8, A13, A17, TREES_1:def 9;
hence
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (
<*1*>,
T2)
by A10, A14, A18, TREES_1:def 9;
verum end;
n <= 0 + 1
by A3, A4, A12, NAT_1:13;
then
( (
n = 1 & (
n = 1 implies
<*n*> ^ q in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (
<*1*>,
T2) ) ) or (
n >= 0 &
n <= 0 ) )
by A10, A13, NAT_1:8, TREES_1:def 9;
hence
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (
<*1*>,
T2)
by A14, A16;
verum end;
hence
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (
<*1*>,
T2)
by TREES_1:22;
verum
end;
assume
p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
; p in tree (T1,T2)
then A19:
( ( p in (elementary_tree 2) with-replacement (<*0*>,T1) & not <*1*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T2 & p = <*1*> ^ r ) )
by A10, TREES_1:def 9;
now ( p in (elementary_tree 2) with-replacement (<*0*>,T1) implies p in tree (T1,T2) )assume
p in (elementary_tree 2) with-replacement (
<*0*>,
T1)
;
p in tree (T1,T2)then A20:
( (
p in elementary_tree 2 & not
<*0*> is_a_proper_prefix_of p ) or ex
r being
FinSequence of
NAT st
(
r in T1 &
p = <*0*> ^ r ) )
by A8, TREES_1:def 9;
now ( p in elementary_tree 2 implies p in tree (T1,T2) )assume
p in elementary_tree 2
;
p in tree (T1,T2)then A21:
(
p = {} or
p = <*0*> or
p = <*1*> )
by ENUMSET1:def 1, TREES_1:53;
p ^ {} = p
by FINSEQ_1:34;
hence
p in tree (
T1,
T2)
by A1, A2, A3, A4, A5, A6, A7, A21, Def15;
verum end; hence
p in tree (
T1,
T2)
by A1, A3, A5, A20, Def15;
verum end;
hence
p in tree (T1,T2)
by A2, A3, A4, A19, Def15; verum