let size be non zero Nat; for V, A being set
for loc being b1 -valued Function
for d1 being NonatomicND of V,A
for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let V, A be set ; for loc being V -valued Function
for d1 being NonatomicND of V,A
for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let loc be V -valued Function; for d1 being NonatomicND of V,A
for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let d1 be NonatomicND of V,A; for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let val be size -element FinSequence; ( Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 implies for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n) )
assume that
A1:
Seg size c= dom loc
and
A2:
loc | (Seg size) is one-to-one
and
A3:
loc,val are_different_wrt size
and
A4:
loc,val,size are_correct_wrt d1
; for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let m, n be Nat; ( 1 <= n & n <= m & m <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n) )
assume that
A5:
1 <= n
and
A6:
n <= m
and
A7:
m <= size
; ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
set F = LocalOverlapSeq (A,loc,val,d1,size);
A8:
Seg size = dom val
by FINSEQ_1:89;
A9:
len (LocalOverlapSeq (A,loc,val,d1,size)) = size
by Def4;
A10:
0 + 1 <= size
by NAT_1:13;
A11:
n <= size
by A6, A7, XXREAL_0:2;
defpred S1[ Nat] means ( n <= $1 & $1 <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) . (loc /. n) = d1 . (val . n) );
A12:
S1[ 0 ]
by A5;
A13:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume that A14:
S1[
k]
and A15:
n <= k + 1
and A16:
k + 1
<= size
;
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)
set D1 =
denaming (
V,
A,
(val . 1));
A17:
dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d }
by NOMIN_1:def 18;
A18:
rng val c= dom d1
by A4, Def1;
1
in Seg size
by A10, FINSEQ_1:1;
then A19:
val . 1
in rng val
by A8, FUNCT_1:def 3;
then
d1 in dom (denaming (V,A,(val . 1)))
by A18, A17;
then reconsider T1 =
(denaming (V,A,(val . 1))) . d1 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
A20:
(LocalOverlapSeq (A,loc,val,d1,size)) . 1
= local_overlapping (
V,
A,
d1,
T1,
(loc /. 1))
by Def4;
n in Seg size
by A5, A11, FINSEQ_1:1;
then A21:
val . n in rng val
by A8, FUNCT_1:def 3;
per cases
( k = 0 or k > 0 )
;
suppose A22:
k = 0
;
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)then
n = 1
by A5, A15, XXREAL_0:1;
hence
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)
by A4, A19, A18, A20, A22, Th2;
verum end; suppose
k > 0
;
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)then A23:
0 + 1
<= k
by NAT_1:13;
A24:
1
<= k + 1
by NAT_1:11;
A25:
k < size
by A16, NAT_1:13;
set D =
denaming (
V,
A,
(val . (k + 1)));
reconsider d2 =
(LocalOverlapSeq (A,loc,val,d1,size)) . k as
NonatomicND of
V,
A by A23, A9, A25, Def6;
A26:
dom (denaming (V,A,(val . (k + 1)))) = { d where d is NonatomicND of V,A : val . (k + 1) in dom d }
by NOMIN_1:def 18;
A27:
val . (k + 1) in dom d2
by A4, A24, A16, A23, A25, Th10;
then
d2 in dom (denaming (V,A,(val . (k + 1))))
by A26;
then reconsider T =
(denaming (V,A,(val . (k + 1)))) . d2 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
A28:
(LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1) = local_overlapping (
V,
A,
d2,
T,
(loc /. (k + 1)))
by A23, A9, A25, Def4;
per cases
( k + 1 = n or k + 1 <> n )
;
suppose A29:
k + 1
= n
;
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)then A30:
k < n
by NAT_1:13;
1
< n
by A23, A29, NAT_1:13;
then A31:
loc /. 1
<> val . n
by A3, A10, A11;
thus ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) =
d2 . (val . n)
by A4, A29, A27, A28, Th2
.=
((LocalOverlapSeq (A,loc,val,d1,size)) . 1) . (val . n)
by A4, A3, A11, A23, A30, Th11
.=
d1 . (val . n)
by A4, A18, A20, A31, A21, NOMIN_5:3
;
verum end; suppose
k + 1
<> n
;
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)then A32:
n < k + 1
by A15, XXREAL_0:1;
then
n <= k
by NAT_1:13;
then
loc /. n in dom d2
by A4, A5, A25, Th9;
hence
((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)
by A1, A2, A5, A4, A11, A14, A16, A24, A28, A32, Th1, NAT_1:13, NOMIN_5:3;
verum end; end; end; end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A12, A13);
hence
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
by A6, A7; verum