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 (pi M,(T1 . t)),(T1 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T1 . t)),(T1 . t)) holds
T1 . (t ^ <*m*>) = (LocSeq (NIC (pi 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 (pi M,(T2 . t)),(T2 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T2 . t)),(T2 . t)) holds
T2 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T2 . t)),(T2 . t)),S) . m ) ) ) implies T1 = T2 )
assume that
A16:
T1 . {} = FirstLoc M
and
A17:
for t being Element of dom T1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . t)),(T1 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T1 . t)),(T1 . t)) holds
T1 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T1 . t)),(T1 . t)),S) . m ) )
and
A18:
T2 . {} = FirstLoc M
and
A19:
for t being Element of dom T2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T2 . t)),(T2 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T2 . t)),(T2 . t)) holds
T2 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T2 . t)),(T2 . t)),S) . m ) )
; T1 = T2
defpred S1[ Element of NAT ] means (dom T1) -level $1 = (dom T2) -level $1;
A20:
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 A21:
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 } ;
A22:
(dom T2) -level n = { v where v is Element of dom T2 : len v = n }
by TREES_2:def 6;
A23:
(dom T1) -level n = { v where v is Element of dom T1 : len v = n }
by TREES_2:def 6;
A24:
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 A25:
a in A
and A26:
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 A27:
A = succ w
and A28:
len w = n
by A26;
w in (dom T1) -level n
by A23, A28;
then consider v being
Element of
dom T2 such that A29:
w = v
and A30:
len v = n
by A21, A22;
A31:
w = w | (Seg (len w))
by FINSEQ_3:55;
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)) );
A32:
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 A33:
S2[
n]
and A34:
n + 1
<= len w
and A35:
w | (Seg (n + 1)) in dom T1
and A36:
v | (Seg (n + 1)) in dom T2
;
T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 =
w | (Seg n);
A37:
1
<= n + 1
by NAT_1:11;
A38:
len (w | (Seg (n + 1))) = n + 1
by A34, FINSEQ_1:21;
then
len (w | (Seg (n + 1))) in Seg (n + 1)
by A37, FINSEQ_1:3;
then A39:
w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A38, FUNCT_1:72;
n + 1
in dom w
by A34, A37, FINSEQ_3:27;
then A40:
w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*>
by A39, FINSEQ_5:11;
A41:
n <= n + 1
by NAT_1:11;
then A42:
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
then
v | (Seg n) = (v | (Seg (n + 1))) | (Seg n)
by RELAT_1:103;
then A43:
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 A42, RELAT_1:103;
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 A35, TREES_1:45;
reconsider t2 =
t1 as
Element of
dom T2 by A29, A36, A43, TREES_1:45;
A44:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . t1)),(T1 . t1)) }
by A17;
A45:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 13;
then
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A35, A40, TREES_2:14;
then consider k being
Element of
NAT such that A46:
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A47:
k in card (NIC (pi M,(T1 . t1)),(T1 . t1))
by A44;
A48:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC (pi M,(T2 . t2)),(T2 . t2))
by A33, A34, A36, A41, A43, A46, A47, FINSEQ_2:20, TREES_1:45, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A46, FINSEQ_2:20;
hence T1 . (w | (Seg (n + 1))) =
(LocSeq (NIC (pi M,(T1 . t1)),(T1 . t1)),S) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))
by A17, A40, A47
.=
T2 . (w | (Seg (n + 1)))
by A19, A33, A34, A36, A41, A43, A45, A40, A48, TREES_1:45, XXREAL_0:2
;
verum
end; A49:
S2[
0 ]
by A16, A18;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A49, A32);
then A50:
T1 . w = T2 . w
by A29, A31;
A51:
succ v in { (succ w) where w is Element of dom T2 : len w = n }
by A30;
(
succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T2 . v)),(T2 . v)) } &
succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . w)),(T1 . w)) } )
by A17, A19;
hence
a in union { (succ w) where w is Element of dom T2 : len w = n }
by A25, A27, A29, A50, A51, 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 A52:
a in A
and A53:
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 A54:
A = succ w
and A55:
len w = n
by A53;
w in (dom T2) -level n
by A22, A55;
then consider v being
Element of
dom T1 such that A56:
w = v
and A57:
len v = n
by A21, A23;
A58:
w = w | (Seg (len w))
by FINSEQ_3:55;
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)) );
A59:
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 A60:
S2[
n]
and A61:
n + 1
<= len w
and A62:
w | (Seg (n + 1)) in dom T1
and A63:
v | (Seg (n + 1)) in dom T2
;
T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 =
w | (Seg n);
A64:
1
<= n + 1
by NAT_1:11;
A65:
len (w | (Seg (n + 1))) = n + 1
by A61, FINSEQ_1:21;
then
len (w | (Seg (n + 1))) in Seg (n + 1)
by A64, FINSEQ_1:3;
then A66:
w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A65, FUNCT_1:72;
n + 1
in dom w
by A61, A64, FINSEQ_3:27;
then A67:
w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*>
by A66, FINSEQ_5:11;
A68:
n <= n + 1
by NAT_1:11;
then A69:
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
then
v | (Seg n) = (v | (Seg (n + 1))) | (Seg n)
by RELAT_1:103;
then A70:
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 A69, RELAT_1:103;
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 A62, TREES_1:45;
reconsider t2 =
t1 as
Element of
dom T2 by A56, A63, A70, TREES_1:45;
A71:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . t1)),(T1 . t1)) }
by A17;
A72:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 13;
then
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1
by A62, A67, TREES_2:14;
then consider k being
Element of
NAT such that A73:
t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A74:
k in card (NIC (pi M,(T1 . t1)),(T1 . t1))
by A71;
A75:
(w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC (pi M,(T2 . t2)),(T2 . t2))
by A60, A61, A63, A68, A70, A73, A74, FINSEQ_2:20, TREES_1:45, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))
by A73, FINSEQ_2:20;
hence T1 . (w | (Seg (n + 1))) =
(LocSeq (NIC (pi M,(T1 . t1)),(T1 . t1)),S) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))
by A17, A67, A74
.=
T2 . (w | (Seg (n + 1)))
by A19, A60, A61, A63, A68, A70, A72, A67, A75, TREES_1:45, XXREAL_0:2
;
verum
end;
A76:
S2[
0 ]
by A16, A18;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A76, A59);
then A77:
T1 . w = T2 . w
by A56, A58;
A78:
succ v in { (succ w) where w is Element of dom T1 : len w = n }
by A57;
(
succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . v)),(T1 . v)) } &
succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T2 . w)),(T2 . w)) } )
by A17, A19;
hence
a in union { (succ w) where w is Element of dom T1 : len w = n }
by A52, A54, A56, A77, A78, TARSKI:def 4;
verum
end;
(dom T1) -level (n + 1) = union { (succ w) where w is Element of dom T1 : len w = n }
by QC_LANG4:18;
hence
S1[
n + 1]
by A24, QC_LANG4:18;
verum
end;
(dom T1) -level 0 =
{{} }
by QC_LANG4:17
.=
(dom T2) -level 0
by QC_LANG4:17
;
then A79:
S1[ 0 ]
;
A80:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A79, A20);
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)) );
A82:
p | (Seg (len p)) = p
by FINSEQ_3:55;
A83:
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 A84:
S2[
n]
and A85:
n + 1
<= len p
and A86:
p | (Seg (n + 1)) in dom T1
;
T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))
set t1 =
p | (Seg n);
A87:
1
<= n + 1
by NAT_1:11;
A88:
len (p | (Seg (n + 1))) = n + 1
by A85, FINSEQ_1:21;
then
len (p | (Seg (n + 1))) in Seg (n + 1)
by A87, FINSEQ_1:3;
then A89:
p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A88, FUNCT_1:72;
n + 1
in dom p
by A85, A87, FINSEQ_3:27;
then A90:
p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*>
by A89, FINSEQ_5:11;
A91:
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
then
p | (Seg n) = (p | (Seg (n + 1))) | (Seg n)
by RELAT_1:103;
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 A86, TREES_1:45;
reconsider t2 =
t1 as
Element of
dom T2 by A80, Th18;
A92:
succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T1 . t1)),(T1 . t1)) }
by A17;
A93:
(p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) is
Element of
NAT
by ORDINAL1:def 13;
then
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1
by A86, A90, TREES_2:14;
then consider k being
Element of
NAT such that A94:
t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*>
and A95:
k in card (NIC (pi M,(T1 . t1)),(T1 . t1))
by A92;
A96:
(p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC (pi M,(T2 . t2)),(T2 . t2))
by A84, A85, A91, A94, A95, FINSEQ_2:20, XXREAL_0:2;
k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))
by A94, FINSEQ_2:20;
hence T1 . (p | (Seg (n + 1))) =
(LocSeq (NIC (pi M,(T1 . t1)),(T1 . t1)),S) . ((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))
by A17, A90, A95
.=
T2 . (p | (Seg (n + 1)))
by A19, A84, A85, A91, A93, A90, A96, XXREAL_0:2
;
verum
end;
A97:
S2[
0 ]
by A16, A18;
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A97, A83);
hence
(
p in dom T1 implies
T1 . p = T2 . p )
by A82;
verum
end;
hence
T1 = T2
by A80, Th18, TREES_2:33; verum