:: deftheorem Def14 defines PrgLocalOverlapSeq NOMIN_8:def 14 :
for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being FPrg (ND (b₁,b₂)) -valued FinSequence st len prg > 0 holds
for b₇ being FinSequence of ND (V,A) holds
( b₇ = PrgLocalOverlapSeq (A,loc,d1,prg,pos) iff ( len b₇ = len prg & b₇ . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b₇ holds
b₇ . (n + 1) = local_overlapping (V,A,(b₇ . n),((prg . (n + 1)) . (b₇ . n)),(loc /. (pos . (n + 1)))) ) ) );