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