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