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 Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being 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 Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being 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 Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being 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 Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being 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[ Nat] means (dom T1) -level $1 = (dom T2) -level $1;
A17:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
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
object ;
( 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[
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
Nat st
S2[
n] holds
S2[
n + 1]
proof
let n be
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 Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A14;
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A32, A37, TREES_2:12;
then consider k being
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 A41;
A44:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A30, A31, A33, A38, A40, 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 A14, A37, A43
.=
T2 . (w | (Seg (n + 1)))
by A16, A30, A31, A33, A38, A40, A37, A44, TREES_1:20, XXREAL_0:2
;
verum
end; A45:
S2[
0 ]
by A13, A15;
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A45, A29);
then A46:
T1 . w = T2 . w
by A26, A28;
A47:
succ v in { (succ w) where w is Element of dom T2 : len w = n }
by A27;
(
succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . v)),(T2 . v))) } &
succ w = { (w ^ <*k*>) where k is 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, A46, A47, TARSKI:def 4;
verum
end;
let a be
object ;
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 A19, A51;
then consider v being
Element of
dom T1 such that A52:
w = v
and A53:
len v = n
by A18, A20;
A54:
w = w | (Seg (len w))
by FINSEQ_3:49;
defpred S2[
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
Nat st
S2[
n] holds
S2[
n + 1]
proof
let n be
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 Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A14;
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A58, A63, TREES_2:12;
then consider k being
Nat such that A68:
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A69:
k in card (NIC ((M /. (T1 . t1)),(T1 . t1)))
by A67;
A70:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A56, A57, A59, A64, A66, A68, A69, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A68, 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, A63, A69
.=
T2 . (w | (Seg (n + 1)))
by A16, A56, A57, A59, A64, A66, A63, A70, TREES_1:20, XXREAL_0:2
;
verum
end;
A71:
S2[
0 ]
by A13, A15;
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A71, A55);
then A72:
T1 . w = T2 . w
by A52, A54;
A73:
succ v in { (succ w) where w is Element of dom T1 : len w = n }
by A53;
(
succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . v)),(T1 . v))) } &
succ w = { (w ^ <*k*>) where k is 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 A48, A50, A52, A72, A73, 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 A74:
S1[ 0 ]
;
A75:
for n being Nat holds S1[n]
from NAT_1:sch 2(A74, 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[
Nat]
means ( $1
<= len p &
p | (Seg $1) in dom T1 implies
T1 . (p | (Seg $1)) = T2 . (p | (Seg $1)) );
A76:
p | (Seg (len p)) = p
by FINSEQ_3:49;
A77:
for
n being
Nat st
S2[
n] holds
S2[
n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume that A78:
S2[
n]
and A79:
n + 1
<= len p
and A80:
p | (Seg (n + 1)) in dom T1
;
T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))
set t1 =
p | (Seg n);
A81:
1
<= n + 1
by NAT_1:11;
A82:
len (p | (Seg (n + 1))) = n + 1
by A79, FINSEQ_1:17;
then
len (p | (Seg (n + 1))) in Seg (n + 1)
by A81, FINSEQ_1:1;
then A83:
p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A82, FUNCT_1:49;
n + 1
in dom p
by A79, A81, FINSEQ_3:25;
then A84:
p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*>
by A83, FINSEQ_5:10;
A85:
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 A80, TREES_1:20;
reconsider t2 =
t1 as
Element of
dom T2 by A75, TREES_2:38;
A86:
succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) }
by A14;
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1
by A80, A84, TREES_2:12;
then consider k being
Nat such that A87:
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A88:
k in card (NIC ((M /. (T1 . t1)),(T1 . t1)))
by A86;
A89:
(p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2)))
by A78, A79, A85, A87, A88, FINSEQ_2:17, XXREAL_0:2;
k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A87, 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, A84, A88
.=
T2 . (p | (Seg (n + 1)))
by A16, A78, A79, A85, A84, A89, XXREAL_0:2
;
verum
end;
A90:
S2[
0 ]
by A13, A15;
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A90, A77);
hence
(
p in dom T1 implies
T1 . p = T2 . p )
by A76;
verum
end;
hence
T1 = T2
by A75, TREES_2:31, TREES_2:38; verum