let c0 be Element of NAT ; :: thesis: for s being c0 -started State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let s be c0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

A1: dom P = NAT by PARTFUN1:def 2;

A2: IC s = c0 by MEMSTR_0:def 12;

let a be Int-Location; :: thesis: for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let k be Integer; :: thesis: ( ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) implies for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i )

assume A3: for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

A4: for c being Element of NAT st c in dom (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) by A3, AFINSQ_1:66;

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let s be c0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

A1: dom P = NAT by PARTFUN1:def 2;

A2: IC s = c0 by MEMSTR_0:def 12;

let a be Int-Location; :: thesis: for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

let k be Integer; :: thesis: ( ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) implies for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i )

assume A3: for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

A4: for c being Element of NAT st c in dom (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) by A3, AFINSQ_1:66;

per cases
( k > 0 or k <= 0 )
;

end;

suppose A5:
k > 0
; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

IC (Comput (P,s,i)) = c0 + i

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, SCMFSA_7:def 2;

defpred S_{1}[ Nat] means ( $1 <= k9 implies IC (Comput (P,s,$1)) = c0 + $1 );

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:34

.= k9 by A6 ;

for i being Element of NAT st i <= len (aSeq (a,k9)) holds

IC (Comput (P,s,i)) = c0 + i

IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum

end;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, SCMFSA_7:def 2;

defpred S

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:34

.= k9 by A6 ;

for i being Element of NAT st i <= len (aSeq (a,k9)) holds

IC (Comput (P,s,i)) = c0 + i

proof

i in dom (aSeq (a,k9)) by A8, AFINSQ_1:86;

.= a := (intloc 0) by A7, AFINSQ_1:35 ;

_{1}[n] holds

S_{1}[n + 1]

assume A32: i <= len (aSeq (a,k9)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i

A33: S_{1}[ 0 ]
by A2;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A33, A23);

hence IC (Comput (P,s,i)) = c0 + i by A8, A32; :: thesis: verum

end;

hence
for i being Element of NAT st i <= len (aSeq (a,k)) holds A9: now :: thesis: for i being Element of NAT st 1 <= i & i < k9 holds

(aSeq (a,k9)) . i = AddTo (a,(intloc 0))

A14:
for i being Element of NAT st i < k9 holds (aSeq (a,k9)) . i = AddTo (a,(intloc 0))

let i be Element of NAT ; :: thesis: ( 1 <= i & i < k9 implies (aSeq (a,k9)) . i = AddTo (a,(intloc 0)) )

assume that

A10: 1 <= i and

A11: i < k9 ; :: thesis: (aSeq (a,k9)) . i = AddTo (a,(intloc 0))

reconsider i1 = i - 1 as Element of NAT by A10, INT_1:5;

i = i1 + 1 ;

then i1 < k1 by A11, A6, XREAL_1:6;

then A12: i1 in Segm k1 by NAT_1:44;

A13: 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 A10, A7, A13, A6, A11, AFINSQ_1:18

.= AddTo (a,(intloc 0)) by A12, FUNCOP_1:7 ;

:: thesis: verum

end;assume that

A10: 1 <= i and

A11: i < k9 ; :: thesis: (aSeq (a,k9)) . i = AddTo (a,(intloc 0))

reconsider i1 = i - 1 as Element of NAT by A10, INT_1:5;

i = i1 + 1 ;

then i1 < k1 by A11, A6, XREAL_1:6;

then A12: i1 in Segm k1 by NAT_1:44;

A13: 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 A10, A7, A13, A6, A11, AFINSQ_1:18

.= AddTo (a,(intloc 0)) by A12, FUNCOP_1:7 ;

:: thesis: verum

i in dom (aSeq (a,k9)) by A8, AFINSQ_1:86;

A15: now :: thesis: for i being Nat st 0 < i & i < k9 holds

P . (c0 + i) = AddTo (a,(intloc 0))

A20: P . (c0 + 0) =
(aSeq (a,k9)) . 0
by A3, A5, A8
P . (c0 + i) = AddTo (a,(intloc 0))

let i be Nat; :: thesis: ( 0 < i & i < k9 implies P . (c0 + i) = AddTo (a,(intloc 0)) )

assume that

A16: 0 < i and

A17: i < k9 ; :: thesis: P . (c0 + i) = AddTo (a,(intloc 0))

A18: 0 + 1 <= i by A16, NAT_1:13;

A19: i in NAT by ORDINAL1:def 12;

hence P . (c0 + i) = (aSeq (a,k9)) . i by A4, A14, A17

.= AddTo (a,(intloc 0)) by A9, A18, A17, A19 ;

:: thesis: verum

end;assume that

A16: 0 < i and

A17: i < k9 ; :: thesis: P . (c0 + i) = AddTo (a,(intloc 0))

A18: 0 + 1 <= i by A16, NAT_1:13;

A19: i in NAT by ORDINAL1:def 12;

