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 = 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 . ((c0 + c) -' 1) ; :: thesis:

per cases ;

suppose A5: k > 0 ; :: thesis:

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

proof

A10: now

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

end;

A11: now

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

end;

then A13: s . (c0 + 0 ) = (aSeq a,k9) . (0 + 1) by A5
.= a := (intloc 0 ) by A7, FINSEQ_1:58 ;

A14: now

end;

A16: now

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

end;

A21: now

let i be Element of NAT ; :: thesis:
assume that
A22: 0 < i and
A23: i < k9 ; :: thesis:
A24: ( 0 + 1 < i + 1 & i + 1 <= k9 ) by A22, A23, NAT_1:13, XREAL_1:8;
thus s . (c0 + i) = (aSeq a,k9) . (i + 1) by A11, A23
.= AddTo a,(intloc 0 ) by A16, A24 ; :: thesis:

end;

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

proof

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

per cases ;

suppose A28: n = 0 ; :: thesis:

hence IC (Comput (ProgramPart s),s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A14
.= succ (c0 + n) by A2, A28, SCMFSA_2:89
.= (c0 + n) + 1 by NAT_1:39
.= c0 + (n + 1) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A14, A28
.= n + 1 by A1, A28, SCMFSA_2:89 ; :: thesis:

end;

hereby :: thesis:

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

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Exec (a := (intloc 0 )),s) . f by A14, A28
.= s . f by SCMFSA_2:89 ; :: thesis:

end;

suppose A30: n > 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = n + ((Comput (ProgramPart s),s,n) . (intloc 0 )) by A26, A27, A35, A32, A34, SCMFSA_2:90, XXREAL_0:2
.= n + 1 by A1, A3, A26, A27, A32, XXREAL_0:2 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A36: b <> a ; :: thesis:
hence (Comput (ProgramPart s),s,(n + 1)) . b = (Comput (ProgramPart s),s,n) . b by A34, SCMFSA_2:90
.= s . b by A26, A27, A32, A36, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Comput (ProgramPart s),s,n) . f by A34, SCMFSA_2:90
.= s . f by A26, A27, A32, XXREAL_0:2 ; :: thesis:

end;

A37: S₁[ 0 ] by A2, AMI_1:13;
A38: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A37, A25);
let i be Element of NAT ; :: thesis:
assume i <= len (aSeq a,k9) ; :: thesis:
hence ( IC (Comput (ProgramPart s),s,i) = c0 + i & ( 1 <= i implies (Comput (ProgramPart s),s,i) . a = i ) & ( for b being Int-Location st b <> a holds
(Comput (ProgramPart s),s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s),s,i) . f = s . f ) ) by A8, A38; :: thesis:

end;

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

end;

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

proof

A44: now

let i be Element of NAT ; :: thesis:
assume i < (mk + 1) + 1 ; :: thesis:
then i in dom (Load (aSeq a,k)) by A42, 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 . (c0 + i) = s . (((c0 + i) + 1) -' 1) by NAT_D:34
.= s . ((c0 + (i + 1)) -' 1)
.= (aSeq a,k) . (i + 1) by A4, A44, A46 ; :: thesis:

end;

then A47: s . (c0 + 0 ) = (aSeq a,k) . (0 + 1)
.= a := (intloc 0 ) by A41, FINSEQ_1:58 ;
A48: 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;

A50: now

let i be Element of NAT ; :: thesis:
assume that
A51: 1 < i and
A52: i <= (mk + 1) + 1 ; :: thesis:
A53: i - 1 <= ((mk + 1) + 1) - 1 by A52, XREAL_1:11;
A54: 1 - 1 < i - 1 by A51, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
(1 - 1) + 1 <= i - 1 by A54, INT_1:20;
then A55: i1 in Seg k1 by A40, A53;
len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
hence (aSeq a,k) . i = (k1 |-> (SubFrom a,(intloc 0 ))) . (i - 1) by A41, A42, A51, A52, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A55, FUNCOP_1:13 ;
:: thesis:

end;

A56: now

let i be Element of NAT ; :: thesis:
assume that
A57: 0 < i and
A58: i < (mk + 1) + 1 ; :: thesis:
A59: ( 0 + 1 < i + 1 & i + 1 <= (mk + 1) + 1 ) by A57, A58, NAT_1:13, XREAL_1:8;
thus s . (c0 + i) = (aSeq a,k) . (i + 1) by A45, A58
.= SubFrom a,(intloc 0 ) by A50, A59 ; :: thesis:

end;

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 (Comput (ProgramPart s),s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A48
.= succ (c0 + n) by A2, A63, SCMFSA_2:89
.= (c0 + n) + 1 by NAT_1:39
.= c0 + (n + 1) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A48, 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 (Comput (ProgramPart s),s,(n + 1)) . b = (Exec (a := (intloc 0 )),s) . b by A48, A63
.= s . b by A64, SCMFSA_2:89 ; :: thesis:

end;

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

end;

suppose A65: n > 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (((- n) + 1) + 1) - ((Comput (ProgramPart s),s,n) . (intloc 0 )) by A61, A62, A70, A69, 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 (Comput (ProgramPart s),s,(n + 1)) . b = (Comput (ProgramPart s),s,n) . b by A69, SCMFSA_2:91
.= s . b by A61, A62, A67, A71, XXREAL_0:2 ;
:: thesis:

end;

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

end;

A72: S₁[ 0 ] by A2, AMI_1:13;
A73: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A72, A60);
let i be Element of NAT ; :: thesis:
assume i <= len (aSeq a,k) ; :: thesis:
hence ( IC (Comput (ProgramPart s),s,i) = c0 + i & ( 1 <= i implies (Comput (ProgramPart s),s,i) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (ProgramPart s),s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s),s,i) . f = s . f ) ) by A42, A73; :: thesis:

end;

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

end;