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
by FINSEQ_1:61;
A2:
<*T1,T2*> . 2 = T2
by FINSEQ_1:61;
A3:
len <*T1,T2*> = 2
by FINSEQ_1:61;
A4:
1 + 1 = 2
;
A5:
0 + 1 = 1
;
A6:
{} in T1
by TREES_1:47;
A7:
{} in T2
by TREES_1:47;
A8:
<*0 *> in elementary_tree 2
by ENUMSET1:def 1, TREES_1:90;
A9:
<*1*> in elementary_tree 2
by ENUMSET1:def 1, TREES_1:90;
not <*0 *> is_a_proper_prefix_of <*1*>
by TREES_1:89;
then A10:
<*1*> in (elementary_tree 2) with-replacement <*0 *>,T1
by A8, A9, TREES_1:def 12;
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 assume
p <> {}
;
p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2then consider n being
Element of
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:50;
A15:
not
<*1*> is_a_prefix_of <*0 *> ^ q
by TREES_1:87;
A16:
now assume A17:
n = 0
;
p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2then A18:
not
<*1*> is_a_proper_prefix_of <*n*> ^ q
by A15, XBOOLE_0:def 8;
<*n*> ^ q in (elementary_tree 2) with-replacement <*0 *>,
T1
by A1, A8, A13, A17, TREES_1:def 12;
hence
p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,
T2
by A10, A14, A18, TREES_1:def 12;
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 A2, A10, A13, NAT_1:8, TREES_1:def 12;
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:47;
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 12;
now assume
p in (elementary_tree 2) with-replacement <*0 *>,
T1
;
p in tree T1,T2then 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 12;
now assume
p in elementary_tree 2
;
p in tree T1,T2then A21:
(
p = {} or
p = <*0 *> or
p = <*1*> )
by ENUMSET1:def 1, TREES_1:90;
p ^ {} = p
by FINSEQ_1:47;
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