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 n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
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 n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
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 n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let loc be V -valued Function; for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let d1 be NonatomicND of V,A; ( loc,val,size are_correct_wrt d1 implies for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
val is_valid_wrt d1
and
A4:
dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val
; NOMIN_7:def 7 for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let n be Nat; ( 1 <= n & n <= size implies dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) )
assume that
A5:
1 <= n
and
A6:
n <= size
; dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
defpred S1[ Nat] means ( 1 <= $1 & $1 <= size implies dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) );
A7:
S1[ 0 ]
;
A8:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume that A9:
S1[
k]
and A10:
1
<= k + 1
and A11:
k + 1
<= size
;
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
A12:
len (LocalOverlapSeq (A,loc,val,d1,size)) = size
by Def4;
per cases
( k = 0 or k > 0 )
;
suppose A13:
k = 0
;
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))set v =
loc /. 1;
set D =
denaming (
V,
A,
(val . 1));
A14:
dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d }
by NOMIN_1:def 18;
1
<= len (LocalOverlapSeq (A,loc,val,d1,size))
by A10, A11, A12, XXREAL_0:2;
then
1
in dom (LocalOverlapSeq (A,loc,val,d1,size))
by FINSEQ_3:25;
then
val . 1
in rng val
by A4, FUNCT_1:def 3;
then
d1 in dom (denaming (V,A,(val . 1)))
by A3, A14;
then reconsider d2 =
(denaming (V,A,(val . 1))) . d1 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
A15:
(LocalOverlapSeq (A,loc,val,d1,size)) . 1
= local_overlapping (
V,
A,
d1,
d2,
(loc /. 1))
by Def4;
dom (local_overlapping (V,A,d1,d2,(loc /. 1))) = {(loc /. 1)} \/ (dom d1)
by A1, A2, NOMIN_4:4;
hence
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
by A13, A15, XBOOLE_1:7;
verum end; suppose
k > 0
;
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))then A16:
0 + 1
<= k
by NAT_1:13;
A17:
k <= k + 1
by NAT_1:12;
then A18:
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k)
by A9, A11, A16, XXREAL_0:2;
k + 0 < k + 1
by XREAL_1:8;
then A19:
k < size
by A11, XXREAL_0:2;
k + 1
in dom (LocalOverlapSeq (A,loc,val,d1,size))
by A11, A12, FINSEQ_3:25, NAT_1:12;
then
val . (k + 1) in rng val
by A4, FUNCT_1:def 3;
then
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
by A1, A2, A3, A16, A18, A19, Th6;
hence
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
by A17, A9, A11, A16, XXREAL_0:2;
verum end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A7, A8);
hence
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
by A5, A6; verum