let c0 be Element of NAT ; :: thesis:
let s be c0 -started State of SCM+FSA; :: thesis:
assume A1: s . (intloc 0) = 1 ; :: thesis:
A2: IC s = c0 by COMPOS_1:def 16;
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) ; :: 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, AFINSQ_1:20
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:36
.= k9 by A6, CARD_1:106 ;
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: for i being Element of NAT st i < k9 holds
i in dom (aSeq (a,k9)) by A8, NAT_1:45;
A13: s . (c0 + 0) = (aSeq (a,k9)) . 0 by A5, A4, A10
.= a := (intloc 0) by A7, AFINSQ_1:39 ;

A14: now

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A15: 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 A2, A13, 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 A2, A13, A15, COMPOS_1:38 ; :: thesis:

end;

A16: 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, A6, 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, A7, TT, A6, A18, AFINSQ_1:21
.= 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 by A22, NAT_1:13;
thus s . (c0 + i) = (aSeq (a,k9)) . i by A4, A10, A23
.= AddTo (a,(intloc 0)) by A16, A24, A23 ; :: 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:

A31: n < k9 by A27, NAT_1:13;
Y: (ProgramPart (Comput ((ProgramPart s),s,n))) /. (IC (Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . (IC (Comput ((ProgramPart s),s,n))) by COMPOS_1:38;
A32: n + 0 <= n + 1 by XREAL_1:9;
then A33: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = s . (c0 + n) by A26, A27, Y, AMI_1:54, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A21, A30, A31 ;
A34: Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((AddTo (a,(intloc 0))),(Comput ((ProgramPart s),s,n))) by A33, AMI_1:123 ;
hence IC (Comput ((ProgramPart s),s,(n + 1))) = succ (IC (Comput ((ProgramPart s),s,n))) by SCMFSA_2:90
.= (c0 + n) + 1 by A26, A27, A32, NAT_1:39, XXREAL_0:2
.= c0 + (n + 1) ;
:: thesis:
A35: 0 + 1 <= n by A30, INT_1:20;

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, EXTPRO_1:3;
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, AFINSQ_1:20
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:36
.= (mk + 1) + 1 by A40, CARD_1:106 ;
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: for i being Element of NAT st i < (mk + 1) + 1 holds
i in dom (aSeq (a,k)) by A42, NAT_1:45;
A47: s . (c0 + 0) = (aSeq (a,k)) . 0 by A4, A44
.= a := (intloc 0) by A41, AFINSQ_1:39 ;
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

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A49: 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 A2, A47, 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 A2, A47, A49, COMPOS_1:38 ; :: thesis:

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;
reconsider i1 = i - 1 as Element of NAT by A51, INT_1:18;
A55: i1 in k1 by A40, 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 A41, A51, TT, A40, A52, AFINSQ_1:21
.= 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 by A57, NAT_1:13;
thus s . (c0 + i) = (aSeq (a,k)) . i by A4, A44, A58
.= SubFrom (a,(intloc 0)) by A50, A59, A58 ; :: 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, EXTPRO_1:3;
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;