let s be State of SCM+FSA ; :: thesis:
assume A1: s . (intloc 0 ) = 1 ; :: thesis:
let c0 be Element of NAT ; :: thesis:
assume A2: IC s = insloc c0 ; :: thesis:
let a be Int-Location ; :: thesis:
let k be Integer; :: thesis:
assume that
A3: a <> intloc 0 and
A4: for c being Element of NAT st c in dom (aSeq a,k) holds
(aSeq a,k) . c = s . (insloc ((c0 + c) -' 1)) ; :: thesis:

per cases ;

suppose A5: k > 0 ; :: thesis:

then reconsider k' = k as Element of NAT by INT_1:16;
consider k1 being Element of NAT such that
A6: k1 + 1 = k' and
A7: aSeq a,k' = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) by A5, Def3;
A8: len (aSeq a,k') = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (AddTo a,(intloc 0 )))) by A7, FINSEQ_1:35
.= 1 + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:56
.= k' by A6, FINSEQ_1:def 18 ;
defpred S₁[ Element of NAT ] means ( $1 <= k' implies ( IC (Computation s,$1) = insloc (c0 + $1) & ( 1 <= $1 implies (Computation s,$1) . a = $1 ) & ( for b being Int-Location st b <> a holds
(Computation s,$1) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,$1) . f = s . f ) ) );
A9: for i being Element of NAT st i <= len (aSeq a,k') holds
( IC (Computation s,i) = insloc (c0 + i) & ( 1 <= i implies (Computation s,i) . a = i ) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) )

proof

