let T1, T2 be DecoratedTree of NAT ; ( T1 . {} = FirstLoc M & ( for t being Element of dom T1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds
T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) ) & T2 . {} = FirstLoc M & ( for t being Element of dom T2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds
T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ) implies T1 = T2 )
assume that
A12:
T1 . {} = FirstLoc M
and
A13:
for t being Element of dom T1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds
T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) )
and
A14:
T2 . {} = FirstLoc M
and
A15:
for t being Element of dom T2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds
T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) )
; T1 = T2
defpred S1[ Element of NAT ] means (dom T1) -level $1 = (dom T2) -level $1;
A16:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )
assume A17:
S1[
n]
;
S1[n + 1]
set U2 =
{ (succ w) where w is Element of dom T2 : len w = n } ;
set U1 =
{ (succ w) where w is Element of dom T1 : len w = n } ;
A18:
(dom T2) -level n = { v where v is Element of dom T2 : len v = n }
by TREES_2:def 6;
A19:
(dom T1) -level n = { v where v is Element of dom T1 : len v = n }
by TREES_2:def 6;
A20:
union { (succ w) where w is Element of dom T1 : len w = n } = union { (succ w) where w is Element of dom T2 : len w = n }
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 union { (succ w) where w is Element of dom T2 : len w = n } c= union { (succ w) where w is Element of dom T1 : len w = n }
let a be
set ;
( a in union { (succ w) where w is Element of dom T1 : len w = n } implies a in union { (succ w) where w is Element of dom T2 : len w = n } )assume
a in union { (succ w) where w is Element of dom T1 : len w = n }
;
a in union { (succ w) where w is Element of dom T2 : len w = n } then consider A being
set such that A21:
a in A
and A22:
A in { (succ w) where w is Element of dom T1 : len w = n }
by TARSKI:def 4;
consider w being
Element of
dom T1 such that A23:
A = succ w
and A24:
len w = n
by A22;
w in (dom T1) -level n
by A19, A24;
then consider v being
Element of
dom T2 such that A25:
w = v
and A26:
len v = n
by A17, A18;
A27:
w = w | (Seg (len w))
by FINSEQ_3:49;
defpred S2[
Element of
NAT ]
means ( $1
<= len w &
w | (Seg $1) in dom T1 &
v | (Seg $1) in dom T2 implies
T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );
A28:
for
n being
Element of
NAT st
S2[
n] holds
S2[
n + 1]
proof
let n be
Element of
NAT ;
( S2[n] implies S2[n + 1] )
assume that A29:
S2[
n]
and A30:
n + 1
<= len w
and A31:
w | (Seg (n + 1)) in dom T1
and A32:
v | (Seg (n + 1)) in dom T2
;
T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 =
w | (Seg n);
A33:
1
<= n + 1
by NAT_1:11;
A34:
len (w | (Seg (n + 1))) = n + 1
by A30, FINSEQ_1:17;
then
len (w | (Seg (n + 1))) in Seg (n + 1)
by A33, FINSEQ_1:1;
then A35:
w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A34, FUNCT_1:49;
n + 1
in dom w
by A30, A33, FINSEQ_3:25;
then A36:
w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*>
by A35, FINSEQ_5:10;
A37:
n <= n + 1
by NAT_1:11;
then A38:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
then
v | (Seg n) = (v | (Seg (n + 1))) | (Seg n)
by RELAT_1:74;
then A39:
v | (Seg n) is_a_prefix_of v | (Seg (n + 1))
by TREES_1:def 1;
w | (Seg n) = (w | (Seg (n + 1))) | (Seg n)
by A38, RELAT_1:74;
then
w | (Seg n) is_a_prefix_of w | (Seg (n + 1))
by TREES_1:def 1;
then reconsider t1 =
w | (Seg n) as
Element of
dom T1 by A31, TREES_1:20;
reconsider t2 =
t1 as
Element of
dom T2 by A25, A32, A39, TREES_1:20;
A40:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A13;
A41:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 12;
then
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A31, A36, TREES_2:12;
then consider k being
Element of
NAT such that A42:
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A43:
k in card (NIC ((M /. (T1 . t1)),(T1 . t1)))
by A40;
A44:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A29, A30, A32, A37, A39, A42, A43, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A42, FINSEQ_2:17;
hence T1 . (w | (Seg (n + 1))) =
(LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))
by A13, A36, A43
.=
T2 . (w | (Seg (n + 1)))
by A15, A29, A30, A32, A37, A39, A41, A36, A44, TREES_1:20, XXREAL_0:2
;
verum
end; A45:
S2[
0 ]
by A12, A14;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A45, A28);
then A46:
T1 . w = T2 . w
by A25, A27;
A47:
succ v in { (succ w) where w is Element of dom T2 : len w = n }
by A26;
(
succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . v)),(T2 . v))) } &
succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . w)),(T1 . w))) } )
by A13, A15;
hence
a in union { (succ w) where w is Element of dom T2 : len w = n }
by A21, A23, A25, A46, A47, TARSKI:def 4;
verum
end;
let a be
set ;
TARSKI:def 3 ( not a in union { (succ w) where w is Element of dom T2 : len w = n } or a in union { (succ w) where w is Element of dom T1 : len w = n } )
assume
a in union { (succ w) where w is Element of dom T2 : len w = n }
;
a in union { (succ w) where w is Element of dom T1 : len w = n }
then consider A being
set such that A48:
a in A
and A49:
A in { (succ w) where w is Element of dom T2 : len w = n }
by TARSKI:def 4;
consider w being
Element of
dom T2 such that A50:
A = succ w
and A51:
len w = n
by A49;
w in (dom T2) -level n
by A18, A51;
then consider v being
Element of
dom T1 such that A52:
w = v
and A53:
len v = n
by A17, A19;
A54:
w = w | (Seg (len w))
by FINSEQ_3:49;
defpred S2[
Element of
NAT ]
means ( $1
<= len w &
w | (Seg $1) in dom T1 &
v | (Seg $1) in dom T2 implies
T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );
A55:
for
n being
Element of
NAT st
S2[
n] holds
S2[
n + 1]
proof
let n be
Element of
NAT ;
( S2[n] implies S2[n + 1] )
assume that A56:
S2[
n]
and A57:
n + 1
<= len w
and A58:
w | (Seg (n + 1)) in dom T1
and A59:
v | (Seg (n + 1)) in dom T2
;
T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 =
w | (Seg n);
A60:
1
<= n + 1
by NAT_1:11;
A61:
len (w | (Seg (n + 1))) = n + 1
by A57, FINSEQ_1:17;
then
len (w | (Seg (n + 1))) in Seg (n + 1)
by A60, FINSEQ_1:1;
then A62:
w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A61, FUNCT_1:49;
n + 1
in dom w
by A57, A60, FINSEQ_3:25;
then A63:
w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*>
by A62, FINSEQ_5:10;
A64:
n <= n + 1
by NAT_1:11;
then A65:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
then
v | (Seg n) = (v | (Seg (n + 1))) | (Seg n)
by RELAT_1:74;
then A66:
v | (Seg n) is_a_prefix_of v | (Seg (n + 1))
by TREES_1:def 1;
w | (Seg n) = (w | (Seg (n + 1))) | (Seg n)
by A65, RELAT_1:74;
then
w | (Seg n) is_a_prefix_of w | (Seg (n + 1))
by TREES_1:def 1;
then reconsider t1 =
w | (Seg n) as
Element of
dom T1 by A58, TREES_1:20;
reconsider t2 =
t1 as
Element of
dom T2 by A52, A59, A66, TREES_1:20;
A67:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A13;
A68:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 12;
then
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A58, A63, TREES_2:12;
then consider k being
Element of
NAT such that A69:
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A70:
k in card (NIC ((M /. (T1 . t1)),(T1 . t1)))
by A67;
A71:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A56, A57, A59, A64, A66, A69, A70, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A69, FINSEQ_2:17;
hence T1 . (w | (Seg (n + 1))) =
(LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))
by A13, A63, A70
.=
T2 . (w | (Seg (n + 1)))
by A15, A56, A57, A59, A64, A66, A68, A63, A71, TREES_1:20, XXREAL_0:2
;
verum
end;
A72:
S2[
0 ]
by A12, A14;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A72, A55);
then A73:
T1 . w = T2 . w
by A52, A54;
A74:
succ v in { (succ w) where w is Element of dom T1 : len w = n }
by A53;
(
succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . v)),(T1 . v))) } &
succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . w)),(T2 . w))) } )
by A13, A15;
hence
a in union { (succ w) where w is Element of dom T1 : len w = n }
by A48, A50, A52, A73, A74, TARSKI:def 4;
verum
end;
(dom T1) -level (n + 1) = union { (succ w) where w is Element of dom T1 : len w = n }
by TREES_9:45;
hence
S1[
n + 1]
by A20, TREES_9:45;
verum
end;
(dom T1) -level 0 =
{{}}
by TREES_9:44
.=
(dom T2) -level 0
by TREES_9:44
;
then A75:
S1[ 0 ]
;
A76:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A75, A16);
for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p
proof
let p be
FinSequence of
NAT ;
( p in dom T1 implies T1 . p = T2 . p )
defpred S2[
Element of
NAT ]
means ( $1
<= len p &
p | (Seg $1) in dom T1 implies
T1 . (p | (Seg $1)) = T2 . (p | (Seg $1)) );
A77:
p | (Seg (len p)) = p
by FINSEQ_3:49;
A78:
for
n being
Element of
NAT st
S2[
n] holds
S2[
n + 1]
proof
let n be
Element of
NAT ;
( S2[n] implies S2[n + 1] )
assume that A79:
S2[
n]
and A80:
n + 1
<= len p
and A81:
p | (Seg (n + 1)) in dom T1
;
T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))
set t1 =
p | (Seg n);
A82:
1
<= n + 1
by NAT_1:11;
A83:
len (p | (Seg (n + 1))) = n + 1
by A80, FINSEQ_1:17;
then
len (p | (Seg (n + 1))) in Seg (n + 1)
by A82, FINSEQ_1:1;
then A84:
p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A83, FUNCT_1:49;
n + 1
in dom p
by A80, A82, FINSEQ_3:25;
then A85:
p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*>
by A84, FINSEQ_5:10;
A86:
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
then
p | (Seg n) = (p | (Seg (n + 1))) | (Seg n)
by RELAT_1:74;
then
p | (Seg n) is_a_prefix_of p | (Seg (n + 1))
by TREES_1:def 1;
then reconsider t1 =
p | (Seg n) as
Element of
dom T1 by A81, TREES_1:20;
reconsider t2 =
t1 as
Element of
dom T2 by A76, TREES_2:38;
A87:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A13;
A88:
(p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 12;
then
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1
by A81, A85, TREES_2:12;
then consider k being
Element of
NAT such that A89:
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A90:
k in card (NIC ((M /. (T1 . t1)),(T1 . t1)))
by A87;
A91:
(p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A79, A80, A86, A89, A90, FINSEQ_2:17, XXREAL_0:2;
k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A89, FINSEQ_2:17;
hence T1 . (p | (Seg (n + 1))) =
(LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))
by A13, A85, A90
.=
T2 . (p | (Seg (n + 1)))
by A15, A79, A80, A86, A88, A85, A91, XXREAL_0:2
;
verum
end;
A92:
S2[
0 ]
by A12, A14;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A92, A78);
hence
(
p in dom T1 implies
T1 . p = T2 . p )
by A77;
verum
end;
hence
T1 = T2
by A76, TREES_2:31, TREES_2:38; verum