let s be State of SCM+FSA ; :: thesis:
let c0 be Element of NAT ; :: thesis:
assume A1: IC s = c0 ; :: thesis:
let a be Int-Location ; :: thesis:
let k be Integer; :: thesis:
assume A2: for c being Element of NAT st c < len (aSeq a,k) holds
(aSeq a,k) . (c + 1) = s . (c0 + c) ; :: thesis:

per cases ;

suppose A3: k > 0 ; :: thesis:

then reconsider k9 = k as Element of NAT by INT_1:16;
consider k1 being Element of NAT such that
A4: k1 + 1 = k9 and
A5: aSeq a,k9 = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) by A3, SCMFSA_7:def 3;
defpred S₁[ Nat] means ( $1 <= k9 implies IC (Comput (ProgramPart s),s,$1) = c0 + $1 );
A6: len (aSeq a,k9) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (AddTo a,(intloc 0 )))) by A5, FINSEQ_1:35
.= 1 + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:56
.= k9 by A4, FINSEQ_1:def 18 ;
for i being Element of NAT st i <= len (aSeq a,k9) holds
IC (Comput (ProgramPart s),s,i) = c0 + i

proof

A7: now

let i be Element of NAT ; :: thesis:
assume that
A8: 1 < i and
A9: i <= k9 ; :: thesis:
A10: 1 <= i - 1 by A8, INT_1:79;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
i - 1 <= k9 - 1 by A9, XREAL_1:11;
then A11: i1 in Seg k1 by A4, A10;
len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
hence (aSeq a,k9) . i = (k1 |-> (AddTo a,(intloc 0 ))) . (i - 1) by A5, A6, A8, A9, FINSEQ_1:37
.= AddTo a,(intloc 0 ) by A11, FUNCOP_1:13 ;
:: thesis:

end;

A12: now

let i be Element of NAT ; :: thesis:
assume that
A13: 0 < i and
A14: i < k9 ; :: thesis:
A15: ( 0 + 1 < i + 1 & i + 1 <= k9 ) by A13, A14, NAT_1:13, XREAL_1:8;
thus s . (c0 + i) = (aSeq a,k9) . (i + 1) by A2, A6, A14
.= AddTo a,(intloc 0 ) by A7, A15 ; :: thesis:

end;

A16: s . (c0 + 0 ) = (aSeq a,k9) . (0 + 1) by A2, A3, A6
.= a := (intloc 0 ) by A5, FINSEQ_1:58 ;

A17: now

end;

A20: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A21: S₁[n] ; :: thesis:
assume A22: n + 1 <= k9 ; :: thesis:

per cases ;

suppose A23: n = 0 ; :: thesis:

hence IC (Comput (ProgramPart s),s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A17
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ (c0 + n) by A1, A23, SCMFSA_2:89
.= (c0 + n) + 1 by NAT_1:39
.= c0 + (n + 1) ;
:: thesis:

end;

suppose A24: n > 0 ; :: thesis:

end;

let i be Element of NAT ; :: thesis:
assume A29: i <= len (aSeq a,k9) ; :: thesis:
A30: S₁[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A30, A20);
hence IC (Comput (ProgramPart s),s,i) = c0 + i by A6, A29; :: thesis:

end;

hence for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Comput (ProgramPart s),s,i) = c0 + i ; :: thesis:

end;

suppose A31: k <= 0 ; :: thesis:

then reconsider mk = - k as Element of NAT by INT_1:16;
defpred S₁[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (ProgramPart s),s,$1) = c0 + $1 );
consider k1 being Element of NAT such that
A32: k1 + k = 1 and
A33: aSeq a,k = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) by A31, SCMFSA_7:def 3;
A34: len (aSeq a,k) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (SubFrom a,(intloc 0 )))) by A33, FINSEQ_1:35
.= 1 + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:56
.= (mk + 1) + 1 by A32, FINSEQ_1:def 18 ;
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Comput (ProgramPart s),s,i) = c0 + i

proof

A35: now

let i be Element of NAT ; :: thesis:
assume that
A36: 1 < i and
A37: i <= (mk + 1) + 1 ; :: thesis:
A38: i - 1 <= ((mk + 1) + 1) - 1 by A37, XREAL_1:11;
A39: 1 - 1 < i - 1 by A36, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
(1 - 1) + 1 <= i - 1 by A39, INT_1:20;
then A40: i1 in Seg k1 by A32, A38;
len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
hence (aSeq a,k) . i = (k1 |-> (SubFrom a,(intloc 0 ))) . (i - 1) by A33, A34, A36, A37, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A40, FUNCOP_1:13 ;
:: thesis:

end;

A41: now

let i be Element of NAT ; :: thesis:
assume that
A42: 0 < i and
A43: i < (mk + 1) + 1 ; :: thesis:
A44: ( 0 + 1 < i + 1 & i + 1 <= (mk + 1) + 1 ) by A42, A43, NAT_1:13, XREAL_1:8;
thus s . (c0 + i) = (aSeq a,k) . (i + 1) by A2, A34, A43
.= SubFrom a,(intloc 0 ) by A35, A44 ; :: thesis:

end;

A45: s . (c0 + 0 ) = (aSeq a,k) . (0 + 1) by A2, A34
.= a := (intloc 0 ) by A33, FINSEQ_1:58 ;
A46: for n being Element of NAT st n = 0 holds
( Comput (ProgramPart s),s,n = s & CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s )

proof

end;

A49: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A50: S₁[n] ; :: thesis:
assume A51: n + 1 <= (mk + 1) + 1 ; :: thesis:

per cases ;

suppose A52: n = 0 ; :: thesis:

hence IC (Comput (ProgramPart s),s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A46
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ (c0 + n) by A1, A52, SCMFSA_2:89
.= (c0 + n) + 1 by NAT_1:39
.= c0 + (n + 1) ;
:: thesis:

end;

suppose A53: n > 0 ; :: thesis:

end;

let i be Element of NAT ; :: thesis:
assume A58: i <= len (aSeq a,k) ; :: thesis:
A59: S₁[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A59, A49);
hence IC (Comput (ProgramPart s),s,i) = c0 + i by A34, A58; :: thesis:

end;

hence for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Comput (ProgramPart s),s,i) = c0 + i ; :: thesis:

end;