let i be Element of NAT ; :: thesis:
assume A10: i <= len (aSeq a,k') ; :: thesis:

A11: now

let i be Element of NAT ; :: thesis:
assume i < k' ; :: thesis:
then insloc i in dom (Load (aSeq a,k')) by A8, Th29;
hence i + 1 in dom (aSeq a,k') by Th26; :: thesis:

end;

A12: now

let i be Element of NAT ; :: thesis:
assume A13: i < k' ; :: thesis:
thus s . (insloc (c0 + i)) = s . (insloc (((c0 + i) + 1) -' 1)) by NAT_D:34
.= s . (insloc ((c0 + (i + 1)) -' 1))
.= (aSeq a,k') . (i + 1) by A4, A11, A13 ; :: thesis:

end;

then A14: s . (insloc (c0 + 0 )) = (aSeq a,k') . (0 + 1) by A5
.= a := (intloc 0 ) by A7, FINSEQ_1:58 ;

A15: now

let i be Element of NAT ; :: thesis:
assume A16: ( 1 < i & i <= k' ) ; :: thesis:
then A17: 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 A16, XREAL_1:11;
then A18: i1 in Seg k1 by A6, A17, 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 A7, A8, A16, FINSEQ_1:37
.= AddTo a,(intloc 0 ) by A18, FUNCOP_1:13 ;
:: thesis:

end;

A19: now

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

end;

A23: now

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A24: Computation s,n = s by AMI_1:13; :: thesis:
hence CurInstr (Computation s,n) = a := (intloc 0 ) by A2, A14; :: thesis:
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A2, A14, A24 ; :: thesis:

end;

A25: S₁[ 0 ] by A2, AMI_1:13;
A26: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

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

per cases ;

suppose A29: n = 0 ; :: thesis:

hence IC (Computation s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A23
.= Next (insloc (c0 + n)) by A2, A29, SCMFSA_2:89
.= insloc ((c0 + n) + 1) by NAT_1:39
.= insloc (c0 + (n + 1)) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Computation s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A23, A29
.= n + 1 by A1, A29, SCMFSA_2:89 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A30: b <> a ; :: thesis:
thus (Computation s,(n + 1)) . b = (Exec (a := (intloc 0 )),s) . b by A23, A29
.= s . b by A30, SCMFSA_2:89 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Computation s,(n + 1)) . f = (Exec (a := (intloc 0 )),s) . f by A23, A29
.= s . f by SCMFSA_2:89 ; :: thesis:

end;

suppose A31: n > 0 ; :: thesis:

then A32: 0 + 1 <= n by INT_1:20;
A33: n + 0 <= n + 1 by XREAL_1:9;
A34: ( 0 < n & n < k' ) by A28, A31, NAT_1:13;
A35: CurInstr (Computation s,n) = s . (insloc (c0 + n)) by A27, A28, A33, AMI_1:54, XXREAL_0:2
.= AddTo a,(intloc 0 ) by A19, A34 ;
A36: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (AddTo a,(intloc 0 )),(Computation s,n) by A35 ;
hence IC (Computation s,(n + 1)) = Next (IC (Computation s,n)) by SCMFSA_2:90
.= insloc ((c0 + n) + 1) by A27, A28, A33, NAT_1:39, XXREAL_0:2
.= insloc (c0 + (n + 1)) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Computation s,(n + 1)) . a = n + ((Computation s,n) . (intloc 0 )) by A27, A28, A32, A33, A36, SCMFSA_2:90, XXREAL_0:2
.= n + 1 by A1, A3, A27, A28, A33, XXREAL_0:2 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A37: b <> a ; :: thesis:
hence (Computation s,(n + 1)) . b = (Computation s,n) . b by A36, SCMFSA_2:90
.= s . b by A27, A28, A33, A37, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Computation s,(n + 1)) . f = (Computation s,n) . f by A36, SCMFSA_2:90
.= s . f by A27, A28, A33, XXREAL_0:2 ; :: thesis:

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A25, A26);
hence ( IC (Computation s,i) = insloc (c0 + i) & ( 1 <= i implies (Computation s,i) . a = i ) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) by A8, A10; :: thesis:

end;

hence for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc (c0 + i) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ; :: thesis:
1 <= len (aSeq a,k) by A6, A8, NAT_1:11;
hence (Computation s,(len (aSeq a,k))) . a = k by A8, A9; :: thesis:

end;

suppose A38: 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
A39: k1 + k = 1 and
A40: aSeq a,k = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) by A38, Def3;
A41: len (aSeq a,k) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (SubFrom a,(intloc 0 )))) by A40, FINSEQ_1:35
.= 1 + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:56
.= (mk + 1) + 1 by A39, FINSEQ_1:def 18 ;
defpred S₁[ Element of NAT ] means ( $1 <= (mk + 1) + 1 implies ( IC (Computation s,$1) = insloc (c0 + $1) & ( 1 <= $1 implies (Computation s,$1) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,$1) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,$1) . f = s . f ) ) );
A42: for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc (c0 + i) & ( 1 <= i implies (Computation s,i) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) )

proof

let i be Element of NAT ; :: thesis:
assume A43: i <= len (aSeq a,k) ; :: thesis:

A44: now

let i be Element of NAT ; :: thesis:
assume i < (mk + 1) + 1 ; :: thesis:
then insloc i in dom (Load (aSeq a,k)) by A41, Th29;
hence i + 1 in dom (aSeq a,k) by Th26; :: thesis:

end;

A45: now

let i be Element of NAT ; :: thesis:
assume A46: i < (mk + 1) + 1 ; :: thesis:
thus s . (insloc (c0 + i)) = s . (insloc (((c0 + i) + 1) -' 1)) by NAT_D:34
.= s . (insloc ((c0 + (i + 1)) -' 1))
.= (aSeq a,k) . (i + 1) by A4, A44, A46 ; :: thesis:

end;

then A47: s . (insloc (c0 + 0 )) = (aSeq a,k) . (0 + 1)
.= a := (intloc 0 ) by A40, FINSEQ_1:58 ;

A48: now

let i be Element of NAT ; :: thesis:
assume A49: ( 1 < i & i <= (mk + 1) + 1 ) ; :: thesis:
then A50: 1 - 1 < i - 1 by XREAL_1:11;
then A51: (1 - 1) + 1 <= i - 1 by INT_1:20;
reconsider i1 = i - 1 as Element of NAT by A50, INT_1:16;
i - 1 <= ((mk + 1) + 1) - 1 by A49, XREAL_1:11;
then A52: i1 in Seg k1 by A39, A51, 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 A40, A41, A49, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A52, FUNCOP_1:13 ;
:: thesis:

end;

A53: now

let i be Element of NAT ; :: thesis:
assume A54: ( 0 < i & i < (mk + 1) + 1 ) ; :: thesis:
then A55: 0 + 1 < i + 1 by XREAL_1:8;
A56: i + 1 <= (mk + 1) + 1 by A54, NAT_1:13;
thus s . (insloc (c0 + i)) = (aSeq a,k) . (i + 1) by A45, A54
.= SubFrom a,(intloc 0 ) by A48, A55, A56 ; :: thesis:

end;

A57: 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 A58: Computation s,n = s by AMI_1:13; :: thesis:
hence CurInstr (Computation s,n) = a := (intloc 0 ) by A2, A47; :: thesis:
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A2, A47, A58 ; :: thesis:

end;

A59: S₁[ 0 ] by A2, AMI_1:13;
A60: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

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

per cases ;

suppose A63: n = 0 ; :: thesis:

hence IC (Computation s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A57
.= Next (insloc (c0 + n)) by A2, A63, SCMFSA_2:89
.= insloc ((c0 + n) + 1) by NAT_1:39
.= insloc (c0 + (n + 1)) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Computation s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A57, A63
.= ((- (n + 1)) + 1) + 1 by A1, A63, SCMFSA_2:89 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A64: b <> a ; :: thesis:
thus (Computation s,(n + 1)) . b = (Exec (a := (intloc 0 )),s) . b by A57, A63
.= s . b by A64, SCMFSA_2:89 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Computation s,(n + 1)) . f = (Exec (a := (intloc 0 )),s) . f by A57, A63
.= s . f by SCMFSA_2:89 ; :: thesis:

end;

suppose A65: n > 0 ; :: thesis:

then A66: 0 + 1 < n + 1 by XREAL_1:8;
A67: n + 0 <= n + 1 by XREAL_1:9;
A68: ( 0 < n & n < (mk + 1) + 1 ) by A62, A65, NAT_1:13;
A69: CurInstr (Computation s,n) = s . (insloc (c0 + n)) by A61, A62, A67, AMI_1:54, XXREAL_0:2
.= SubFrom a,(intloc 0 ) by A53, A68 ;
A70: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (SubFrom a,(intloc 0 )),(Computation s,n) by A69 ;
hence IC (Computation s,(n + 1)) = Next (IC (Computation s,n)) by SCMFSA_2:91
.= insloc ((c0 + n) + 1) by A61, A62, A67, NAT_1:39, XXREAL_0:2
.= insloc (c0 + (n + 1)) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Computation s,(n + 1)) . a = (((- n) + 1) + 1) - ((Computation s,n) . (intloc 0 )) by A61, A62, A66, A70, NAT_1:13, SCMFSA_2:91
.= (((- n) + 1) + 1) - (s . (intloc 0 )) by A3, A61, A62, A67, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A1 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A71: b <> a ; :: thesis:
hence (Computation s,(n + 1)) . b = (Computation s,n) . b by A70, SCMFSA_2:91
.= s . b by A61, A62, A67, A71, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Computation s,(n + 1)) . f = (Computation s,n) . f by A70, SCMFSA_2:91
.= s . f by A61, A62, A67, XXREAL_0:2 ; :: thesis:

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A59, A60);
hence ( IC (Computation s,i) = insloc (c0 + i) & ( 1 <= i implies (Computation s,i) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) by A41, A43; :: thesis:

end;

hence for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc (c0 + i) & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ; :: thesis:
1 <= len (aSeq a,k) by A41, NAT_1:11;
hence (Computation s,(len (aSeq a,k))) . a = ((- ((- k) + (1 + 1))) + 1) + 1 by A41, A42
.= k ;
:: thesis:

end;