let n be Nat; :: thesis:
let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let d1 be NonatomicND of V,A; :: thesis:
let p be SCPartialNominativePredicate of V,A; :: thesis:
let d be object ; :: thesis:
let size be non zero Nat; :: thesis:
let val be size -element FinSequence; :: thesis:
set D = denaming (V,A,(val . (len val)));
set S = SC_Psuperpos_Seq (loc,val,p);
set L = LocalOverlapSeq (A,loc,val,d1,size);
deffunc H₁( Nat) -> TypeSCNominativeData of V,A = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - $1) - 1)),((denaming (V,A,(val . ((len val) - $1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - $1) - 1))),(loc /. ((len val) - $1)));
assume that
A1: loc,val,size are_correct_wrt d1 and
A2: d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) and
A3: 2 <= n + 1 and
A4: n + 1 < size and
A5: local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p ; :: thesis:
A6: len val = size by CARD_1:def 7;
A7: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by NOMIN_7:def 4;
A8: len (SC_Psuperpos_Seq (loc,val,p)) = len val by Def9;
defpred S₁[ Nat] means ( 2 <= $1 + 1 & $1 + 1 < size implies H₁($1) in dom ((SC_Psuperpos_Seq (loc,val,p)) . $1) );
A9: S₁[ 0 ] ;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume that
A11: S₁[k] and
2 <= (k + 1) + 1 and
A12: (k + 1) + 1 < size ; :: thesis:
A13: 2 <= k + 2 by NAT_1:11;
then A14: 2 < size by A12, XXREAL_0:2;

per cases ;

suppose A15: k = 0 ; :: thesis:

(SC_Psuperpos_Seq (loc,val,p)) . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) by Def9;
then A16: dom ((SC_Psuperpos_Seq (loc,val,p)) . 1) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p & d in dom (denaming (V,A,(val . (len val)))) ) } by NOMIN_2:def 11;
A17: dom (denaming (V,A,(val . (len val)))) = { d where d is NonatomicND of V,A : val . (len val) in dom d } by NOMIN_1:def 18;
reconsider N = size - 2 as Element of NAT by A13, A12, XXREAL_0:2, INT_1:5;
2 - 2 < size - 2 by A14, XREAL_1:14;
then A18: 0 + 1 <= N by NAT_1:13;
A19: N < len (LocalOverlapSeq (A,loc,val,d1,size)) by A7, XREAL_1:44;
then A20: (LocalOverlapSeq (A,loc,val,d1,size)) . (N + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . N),((denaming (V,A,(val . (N + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . N)),(loc /. (N + 1))) by A18, NOMIN_7:def 4;
A21: 1 <= len val by A6, A7, A18, A19, XXREAL_0:2;
A22: 1 <= N + 1 by NAT_1:11;
A23: N + 1 <= size by XREAL_1:44, NAT_1:13;
reconsider F1 = H₁(1) as NonatomicND of V,A by A6, A7, A20, A23, NAT_1:11, NOMIN_7:def 6;
val . (len val) in dom F1 by A1, A6, A21, A20, A22, A23, NOMIN_7:10;
then H₁(1) in dom (denaming (V,A,(val . (len val)))) by A17;
hence H₁(k + 1) in dom ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) by A15, A16, A5, A2, A6, A20; :: thesis:

end;

suppose A24: k > 0 ; :: thesis:

then 0 + 1 <= k by NAT_1:13;
then A25: 1 + 1 <= k + 1 by XREAL_1:7;
A26: k + 1 < size by A12, NAT_1:13;
set D = denaming (V,A,(val . ((len val) - k)));
A27: 0 + 1 <= k by A24, NAT_1:13;
k < k + 2 by XREAL_1:29;
then k < size by A12, XXREAL_0:2;
then (SC_Psuperpos_Seq (loc,val,p)) . (k + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . k),(denaming (V,A,(val . ((len val) - k)))),(loc /. ((len val) - k))) by A6, A8, A27, Def9;
then A28: dom ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . ((len val) - k)))) . d),(loc /. ((len val) - k))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . k) & d in dom (denaming (V,A,(val . ((len val) - k)))) ) } by NOMIN_2:def 11;
A29: dom (denaming (V,A,(val . ((len val) - k)))) = { d where d is NonatomicND of V,A : val . ((len val) - k) in dom d } by NOMIN_1:def 18;
A30: size - (k + 1) < size by XREAL_1:44;
A31: (k + 1) - k < size - k by A26, XREAL_1:9;
then A32: 1 - 1 < (size - k) - 1 by XREAL_1:9;
then A33: 0 + 1 <= (size - k) - 1 by INT_1:7;
reconsider s = (size - k) - 1 as Element of NAT by A32, INT_1:3;
reconsider N = s - 1 as Element of NAT by A33, INT_1:5;
((k + 1) + 1) - k < size - k by A12, XREAL_1:9;
then (1 + 1) - 1 < (size - k) - 1 by XREAL_1:9;
then 1 - 1 < N by XREAL_1:9;
then A34: 0 + 1 <= N by INT_1:7;
N < s by XREAL_1:44;
then N < len (LocalOverlapSeq (A,loc,val,d1,size)) by A7, A30, XXREAL_0:2;
then A35: (LocalOverlapSeq (A,loc,val,d1,size)) . s = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . N),((denaming (V,A,(val . (N + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . N)),(loc /. (N + 1))) by A34, NOMIN_7:def 4;
reconsider Fk1 = H₁(k + 1) as NonatomicND of V,A by A6, A7, A35, A30, A33, NOMIN_7:def 6;
reconsider M = size - k as Element of NAT by A31, INT_1:3;
M <= size by XREAL_1:43;
then val . ((len val) - k) in dom Fk1 by A1, A6, A35, A30, A33, A31, NOMIN_7:10;
then H₁(k + 1) in dom (denaming (V,A,(val . ((len val) - k)))) by A29;
hence H₁(k + 1) in dom ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) by A6, A11, A25, A28, A35, A12, NAT_1:13; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10);
hence local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - n) - 1)),((denaming (V,A,(val . ((len val) - n)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - n) - 1))),(loc /. ((len val) - n))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . n) by A3, A4; :: thesis: