let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
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 MEMSTR_0:def 8;
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 = P . (c0 + c) ; :: thesis:

suppose A5: k > 0 ; :: thesis:

then reconsider k9 = k as Element of NAT by INT_1:3;
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 (P,s,$1)) = c0 + $1 & ( 1 <= $1 implies (Comput (P,s,$1)) . a = $1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) );
A8: len (aSeq (a,k9)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by A7, AFINSQ_1:17
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:33
.= k9 by A6, CARD_1:64 ;
A9: for i being Element of NAT st i <= len (aSeq (a,k9)) holds
( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = i ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,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:44;
A11: P . (c0 + 0) = (aSeq (a,k9)) . 0 by A5, A4, A10
.= a := (intloc 0) by A7, AFINSQ_1:35 ;

A12: now

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A13: Comput (P,s,n) = s by EXTPRO_1:2; :: thesis:
hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A2, A11, PBOOLE:143; :: thesis:
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A2, A11, A13, PBOOLE:143 ; :: thesis:

end;

A14: now

let i be Element of NAT ; :: thesis:
assume that
A15: 1 <= i and
A16: i < k9 ; :: thesis:
reconsider i1 = i - 1 as Element of NAT by A15, INT_1:5;
i = i1 + 1 ;
then i1 < k1 by A16, A6, XREAL_1:6;
then A17: i1 in k1 by NAT_1:44;
A18: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:64;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
hence (aSeq (a,k9)) . i = (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A15, A7, A18, A6, A16, AFINSQ_1:18
.= AddTo (a,(intloc 0)) by A17, FUNCOP_1:7 ;
:: thesis:

end;

A19: now

let i be Element of NAT ; :: thesis:
assume that
A20: 0 < i and
A21: i < k9 ; :: thesis:
A22: 0 + 1 <= i by A20, NAT_1:13;
thus P . (c0 + i) = (aSeq (a,k9)) . i by A4, A10, A21
.= AddTo (a,(intloc 0)) by A14, A22, A21 ; :: thesis:

end;

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

proof

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

per cases ;

suppose A26: n = 0 ; :: thesis:

hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A12
.= succ (c0 + n) by A2, A26, SCMFSA_2:63
.= (c0 + n) + 1 by NAT_1:38
.= c0 + (n + 1) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A12, A26
.= n + 1 by A1, A26, SCMFSA_2:63 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A27: b <> a ; :: thesis:
thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A12, A26
.= s . b by A27, SCMFSA_2:63 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A12, A26
.= s . f by SCMFSA_2:63 ; :: thesis:

end;

suppose A28: n > 0 ; :: thesis:

A29: n < k9 by A25, NAT_1:13;
A30: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143;
A31: n + 0 <= n + 1 by XREAL_1:7;
then A32: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, A30, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A19, A28, A29 ;
A33: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((AddTo (a,(intloc 0))),(Comput (P,s,n))) by A32 ;
hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:64
.= (c0 + n) + 1 by A24, A25, A31, NAT_1:38, XXREAL_0:2
.= c0 + (n + 1) ;
:: thesis:
A34: 0 + 1 <= n by A28, INT_1:7;

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (P,s,(n + 1))) . a = n + ((Comput (P,s,n)) . (intloc 0)) by A24, A25, A34, A31, A33, SCMFSA_2:64, XXREAL_0:2
.= n + 1 by A1, A3, A24, A25, A31, XXREAL_0:2 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A35: b <> a ; :: thesis:
hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A33, SCMFSA_2:64
.= s . b by A24, A25, A31, A35, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A33, SCMFSA_2:64
.= s . f by A24, A25, A31, XXREAL_0:2 ; :: thesis:

end;

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

end;

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

end;

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

then reconsider mk = - k as Element of NAT by INT_1:3;
defpred S₁[ Nat] means ( $1 <= (mk + 1) + 1 implies ( IC (Comput (P,s,$1)) = c0 + $1 & ( 1 <= $1 implies (Comput (P,s,$1)) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) );
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, AFINSQ_1:17
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33
.= (mk + 1) + 1 by A39, CARD_1:64 ;
A42: for i being Element of NAT st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) )

proof

A43: for i being Element of NAT st i < (mk + 1) + 1 holds
i in dom (aSeq (a,k)) by A41, NAT_1:44;
A44: P . (c0 + 0) = (aSeq (a,k)) . 0 by A4, A43
.= a := (intloc 0) by A40, AFINSQ_1:35 ;
A45: for n being Element of NAT st n = 0 holds
( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

proof

let n be Element of NAT ; :: thesis:
assume n = 0 ; :: thesis:
hence A46: Comput (P,s,n) = s by EXTPRO_1:2; :: thesis:
hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A2, A44, PBOOLE:143; :: thesis:
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A2, A44, A46, PBOOLE:143 ; :: thesis:

end;

A47: now

let i be Element of NAT ; :: thesis:
assume that
A48: 1 <= i and
A49: i < (mk + 1) + 1 ; :: thesis:
A50: i - 1 < ((mk + 1) + 1) - 1 by A49, XREAL_1:9;
reconsider i1 = i - 1 as Element of NAT by A48, INT_1:5;
A51: i1 in k1 by A39, A50, NAT_1:44;
A52: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:64;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
hence (aSeq (a,k)) . i = (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A40, A48, A52, A39, A49, AFINSQ_1:18
.= SubFrom (a,(intloc 0)) by A51, FUNCOP_1:7 ;
:: thesis:

end;

A53: now

let i be Element of NAT ; :: thesis:
assume that
A54: 0 < i and
A55: i < (mk + 1) + 1 ; :: thesis:
A56: 0 + 1 <= i by A54, NAT_1:13;
thus P . (c0 + i) = (aSeq (a,k)) . i by A4, A43, A55
.= SubFrom (a,(intloc 0)) by A47, A56, A55 ; :: thesis:

end;

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

proof

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

per cases ;

suppose A60: n = 0 ; :: thesis:

hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A45
.= succ (c0 + n) by A2, A60, SCMFSA_2:63
.= (c0 + n) + 1 by NAT_1:38
.= c0 + (n + 1) ;
:: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A45, A60
.= ((- (n + 1)) + 1) + 1 by A1, A60, SCMFSA_2:63 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A61: b <> a ; :: thesis:
thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A45, A60
.= s . b by A61, SCMFSA_2:63 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A45, A60
.= s . f by SCMFSA_2:63 ; :: thesis:

end;

suppose A62: n > 0 ; :: thesis:

A63: n < (mk + 1) + 1 by A59, NAT_1:13;
A64: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143;
A65: n + 0 <= n + 1 by XREAL_1:7;
then A66: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A58, A59, A64, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A53, A62, A63 ;
A67: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((SubFrom (a,(intloc 0))),(Comput (P,s,n))) by A66 ;
hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:65
.= (c0 + n) + 1 by A58, A59, A65, NAT_1:38, XXREAL_0:2
.= c0 + (n + 1) ;
:: thesis:
A68: 0 + 1 < n + 1 by A62, XREAL_1:6;

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (P,s,(n + 1))) . a = (((- n) + 1) + 1) - ((Comput (P,s,n)) . (intloc 0)) by A58, A59, A68, A67, NAT_1:13, SCMFSA_2:65
.= (((- n) + 1) + 1) - (s . (intloc 0)) by A3, A58, A59, A65, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A1 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A69: b <> a ; :: thesis:
hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A67, SCMFSA_2:65
.= s . b by A58, A59, A65, A69, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A67, SCMFSA_2:65
.= s . f by A58, A59, A65, XXREAL_0:2 ; :: thesis:

end;

A70: S₁[ 0 ] by A2, EXTPRO_1:2;
A71: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A70, A57);
let i be Element of NAT ; :: thesis:
assume i <= len (aSeq (a,k)) ; :: thesis:
hence ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) by A41, A71; :: thesis:

end;

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

end;