let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let c0 be 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 11;
let a be Int-Location; :: thesis:
let k be Integer; :: thesis:
assume that
A3: a <> intloc 0 and
A4: for c being 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 Nat such that
A6: k1 + 1 = k9 and
A7: aSeq (a,k9) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) by A5, Def2;
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 ;
A9: for i being 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 Nat st i < k9 holds
i in dom (aSeq (a,k9)) by A8, AFINSQ_1:86;
A11: P . (c0 + 0) = (aSeq (a,k9)) . 0 by A5, A4, A10
.= a := (intloc 0) by A7, AFINSQ_1:35 ;

A12: now :: thesis:

let n be 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 :: thesis:

let i be 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 Segm k1 by NAT_1:44;
A18: len (k1 --> (AddTo (a,(intloc 0)))) = k1 ;
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 :: thesis:

let i be 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 Nat st S₁[n] holds
S₁[n + 1]

proof

let n be 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
.= c0 + (n + 1) by A2, A26, SCMFSA_2:63 ;
:: 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: n + 0 <= n + 1 by XREAL_1:7;
then A31: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, PBOOLE:143, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A19, A28, A29 ;
A32: 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 A31 ;
hence IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by SCMFSA_2:64
.= c0 + (n + 1) by A24, A25, A30, XXREAL_0:2 ;
:: thesis:
A33: 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, A33, A30, A32, SCMFSA_2:64, XXREAL_0:2
.= n + 1 by A1, A3, A24, A25, A30, XXREAL_0:2 ; :: thesis:

end;

hereby :: thesis:

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

end;

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

end;

A35: S₁[ 0 ] by A2, EXTPRO_1:2;
A36: for i being Nat holds S₁[i] from NAT_1:sch 2(A35, A23);
let i be 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, A36; :: thesis:

end;

hence for i being 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 A37: 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 Nat such that
A38: k1 + k = 1 and
A39: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A37, Def2;
A40: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A39, AFINSQ_1:17
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33
.= (mk + 1) + 1 by A38 ;
A41: for i being 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

A42: for i being Nat st i < (mk + 1) + 1 holds
i in dom (aSeq (a,k)) by A40, AFINSQ_1:86;
A43: P . (c0 + 0) = (aSeq (a,k)) . 0 by A4, A42
.= a := (intloc 0) by A39, AFINSQ_1:35 ;
A44: for n being 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 Nat; :: thesis:
assume n = 0 ; :: thesis:
hence A45: Comput (P,s,n) = s by EXTPRO_1:2; :: thesis:
hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A2, A43, 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, A43, A45, PBOOLE:143 ; :: thesis:

end;

A46: now :: thesis:

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

end;

A52: now :: thesis:

let i be Nat; :: thesis:
assume that
A53: 0 < i and
A54: i < (mk + 1) + 1 ; :: thesis:
A55: 0 + 1 <= i by A53, NAT_1:13;
thus P . (c0 + i) = (aSeq (a,k)) . i by A4, A42, A54
.= SubFrom (a,(intloc 0)) by A46, A55, A54 ; :: thesis:

end;

A56: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A57: S₁[n] ; :: thesis:
assume A58: n + 1 <= (mk + 1) + 1 ; :: thesis:

per cases ;

suppose A59: n = 0 ; :: thesis:

hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A44
.= c0 + (n + 1) by A2, A59, SCMFSA_2:63 ;
:: thesis:

hereby :: thesis:

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

end;

hereby :: thesis:

let b be Int-Location; :: thesis:
assume A60: b <> a ; :: thesis:
thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A44, A59
.= s . b by A60, 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 A44, A59
.= s . f by SCMFSA_2:63 ; :: thesis:

end;

suppose A61: n > 0 ; :: thesis:

A62: n < (mk + 1) + 1 by A58, NAT_1:13;
A63: n + 0 <= n + 1 by XREAL_1:7;
then A64: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A57, A58, PBOOLE:143, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A52, A61, A62 ;
A65: 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 A64 ;
hence IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by SCMFSA_2:65
.= c0 + (n + 1) by A57, A58, A63, XXREAL_0:2 ;
:: thesis:
A66: 0 + 1 < n + 1 by A61, 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 A57, A58, A66, A65, NAT_1:13, SCMFSA_2:65
.= (((- n) + 1) + 1) - (s . (intloc 0)) by A3, A57, A58, A63, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A1 ; :: thesis:

end;

hereby :: thesis:

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

end;

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

end;

A68: S₁[ 0 ] by A2, EXTPRO_1:2;
A69: for i being Nat holds S₁[i] from NAT_1:sch 2(A68, A56);
let i be 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 A40, A69; :: thesis:

end;

hence for i being 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 A40, NAT_1:11;
hence (Comput (P,s,(len (aSeq (a,k))))) . a = ((- ((- k) + (1 + 1))) + 1) + 1 by A40, A41
.= k ;
:: thesis:

end;