hence P . (c0 + i) = (aSeq (a,k9)) . i by A4, A14, A17

.= AddTo (a,(intloc 0)) by A9, A18, A17, A19 ;

:: thesis: verum

.= a := (intloc 0) by A7, AFINSQ_1:35 ;

A21: now :: thesis: 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) )

A23:
for n being Nat st S( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )

assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

hence A22: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6

.= a := (intloc 0) by A20, A22, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)

thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3

.= Exec ((a := (intloc 0)),s) by A22, A2, A20, A1, PARTFUN1:def 6 ; :: thesis: verum

end;assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

hence A22: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6

.= a := (intloc 0) by A20, A22, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)

thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3

.= Exec ((a := (intloc 0)),s) by A22, A2, A20, A1, PARTFUN1:def 6 ; :: thesis: verum

S

proof

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (a,k9)) implies IC (Comput (P,s,i)) = c0 + i )
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A24: S_{1}[n]
; :: thesis: S_{1}[n + 1]

assume A25: n + 1 <= k9 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

end;assume A24: S

assume A25: n + 1 <= k9 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

per cases
( n = 0 or n > 0 )
;

end;

suppose A26:
n = 0
; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

hence IC (Comput (P,s,(n + 1))) =
(Exec ((a := (intloc 0)),s)) . (IC )
by A21

.= (c0 + 1) + n by A2, A26, SCMFSA_2:63

.= c0 + (n + 1) ;

:: thesis: verum

end;.= (c0 + 1) + n by A2, A26, SCMFSA_2:63

.= c0 + (n + 1) ;

:: thesis: verum

suppose A27:
n > 0
; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

A28:
n < k9
by A25, NAT_1:13;

A29: n + 0 <= n + 1 by XREAL_1:7;

A30: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, A29, A1, PARTFUN1:def 6, XXREAL_0:2

.= AddTo (a,(intloc 0)) by A15, A27, A28 ;

A31: 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 A30 ;

thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A31, SCMFSA_2:64

.= (c0 + n) + 1 by A24, A25, A29, XXREAL_0:2

.= c0 + (n + 1) ; :: thesis: verum

end;A29: n + 0 <= n + 1 by XREAL_1:7;

A30: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, A29, A1, PARTFUN1:def 6, XXREAL_0:2

.= AddTo (a,(intloc 0)) by A15, A27, A28 ;

A31: 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 A30 ;

thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A31, SCMFSA_2:64

.= (c0 + n) + 1 by A24, A25, A29, XXREAL_0:2

.= c0 + (n + 1) ; :: thesis: verum

assume A32: i <= len (aSeq (a,k9)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i

A33: S

for i being Nat holds S

hence IC (Comput (P,s,i)) = c0 + i by A8, A32; :: thesis: verum

IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum

suppose A34:
k <= 0
; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

IC (Comput (P,s,i)) = c0 + i

then reconsider mk = - k as Element of NAT by INT_1:3;

defpred S_{1}[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (P,s,$1)) = c0 + $1 );

consider k1 being Nat such that

A35: k1 + k = 1 and

A36: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A34, SCMFSA_7:def 2;

A37: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A36, AFINSQ_1:17

.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:34

.= (mk + 1) + 1 by A35 ;

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum

end;defpred S

consider k1 being Nat such that

A35: k1 + k = 1 and

A36: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A34, SCMFSA_7:def 2;

A37: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A36, AFINSQ_1:17

.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:34

.= (mk + 1) + 1 by A35 ;

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

proof

i in dom (aSeq (a,k)) by A37, AFINSQ_1:86;

.= a := (intloc 0) by A36, AFINSQ_1:35 ;

A51: 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) )_{1}[n] holds

S_{1}[n + 1]

assume A62: i <= len (aSeq (a,k)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i

A63: S_{1}[ 0 ]
by A2;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A63, A53);

hence IC (Comput (P,s,i)) = c0 + i by A37, A62; :: thesis: verum

end;

hence
for i being Element of NAT st i <= len (aSeq (a,k)) holds A38: now :: thesis: for i being Element of NAT st 1 <= i & i < (mk + 1) + 1 holds

(aSeq (a,k)) . i = SubFrom (a,(intloc 0))

A44:
for i being Element of NAT st i < (mk + 1) + 1 holds (aSeq (a,k)) . i = SubFrom (a,(intloc 0))

let i be Element of NAT ; :: thesis: ( 1 <= i & i < (mk + 1) + 1 implies (aSeq (a,k)) . i = SubFrom (a,(intloc 0)) )

assume that

A39: 1 <= i and

A40: i < (mk + 1) + 1 ; :: thesis: (aSeq (a,k)) . i = SubFrom (a,(intloc 0))

A41: i - 1 < ((mk + 1) + 1) - 1 by A40, XREAL_1:9;

reconsider i1 = i - 1 as Element of NAT by A39, INT_1:5;

