let c0 be Element of NAT ; :: thesis:
let s be c0 -started State of SCM+FSA; :: thesis:
A1: IC s = c0 by COMPOS_1:def 20;
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 = s . (c0 + c) ; :: thesis:
S4: for c being Element of NAT st c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = s . (c0 + c)

proof

let c be Element of NAT ; :: thesis:
assume c in dom (aSeq (a,k)) ; :: thesis:
then c < len (aSeq (a,k)) by AFINSQ_1:70;
hence (aSeq (a,k)) . c = s . (c0 + c) by A2; :: thesis:

end;

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, AFINSQ_1:20
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:38
.= k9 by A4, CARD_1:106 ;
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
A17: 1 <= i and
A18: i < k9 ; :: thesis:
reconsider i1 = i - 1 as Element of NAT by A17, INT_1:18;
i = i1 + 1 ;
then i1 < k1 by A18, A4, XREAL_1:8;
then A20: i1 in k1 by NAT_1:45;
TT: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:106;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:36;
hence (aSeq (a,k9)) . i = (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A17, A5, TT, A4, A18, AFINSQ_1:21
.= AddTo (a,(intloc 0)) by A20, FUNCOP_1:13 ;
:: thesis:

end;

S10: for i being Element of NAT st i < k9 holds
i in dom (aSeq (a,k9)) by A6, NAT_1:45;

A12: now

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

end;

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

A17: now

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A18: Comput ((ProgramPart s),s,n) = s by EXTPRO_1:3; :: thesis:
hence CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) by A1, A16, COMPOS_1:38; :: thesis:
thus Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((a := (intloc 0)),s) by A18, A1, A16, COMPOS_1:38 ; :: thesis:

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))) = (Exec ((a := (intloc 0)),s)) . (IC SCM+FSA) by A17
.= (succ c0) + n by A1, A23, SCMFSA_2:89
.= (c0 + 1) + n 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, EXTPRO_1:3;
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, AFINSQ_1:20
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:38
.= (mk + 1) + 1 by A32, CARD_1:106 ;
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
A51: 1 <= i and
A52: i < (mk + 1) + 1 ; :: thesis:
A53: i - 1 < ((mk + 1) + 1) - 1 by A52, XREAL_1:11;
reconsider i1 = i - 1 as Element of NAT by A51, INT_1:18;
A55: i1 in k1 by A32, A53, NAT_1:45;
TT: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:106;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:36;
hence (aSeq (a,k)) . i = (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A33, A51, TT, A32, A52, AFINSQ_1:21
.= SubFrom (a,(intloc 0)) by A55, FUNCOP_1:13 ;
:: thesis:

end;

S44: for i being Element of NAT st i < (mk + 1) + 1 holds
i in dom (aSeq (a,k)) by A34, NAT_1:45;

A41: now

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

end;

A45: s . (c0 + 0) = (aSeq (a,k)) . 0 by A2, A34
.= a := (intloc 0) by A33, AFINSQ_1:39 ;
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

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A47: Comput ((ProgramPart s),s,n) = s by EXTPRO_1:3; :: thesis:
hence CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) by A1, A45, COMPOS_1:38; :: thesis:
thus Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((a := (intloc 0)),s) by A47, A1, A45, COMPOS_1:38 ; :: thesis:

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))) = (Exec ((a := (intloc 0)),s)) . (IC SCM+FSA) by A46
.= 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, EXTPRO_1:3;
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;