let s be State of SCM+FSA ; :: thesis:
let c0 be Element of NAT ; :: thesis:
assume A1: IC s = insloc 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 . (insloc (c0 + c)) ; :: thesis:

per cases ;

suppose A3: k > 0 ; :: thesis:

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

proof

let i be Element of NAT ; :: thesis:
assume A7: i <= len (aSeq a,k') ; :: thesis:
A8: s . (insloc (c0 + 0 )) = (aSeq a,k') . (0 + 1) by A2, A3, A6
.= a := (intloc 0 ) by A5, FINSEQ_1:58 ;

A9: now

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

end;

A13: now

let i be Element of NAT ; :: thesis:
assume A14: ( 0 < i & i < k' ) ; :: thesis:
then A15: 0 + 1 < i + 1 by XREAL_1:8;
A16: i + 1 <= k' by A14, NAT_1:13;
thus s . (insloc (c0 + i)) = (aSeq a,k') . (i + 1) by A2, A6, A14
.= AddTo a,(intloc 0 ) by A9, A15, A16 ; :: thesis:

end;

A17: now

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A18: Computation s,n = s by AMI_1:13; :: thesis:
hence A19: CurInstr (Computation s,n) = a := (intloc 0 ) by A1, A8, AMI_1:def 17; :: thesis:
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A18, A19, AMI_1:def 18 ; :: thesis:

end;

A20: S₁[ 0 ] by A1, AMI_1:13;
A21: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A22: S₁[n] ; :: thesis:
assume A23: n + 1 <= k' ; :: thesis:

per cases ;

suppose A24: n = 0 ; :: thesis:

hence IC (Computation s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A17
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (insloc (c0 + n)) by A1, A24, SCMFSA_2:89
.= insloc ((c0 + n) + 1) by NAT_1:39
.= insloc (c0 + (n + 1)) ;
:: thesis:

end;

suppose A25: n > 0 ; :: thesis:

A26: n + 0 <= n + 1 by XREAL_1:9;
A27: ( 0 < n & n < k' ) by A23, A25, NAT_1:13;
A28: CurInstr (Computation s,n) = (Computation s,n) . (insloc (c0 + n)) by A22, A23, A26, AMI_1:def 17, XXREAL_0:2
.= s . (insloc (c0 + n)) by AMI_1:54
.= AddTo a,(intloc 0 ) by A13, A27 ;
A29: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (AddTo a,(intloc 0 )),(Computation s,n) by A28, AMI_1:def 18 ;
thus IC (Computation s,(n + 1)) = (Computation s,(n + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (IC (Computation s,n)) by A29, SCMFSA_2:90
.= insloc ((c0 + n) + 1) by A22, A23, A26, NAT_1:39, XXREAL_0:2
.= insloc (c0 + (n + 1)) ; :: thesis:

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A20, A21);
hence IC (Computation s,i) = insloc (c0 + i) by A6, A7; :: thesis:

end;

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

end;

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

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

proof

let i be Element of NAT ; :: thesis:
assume A34: i <= len (aSeq a,k) ; :: thesis:
A35: s . (insloc (c0 + 0 )) = (aSeq a,k) . (0 + 1) by A2, A33
.= a := (intloc 0 ) by A32, FINSEQ_1:58 ;

A36: now

let i be Element of NAT ; :: thesis:
assume A37: ( 1 < i & i <= (mk + 1) + 1 ) ; :: thesis:
then A38: 1 - 1 < i - 1 by XREAL_1:11;
then A39: (1 - 1) + 1 <= i - 1 by INT_1:20;
reconsider i1 = i - 1 as Element of NAT by A38, INT_1:16;
i - 1 <= ((mk + 1) + 1) - 1 by A37, XREAL_1:11;
then A40: i1 in Seg k1 by A31, A39, FINSEQ_1:3;
len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
hence (aSeq a,k) . i = (k1 |-> (SubFrom a,(intloc 0 ))) . (i - 1) by A32, A33, 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 A42: ( 0 < i & i < (mk + 1) + 1 ) ; :: thesis:
then A43: 0 + 1 < i + 1 by XREAL_1:8;
A44: i + 1 <= (mk + 1) + 1 by A42, NAT_1:13;
thus s . (insloc (c0 + i)) = (aSeq a,k) . (i + 1) by A2, A33, A42
.= SubFrom a,(intloc 0 ) by A36, A43, A44 ; :: thesis:

end;

A45: for n being Element of NAT st n = 0 holds
( Computation s,n = s & CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s )

proof

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A46: Computation s,n = s by AMI_1:13; :: thesis:
hence A47: CurInstr (Computation s,n) = a := (intloc 0 ) by A1, A35, AMI_1:def 17; :: thesis:
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A46, A47, AMI_1:def 18 ; :: thesis:

end;

A48: S₁[ 0 ] by A1, AMI_1:13;
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 (Computation s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A45
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (insloc (c0 + n)) by A1, A52, SCMFSA_2:89
.= insloc ((c0 + n) + 1) by NAT_1:39
.= insloc (c0 + (n + 1)) ;
:: thesis:

end;

suppose A53: n > 0 ; :: thesis:

A54: n + 0 <= n + 1 by XREAL_1:9;
A55: ( 0 < n & n < (mk + 1) + 1 ) by A51, A53, NAT_1:13;
A56: CurInstr (Computation s,n) = (Computation s,n) . (insloc (c0 + n)) by A50, A51, A54, AMI_1:def 17, XXREAL_0:2
.= s . (insloc (c0 + n)) by AMI_1:54
.= SubFrom a,(intloc 0 ) by A41, A55 ;
A57: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (SubFrom a,(intloc 0 )),(Computation s,n) by A56, AMI_1:def 18 ;
thus IC (Computation s,(n + 1)) = (Computation s,(n + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (IC (Computation s,n)) by A57, SCMFSA_2:91
.= insloc ((c0 + n) + 1) by A50, A51, A54, NAT_1:39, XXREAL_0:2
.= insloc (c0 + (n + 1)) ; :: thesis:

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A48, A49);
hence IC (Computation s,i) = insloc (c0 + i) by A33, A34; :: thesis:

end;

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

end;