let size be non zero Nat; for V, A being set
for val being Function
for loc being b1 -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let V, A be set ; for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let val be Function; for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let loc be V -valued Function; for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let d1 be NonatomicND of V,A; ( loc,val,size are_correct_wrt d1 implies for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume A1:
loc,val,size are_correct_wrt d1
; for m, n being Nat st 1 <= n & n <= m & m <= size holds
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
then A2:
val is_valid_wrt d1
;
let m, n be Nat; ( 1 <= n & n <= m & m <= size implies loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
assume that
A3:
1 <= n
and
A4:
n <= m
and
A5:
m <= size
; loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
A6:
1 <= m
by A3, A4, XXREAL_0:2;
A7:
n <= size
by A4, A5, XXREAL_0:2;
A8:
len (LocalOverlapSeq (A,loc,val,d1,size)) = size
by Def4;
reconsider i1 = n - 1 as Element of NAT by A3, INT_1:5;
set v = loc /. n;
set D = denaming (V,A,(val . n));
A9:
dom (denaming (V,A,(val . n))) = { d where d is NonatomicND of V,A : val . n in dom d }
by NOMIN_1:def 18;
A10:
loc /. n in {(loc /. n)}
by TARSKI:def 1;
n in dom (LocalOverlapSeq (A,loc,val,d1,size))
by A3, A7, A8, FINSEQ_3:25;
then A11:
val . n in rng val
by A1, FUNCT_1:def 3;
then A12:
val . n in dom d1
by A2;
per cases
( i1 = 0 or i1 > 0 )
;
suppose A13:
i1 = 0
;
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
d1 in dom (denaming (V,A,(val . n)))
by A2, A9, A11;
then reconsider d2 =
(denaming (V,A,(val . n))) . d1 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
A14:
(LocalOverlapSeq (A,loc,val,d1,size)) . 1
= local_overlapping (
V,
A,
d1,
d2,
(loc /. n))
by A13, Def4;
A15:
dom (local_overlapping (V,A,d1,d2,(loc /. n))) = {(loc /. n)} \/ (dom d1)
by A1, NOMIN_4:4;
A16:
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . 1) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
by A1, A5, A6, Th8;
loc /. n in {(loc /. n)} \/ (dom d1)
by A10, XBOOLE_0:def 3;
hence
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
by A14, A15, A16;
verum end; suppose
i1 > 0
;
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)then A17:
0 + 1
<= i1
by NAT_1:13;
n - 1
< n - 0
by XREAL_1:15;
then A18:
i1 < size
by A7, XXREAL_0:2;
then reconsider dd =
(LocalOverlapSeq (A,loc,val,d1,size)) . i1 as
NonatomicND of
V,
A by A17, A8, Def6;
dom d1 c= dom dd
by A1, A17, A18, Th7;
then
dd in dom (denaming (V,A,(val . n)))
by A12, A9;
then reconsider d2 =
(denaming (V,A,(val . n))) . dd as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
A19:
(LocalOverlapSeq (A,loc,val,d1,size)) . n = local_overlapping (
V,
A,
dd,
d2,
(loc /. (i1 + 1)))
by A8, A17, A18, Def4;
A20:
dom (local_overlapping (V,A,dd,d2,(loc /. n))) = {(loc /. n)} \/ (dom dd)
by A1, NOMIN_4:4;
A21:
loc /. n in {(loc /. n)} \/ (dom dd)
by A10, XBOOLE_0:def 3;
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
by A1, A3, A4, A5, Th8;
hence
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
by A21, A19, A20;
verum end;