A42: i1 in Segm k1 by A35, A41, NAT_1:44;

A43: 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 A36, A39, A43, A35, A40, AFINSQ_1:18

.= SubFrom (a,(intloc 0)) by A42, FUNCOP_1:7 ;

:: thesis: verum

end;assume that

A39: 1 <= i and

A40: i < (mk + 1) + 1 ; :: thesis: (aSeq (a,k)) . i = SubFrom (a,(intloc 0))

A41: i - 1 < ((mk + 1) + 1) - 1 by A40, XREAL_1:9;

reconsider i1 = i - 1 as Element of NAT by A39, INT_1:5;

A42: i1 in Segm k1 by A35, A41, NAT_1:44;

A43: 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 A36, A39, A43, A35, A40, AFINSQ_1:18

.= SubFrom (a,(intloc 0)) by A42, FUNCOP_1:7 ;

:: thesis: verum

i in dom (aSeq (a,k)) by A37, AFINSQ_1:86;

A45: now :: thesis: for i being Nat st 0 < i & i < (mk + 1) + 1 holds

P . (c0 + i) = SubFrom (a,(intloc 0))

A50: P . (c0 + 0) =
(aSeq (a,k)) . 0
by A3, A37
P . (c0 + i) = SubFrom (a,(intloc 0))

let i be Nat; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies P . (c0 + i) = SubFrom (a,(intloc 0)) )

assume that

A46: 0 < i and

A47: i < (mk + 1) + 1 ; :: thesis: P . (c0 + i) = SubFrom (a,(intloc 0))

A48: 0 + 1 <= i by A46, NAT_1:13;

A49: i in NAT by ORDINAL1:def 12;

hence P . (c0 + i) = (aSeq (a,k)) . i by A4, A44, A47

.= SubFrom (a,(intloc 0)) by A38, A48, A47, A49 ;

:: thesis: verum

end;assume that

A46: 0 < i and

A47: i < (mk + 1) + 1 ; :: thesis: P . (c0 + i) = SubFrom (a,(intloc 0))

A48: 0 + 1 <= i by A46, NAT_1:13;

A49: i in NAT by ORDINAL1:def 12;

hence P . (c0 + i) = (aSeq (a,k)) . i by A4, A44, A47

.= SubFrom (a,(intloc 0)) by A38, A48, A47, A49 ;

:: thesis: verum

.= a := (intloc 0) by A36, AFINSQ_1:35 ;

A51: 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

A53:
for n being Nat st S
let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )

assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

hence A52: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6

.= a := (intloc 0) by A50, A52, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)

thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3

.= Exec ((a := (intloc 0)),s) by A52, A2, A50, A1, PARTFUN1:def 6 ; :: thesis: verum

end;assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

hence A52: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )

thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6

.= a := (intloc 0) by A50, A52, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)

thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3

.= Exec ((a := (intloc 0)),s) by A52, A2, A50, A1, PARTFUN1:def 6 ; :: thesis: verum

S

proof

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (a,k)) implies IC (Comput (P,s,i)) = c0 + i )
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A54: S_{1}[n]
; :: thesis: S_{1}[n + 1]

assume A55: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

end;assume A54: S

assume A55: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

per cases
( n = 0 or n > 0 )
;

end;

suppose A56:
n = 0
; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

hence IC (Comput (P,s,(n + 1))) =
(Exec ((a := (intloc 0)),s)) . (IC )
by A51

.= (c0 + n) + 1 by A2, A56, SCMFSA_2:63

.= c0 + (n + 1) ;

:: thesis: verum

end;.= (c0 + n) + 1 by A2, A56, SCMFSA_2:63

.= c0 + (n + 1) ;

:: thesis: verum

suppose A57:
n > 0
; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)

A58:
n < (mk + 1) + 1
by A55, NAT_1:13;

A59: n + 0 <= n + 1 by XREAL_1:7;

A60: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A54, A55, A59, A1, PARTFUN1:def 6, XXREAL_0:2

.= SubFrom (a,(intloc 0)) by A45, A57, A58 ;

A61: 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 A60 ;

thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A61, SCMFSA_2:65

.= (c0 + n) + 1 by A54, A55, A59, XXREAL_0:2

.= c0 + (n + 1) ; :: thesis: verum

end;A59: n + 0 <= n + 1 by XREAL_1:7;

A60: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A54, A55, A59, A1, PARTFUN1:def 6, XXREAL_0:2

.= SubFrom (a,(intloc 0)) by A45, A57, A58 ;

A61: 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 A60 ;

thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A61, SCMFSA_2:65

.= (c0 + n) + 1 by A54, A55, A59, XXREAL_0:2

.= c0 + (n + 1) ; :: thesis: verum

assume A62: i <= len (aSeq (a,k)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i

A63: S

for i being Nat holds S

hence IC (Comput (P,s,i)) = c0 + i by A37, A62; :: thesis: verum

IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum