let m, n be Element of NAT ; :: thesis: for s, s1 being State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st s = Computation (s1 +* (Initialized (stop J))),m holds
Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
let s, s1 be State of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS st s = Computation (s1 +* (Initialized (stop J))),m holds
Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
let J be parahalting shiftable Program of SCMPDS ; :: thesis: ( s = Computation (s1 +* (Initialized (stop J))),m implies Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) )
set pJ = stop J;
set IsJ = Initialized (stop J);
set s2 = s1 +* (Initialized (stop J));
assume A1: s = Computation (s1 +* (Initialized (stop J))),m ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
set i = CurInstr s;
set ss = s +* (Start-At ((IC s) + n));
reconsider k = IC s as Element of NAT by ORDINAL1:def 13;
reconsider Nl = Next (IC s) as Instruction-Location of SCMPDS ;
A4: Next (IC (s +* (Start-At ((IC s) + n)))) = inspos ((k + n) + 1) by AMI_1:111
.= IC ((Exec (CurInstr s),s) +* (Start-At (Nl + n))) by AMI_1:111 ;
A5: IC (s +* (Start-At ((IC s) + n))) = (IC s) + n by AMI_1:111;
set IEn = (IC (Exec (CurInstr s),s)) + n;

A6: now

let d be Instruction-Location of SCMPDS ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . d
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . d = (s +* (Start-At ((IC s) + n))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (Exec (CurInstr s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . d by AMI_1:112 ; :: thesis: verum

end;

reconsider n1 = IC s as Element of NAT by ORDINAL1:def 13;
A7: IC s = inspos n1 ;
A8: Initialized (stop J) c= s1 +* (Initialized (stop J)) by FUNCT_4:26;
then A9: IC s in dom (stop J) by A1, SCMPDS_4:def 9;
stop J c= s by A1, A8, AMI_1:81, SCMPDS_4:57;
then CurInstr s = (stop J) . (inspos n1) by A9, GRFUNC_1:8;
then A10: ( InsCode (CurInstr s) <> 1 & InsCode (CurInstr s) <> 3 & CurInstr s valid_at n1 ) by A9, SCMPDS_4:def 12;

per cases ( InsCode (CurInstr s) = 0 or InsCode (CurInstr s) = 2 or InsCode (CurInstr s) = 4 or InsCode (CurInstr s) = 5 or InsCode (CurInstr s) = 6 or InsCode (CurInstr s) = 7 or InsCode (CurInstr s) = 8 or InsCode (CurInstr s) = 9 or InsCode (CurInstr s) = 10 or InsCode (CurInstr s) = 11 or InsCode (CurInstr s) = 12 or InsCode (CurInstr s) = 13 ) by A10, NAT_1:38, SCMPDS_2:15;

suppose InsCode (CurInstr s) = 0 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider k1 being Integer such that
A11: ( CurInstr s = goto k1 & n1 + k1 >= 0 ) by A10, SCMPDS_4:def 11;
A12: IC (Exec (CurInstr s),s) = ICplusConst s,k1 by A11, SCMPDS_2:66;
A13: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k1 by A11, SCMPDS_2:66
.= (IC (Exec (CurInstr s),s)) + n by A5, A7, A11, A12, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A11, SCMPDS_2:66
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A11, SCMPDS_2:66
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A13, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 2 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1 being Integer such that
A14: CurInstr s = a := k1 by SCMPDS_2:37;
IC (Exec (CurInstr s),s) = Nl by A14, SCMPDS_2:57;
then A15: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A14, SCMPDS_2:57;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( a = b or a <> b ) ;

suppose A16: a = b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = k1 by A14, SCMPDS_2:57
.= (Exec (CurInstr s),s) . b by A14, A16, SCMPDS_2:57
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A17: a <> b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A14, SCMPDS_2:57
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A14, A17, SCMPDS_2:57
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ;
:: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A15, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 4 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1, k2 being Integer such that
A18: ( CurInstr s = a,k1 <>0_goto k2 & n1 + k2 >= 0 ) by A10, SCMPDS_4:def 11;

A19: now

per cases ( s . (DataLoc (s . a),k1) <> 0 or s . (DataLoc (s . a),k1) = 0 ) ;

suppose A20: s . (DataLoc (s . a),k1) <> 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) <> 0 by SCMPDS_3:14;
then A21: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) <> 0 by SCMPDS_3:14;
A22: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A18, A20, SCMPDS_2:67;
thus IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A18, A21, SCMPDS_2:67
.= (IC (Exec (CurInstr s),s)) + n by A5, A7, A18, A22, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ; :: thesis: verum

end;

suppose A23: s . (DataLoc (s . a),k1) = 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) = 0 by SCMPDS_3:14;
then A24: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A18, A23, SCMPDS_2:67;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A18, A24, SCMPDS_2:67; :: thesis: verum

end;

end;

end;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A18, SCMPDS_2:67
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A18, SCMPDS_2:67
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A19, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 5 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1, k2 being Integer such that
A25: ( CurInstr s = a,k1 <=0_goto k2 & n1 + k2 >= 0 ) by A10, SCMPDS_4:def 11;

A26: now

per cases ( s . (DataLoc (s . a),k1) <= 0 or s . (DataLoc (s . a),k1) > 0 ) ;

suppose A27: s . (DataLoc (s . a),k1) <= 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) <= 0 by SCMPDS_3:14;
then A28: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) <= 0 by SCMPDS_3:14;
A29: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A25, A27, SCMPDS_2:68;
thus IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A25, A28, SCMPDS_2:68
.= (IC (Exec (CurInstr s),s)) + n by A5, A7, A25, A29, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ; :: thesis: verum

end;

suppose A30: s . (DataLoc (s . a),k1) > 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) > 0 by SCMPDS_3:14;
then A31: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) > 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A25, A30, SCMPDS_2:68;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A25, A31, SCMPDS_2:68; :: thesis: verum

end;

end;

end;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A25, SCMPDS_2:68
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A25, SCMPDS_2:68
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A26, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 6 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1, k2 being Integer such that
A32: ( CurInstr s = a,k1 >=0_goto k2 & n1 + k2 >= 0 ) by A10, SCMPDS_4:def 11;

A33: now

per cases ( s . (DataLoc (s . a),k1) >= 0 or s . (DataLoc (s . a),k1) < 0 ) ;

suppose A34: s . (DataLoc (s . a),k1) >= 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) >= 0 by SCMPDS_3:14;
then A35: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) >= 0 by SCMPDS_3:14;
A36: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A32, A34, SCMPDS_2:69;
thus IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A32, A35, SCMPDS_2:69
.= (IC (Exec (CurInstr s),s)) + n by A5, A7, A32, A36, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ; :: thesis: verum

end;

suppose A37: s . (DataLoc (s . a),k1) < 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) < 0 by SCMPDS_3:14;
then A38: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) < 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A32, A37, SCMPDS_2:69;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A32, A38, SCMPDS_2:69; :: thesis: verum

end;

end;

end;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A32, SCMPDS_2:69
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A32, SCMPDS_2:69
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A33, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 7 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1, k2 being Integer such that
A39: CurInstr s = a,k1 := k2 by SCMPDS_2:42;
IC (Exec (CurInstr s),s) = Nl by A39, SCMPDS_2:58;
then A40: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A39, SCMPDS_2:58;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ) ;

suppose A41: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A42: DataLoc (s . a),k1 = b by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = k2 by A39, A41, SCMPDS_2:58
.= (Exec (CurInstr s),s) . b by A39, A42, SCMPDS_2:58
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A43: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A44: DataLoc (s . a),k1 <> b by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A39, A43, SCMPDS_2:58
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A39, A44, SCMPDS_2:58
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A40, SCMPDS_2:54; :: thesis: verum
thus verum ; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 8 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a being Int_position , k1, k2 being Integer such that
A45: CurInstr s = AddTo a,k1,k2 by SCMPDS_2:43;
IC (Exec (CurInstr s),s) = Nl by A45, SCMPDS_2:60;
then A46: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A45, SCMPDS_2:60;

now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ) ;

suppose A47: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A48: DataLoc (s . a),k1 = b by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = ((s +* (Start-At ((IC s) + n))) . b) + k2 by A45, A47, SCMPDS_2:60
.= (s . b) + k2 by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A45, A48, SCMPDS_2:60
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A49: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A50: DataLoc (s . a),k1 <> b by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b = (s +* (Start-At ((IC s) + n))) . b by A45, A49, SCMPDS_2:60
.= s . b by SCMPDS_3:14
.= (Exec (CurInstr s),s) . b by A45, A50, SCMPDS_2:60
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A46, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 9 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a, b being Int_position , k1, k2 being Integer such that
A51: CurInstr s = AddTo a,k1,b,k2 by SCMPDS_2:44;
IC (Exec (CurInstr s),s) = Nl by A51, SCMPDS_2:61;
then A52: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A51, SCMPDS_2:61;

now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

suppose A53: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A54: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A55: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) + (s . (DataLoc (s . b),k2)) by A51, A53, A55, SCMPDS_2:61
.= (Exec (CurInstr s),s) . c by A51, A54, SCMPDS_2:61
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A56: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A57: DataLoc (s . a),k1 <> c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . c by A51, A56, SCMPDS_2:61
.= s . c by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A51, A57, SCMPDS_2:61
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A52, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 10 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a, b being Int_position , k1, k2 being Integer such that
A58: CurInstr s = SubFrom a,k1,b,k2 by SCMPDS_2:45;
IC (Exec (CurInstr s),s) = Nl by A58, SCMPDS_2:62;
then A59: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A58, SCMPDS_2:62;

now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

suppose A60: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A61: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A62: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) - (s . (DataLoc (s . b),k2)) by A58, A60, A62, SCMPDS_2:62
.= (Exec (CurInstr s),s) . c by A58, A61, SCMPDS_2:62
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A63: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A64: DataLoc (s . a),k1 <> c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . c by A58, A63, SCMPDS_2:62
.= s . c by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A58, A64, SCMPDS_2:62
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A59, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 11 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a, b being Int_position , k1, k2 being Integer such that
A65: CurInstr s = MultBy a,k1,b,k2 by SCMPDS_2:46;
IC (Exec (CurInstr s),s) = Nl by A65, SCMPDS_2:63;
then A66: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A65, SCMPDS_2:63;

now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

suppose A67: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A68: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A69: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) * (s . (DataLoc (s . b),k2)) by A65, A67, A69, SCMPDS_2:63
.= (Exec (CurInstr s),s) . c by A65, A68, SCMPDS_2:63
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A70: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A71: DataLoc (s . a),k1 <> c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . c by A65, A70, SCMPDS_2:63
.= s . c by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A65, A71, SCMPDS_2:63
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A66, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 12 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a, b being Int_position , k1, k2 being Integer such that
A72: CurInstr s = Divide a,k1,b,k2 by SCMPDS_2:47;
IC (Exec (CurInstr s),s) = Nl by A72, SCMPDS_2:64;
then A73: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A72, SCMPDS_2:64;

now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁
A74: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
A75: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 <> c ) ;

suppose A76: DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A77: DataLoc (s . b),k2 = c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) mod (s . (DataLoc (s . b),k2)) by A72, A74, A75, A76, SCMPDS_2:64
.= (Exec (CurInstr s),s) . c by A72, A77, SCMPDS_2:64
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A78: DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A79: DataLoc (s . b),k2 <> c by SCMPDS_3:14;

hereby :: thesis: verum

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ) ;

suppose A80: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c

then A81: DataLoc (s . a),k1 <> c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . c by A72, A78, A80, SCMPDS_2:64
.= s . c by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A72, A79, A81, SCMPDS_2:64
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A82: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c

then A83: DataLoc (s . a),k1 = c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) div (s . (DataLoc (s . b),k2)) by A72, A74, A75, A78, A82, SCMPDS_2:64
.= (Exec (CurInstr s),s) . c by A72, A79, A83, SCMPDS_2:64
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A73, SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 13 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

then consider a, b being Int_position , k1, k2 being Integer such that
A84: CurInstr s = a,k1 := b,k2 by SCMPDS_2:48;
IC (Exec (CurInstr s),s) = Nl by A84, SCMPDS_2:59;
then A85: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A4, A84, SCMPDS_2:59;

now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

suppose A86: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A87: DataLoc (s . a),k1 = c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by A84, A86, SCMPDS_2:59
.= s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A84, A87, SCMPDS_2:59
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A88: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

then A89: DataLoc (s . a),k1 <> c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . c by A84, A88, SCMPDS_2:59
.= s . c by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A84, A89, SCMPDS_2:59
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

end;

end;

hence Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) by A6, A85, SCMPDS_2:54; :: thesis: verum

end;

end;