let p, q be Tree-yielding FinSequence; for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
let T1, T2 be Tree; tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
set w1 = (p ^ <*T1*>) ^ q;
set W1 = tree ((p ^ <*T1*>) ^ q);
set w2 = (p ^ <*T2*>) ^ q;
set W2 = tree ((p ^ <*T2*>) ^ q);
set W = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1;
A1:
len <*T1*> = 1
by FINSEQ_1:57;
A2:
len <*T2*> = 1
by FINSEQ_1:57;
A3:
len (p ^ <*T1*>) = (len p) + 1
by A1, FINSEQ_1:35;
A4:
len ((p ^ <*T1*>) ^ q) = (len (p ^ <*T1*>)) + (len q)
by FINSEQ_1:35;
A5:
len (p ^ <*T2*>) = (len p) + 1
by A2, FINSEQ_1:35;
A6:
len ((p ^ <*T2*>) ^ q) = (len (p ^ <*T2*>)) + (len q)
by FINSEQ_1:35;
(len p) + 1 <= ((len p) + 1) + (len q)
by NAT_1:11;
then A7:
len p < ((len p) + 1) + (len q)
by NAT_1:13;
then A8:
((p ^ <*T2*>) ^ q) . ((len p) + 1) in rng ((p ^ <*T2*>) ^ q)
by A5, A6, Lm4;
rng ((p ^ <*T2*>) ^ q) is constituted-Trees
by Def9;
then
((p ^ <*T2*>) ^ q) . ((len p) + 1) is Tree
by A8;
then A9:
{} in ((p ^ <*T2*>) ^ q) . ((len p) + 1)
by TREES_1:47;
<*(len p)*> ^ {} = <*(len p)*>
by FINSEQ_1:47;
then A10:
<*(len p)*> in tree ((p ^ <*T2*>) ^ q)
by A5, A6, A7, A9, Def15;
let r be FinSequence of NAT ; TREES_2:def 1 ( ( not r in tree ((p ^ <*T1*>) ^ q) or r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 ) & ( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 or r in tree ((p ^ <*T1*>) ^ q) ) )
thus
( r in tree ((p ^ <*T1*>) ^ q) implies r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 )
( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 or r in tree ((p ^ <*T1*>) ^ q) )proof
assume
r in tree ((p ^ <*T1*>) ^ q)
;
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
then A11:
(
r = {} or ex
n being
Element of
NAT ex
s being
FinSequence st
(
n < len ((p ^ <*T1*>) ^ q) &
s in ((p ^ <*T1*>) ^ q) . (n + 1) &
r = <*n*> ^ s ) )
by Def15;
now given n being
Element of
NAT ,
s being
FinSequence such that A12:
n < len ((p ^ <*T1*>) ^ q)
and A13:
s in ((p ^ <*T1*>) ^ q) . (n + 1)
and A14:
r = <*n*> ^ s
;
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1reconsider s =
s as
FinSequence of
NAT by A14, FINSEQ_1:50;
A15:
(
n <= len p or
n >= (len p) + 1 )
by NAT_1:13;
A16:
now assume A17:
n < len p
;
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1then A18:
n + 1
in dom p
by Lm4;
A19:
dom p c= dom (p ^ <*T2*>)
by FINSEQ_1:39;
A20:
dom p c= dom (p ^ <*T1*>)
by FINSEQ_1:39;
A21:
(p ^ <*T2*>) . (n + 1) = p . (n + 1)
by A18, FINSEQ_1:def 7;
A22:
(p ^ <*T1*>) . (n + 1) = p . (n + 1)
by A18, FINSEQ_1:def 7;
A23:
((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1)
by A18, A19, A21, FINSEQ_1:def 7;
((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1)
by A18, A20, A22, FINSEQ_1:def 7;
then A24:
r in tree ((p ^ <*T2*>) ^ q)
by A3, A4, A5, A6, A12, A13, A14, A23, Def15;
not
<*(len p)*> is_a_prefix_of <*n*> ^ s
by A17, TREES_1:87;
then
not
<*(len p)*> is_a_proper_prefix_of <*n*> ^ s
by XBOOLE_0:def 8;
hence
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,
T1
by A10, A14, A24, TREES_1:def 12;
verum end; A25:
now assume A26:
n = len p
;
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1then A27:
(p ^ <*T1*>) . (n + 1) = T1
by FINSEQ_1:59;
n < (len p) + 1
by A26, NAT_1:13;
then
n + 1
in dom (p ^ <*T1*>)
by A3, Lm4;
then A28:
((p ^ <*T1*>) ^ q) . (n + 1) = T1
by A27, FINSEQ_1:def 7;
s = s
;
hence
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,
T1
by A10, A13, A14, A26, A28, TREES_1:def 12;
verum end; now assume that A29:
n >= (len p) + 1
and A30:
n < ((len p) + 1) + (len q)
;
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1A31:
n + 1
>= ((len p) + 1) + 1
by A29, XREAL_1:9;
A32:
n + 1
<= ((len p) + 1) + (len q)
by A30, NAT_1:13;
then A33:
((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1))
by A3, A31, FINSEQ_1:36;
((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1))
by A5, A31, A32, FINSEQ_1:36;
then A34:
r in tree ((p ^ <*T2*>) ^ q)
by A3, A4, A5, A6, A12, A13, A14, A33, Def15;
len p <> n
by A29, NAT_1:13;
then
not
<*(len p)*> is_a_prefix_of <*n*> ^ s
by TREES_1:87;
then
not
<*(len p)*> is_a_proper_prefix_of <*n*> ^ s
by XBOOLE_0:def 8;
hence
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,
T1
by A10, A14, A34, TREES_1:def 12;
verum end; hence
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,
T1
by A3, A12, A15, A16, A25, FINSEQ_1:35, XXREAL_0:1;
verum end;
hence
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,
T1
by A11, TREES_1:47;
verum
end;
assume
r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
; r in tree ((p ^ <*T1*>) ^ q)
then A35:
( ( r in tree ((p ^ <*T2*>) ^ q) & not <*(len p)*> is_a_proper_prefix_of r ) or ex s being FinSequence of NAT st
( s in T1 & r = <*(len p)*> ^ s ) )
by A10, TREES_1:def 12;
assume A36:
not r in tree ((p ^ <*T1*>) ^ q)
; contradiction
then A37:
r <> {}
by Def15;
A38:
(p ^ <*T1*>) . ((len p) + 1) = T1
by FINSEQ_1:59;
A39:
len p < (len p) + 1
by NAT_1:13;
(len p) + 1 <= ((len p) + 1) + (len q)
by NAT_1:11;
then A40:
len p < len ((p ^ <*T2*>) ^ q)
by A5, A6, NAT_1:13;
(len p) + 1 in dom (p ^ <*T1*>)
by A3, A39, Lm4;
then A41:
((p ^ <*T1*>) ^ q) . ((len p) + 1) = T1
by A38, FINSEQ_1:def 7;
then consider n being Element of NAT , s being FinSequence such that
A42:
n < len ((p ^ <*T2*>) ^ q)
and
A43:
s in ((p ^ <*T2*>) ^ q) . (n + 1)
and
A44:
r = <*n*> ^ s
by A3, A4, A5, A6, A35, A36, A37, A40, Def15;
reconsider s = s as FinSequence of NAT by A44, FINSEQ_1:50;
A45:
( n = len p implies s = {} )
by A3, A4, A5, A6, A35, A36, A41, A42, A44, Def15, TREES_1:33;
{} in T1
by TREES_1:47;
then
n <> len p
by A3, A4, A5, A6, A36, A41, A42, A44, A45, Def15;
then
( n < len p or ( n > len p & 1 <= 1 ) )
by XXREAL_0:1;
then
( ( 1 <= 1 + n & 1 + n = n + 1 & n + 1 <= len p & (p ^ <*T1*>) ^ q = p ^ (<*T1*> ^ q) & (p ^ <*T2*>) ^ q = p ^ (<*T2*> ^ q) ) or ( (len p) + 1 < n + 1 & n + 1 <= len ((p ^ <*T1*>) ^ q) ) )
by A3, A4, A5, A6, A42, FINSEQ_1:45, NAT_1:11, NAT_1:13, XREAL_1:8;
then
( ( ((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1) & ((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1) ) or ( ((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) & ((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) ) )
by A3, A4, A5, A6, Lm1, FINSEQ_1:37;
hence
contradiction
by A3, A4, A5, A6, A36, A42, A43, A44, Def15; verum