let m, n be Nat; :: thesis:
let P, P1 be Instruction-Sequence of SCMPDS; :: thesis:
let s be State of SCMPDS; :: thesis:
let s1 be 0 -started State of SCMPDS; :: thesis:
let J be parahalting shiftable Program of ; :: thesis:
set pJ = stop J;
set s2 = s1;
set P2 = P1 +* (stop J);
set i = CurInstr (P,s);
set ss = s +* (Start-At (((IC s) + n),SCMPDS));
reconsider k = IC s as Element of NAT ;
reconsider Nl = (IC s) + 1 as Element of NAT ;
A1: (IC (s +* (Start-At (((IC s) + n),SCMPDS)))) + 1 = (k + n) + 1 by FUNCT_4:113
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At ((Nl + n),SCMPDS))) by FUNCT_4:113 ;
assume A2: stop J c= P ; :: thesis:
assume A3: s = Comput ((P1 +* (stop J)),s1,m) ; :: thesis:
stop J c= P1 +* (stop J) by FUNCT_4:25;
then A4: IC s in dom (stop J) by A3, SCMPDS_4:def 6;
reconsider n1 = IC s as Nat ;
set IEn = (IC (Exec ((CurInstr (P,s)),s))) + n;
A5: IC (s +* (Start-At (((IC s) + n),SCMPDS))) = (IC s) + n by FUNCT_4:113;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: CurInstr (P,s) = (stop J) . n1 by A4, A6, A2, GRFUNC_1:2;
then A8: InsCode (CurInstr (P,s)) <> 1 by A4, SCMPDS_4:def 9;
A9: CurInstr (P,s) valid_at n1 by A4, A7, SCMPDS_4:def 9;
A10: InsCode (CurInstr (P,s)) <> 3 by A4, A7, SCMPDS_4:def 9;
InsCode (CurInstr (P,s)) <= 14 by SCMPDS_2:6;
then not not InsCode (CurInstr (P,s)) = 0 & ... & not InsCode (CurInstr (P,s)) = 14 ;

per cases by A8, A10;

suppose A11: InsCode (CurInstr (P,s)) = 0 ; :: thesis:

A12: Following (P,s) = s by A11, SCMPDS_2:86;
thus Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC (s,n) by A11, SCMPDS_2:86
.= IncIC ((Following (P,s)),n) by A12 ; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 14 ; :: thesis:

then consider k1 being Integer such that
A13: CurInstr (P,s) = goto k1 and
A14: n1 + k1 >= 0 by A9;
A15: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k1) by A13, SCMPDS_2:54;

A16: now :: thesis:

let b be Int_position; :: thesis:
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A13, SCMPDS_2:54
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A13, SCMPDS_2:54
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k1) by A13, SCMPDS_2:54
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A14, A15, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A16, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 2 ; :: thesis:

then consider a being Int_position, k1 being Integer such that
A17: CurInstr (P,s) = a := k1 by SCMPDS_2:28;

A18: now :: thesis:

let b be Int_position; :: thesis:

per cases ;

suppose A19: a = b ; :: thesis:

hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = k1 by A17, SCMPDS_2:45
.= (Exec ((CurInstr (P,s)),s)) . b by A17, A19, SCMPDS_2:45
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ;
:: thesis:

end;

suppose A20: a <> b ; :: thesis:

hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A17, SCMPDS_2:45
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A17, A20, SCMPDS_2:45
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ;
:: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A17, SCMPDS_2:45;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A17, SCMPDS_2:45;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A18, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 4 ; :: thesis:

then consider a being Int_position, k1, k2 being Integer such that
A21: CurInstr (P,s) = (a,k1) <>0_goto k2 and
A22: n1 + k2 >= 0 by A9;

A23: now :: thesis:

per cases ;

suppose A24: s . (DataLoc ((s . a),k1)) <> 0 ; :: thesis:

then A25: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A21, SCMPDS_2:55;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <> 0 by A24, SCMPDS_3:6;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <> 0 by SCMPDS_3:6;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A21, SCMPDS_2:55
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A22, A25, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A26: s . (DataLoc ((s . a),k1)) = 0 ; :: thesis:

then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) = 0 by SCMPDS_3:6;
then A27: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = 0 by SCMPDS_3:6;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A21, A26, SCMPDS_2:55;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A21, A27, SCMPDS_2:55; :: thesis:

end;

now :: thesis:

let b be Int_position; :: thesis:
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A21, SCMPDS_2:55
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A21, SCMPDS_2:55
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A23, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 5 ; :: thesis:

then consider a being Int_position, k1, k2 being Integer such that
A28: CurInstr (P,s) = (a,k1) <=0_goto k2 and
A29: n1 + k2 >= 0 by A9;

A30: now :: thesis:

per cases ;

suppose A31: s . (DataLoc ((s . a),k1)) <= 0 ; :: thesis:

then A32: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A28, SCMPDS_2:56;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <= 0 by A31, SCMPDS_3:6;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <= 0 by SCMPDS_3:6;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A28, SCMPDS_2:56
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A29, A32, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A33: s . (DataLoc ((s . a),k1)) > 0 ; :: thesis:

then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) > 0 by SCMPDS_3:6;
then A34: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) > 0 by SCMPDS_3:6;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A28, A33, SCMPDS_2:56;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A28, A34, SCMPDS_2:56; :: thesis:

end;

now :: thesis:

let b be Int_position; :: thesis:
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A28, SCMPDS_2:56
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A28, SCMPDS_2:56
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A30, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 6 ; :: thesis:

then consider a being Int_position, k1, k2 being Integer such that
A35: CurInstr (P,s) = (a,k1) >=0_goto k2 and
A36: n1 + k2 >= 0 by A9;

A37: now :: thesis:

per cases ;

suppose A38: s . (DataLoc ((s . a),k1)) >= 0 ; :: thesis:

then A39: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A35, SCMPDS_2:57;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) >= 0 by A38, SCMPDS_3:6;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) >= 0 by SCMPDS_3:6;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A35, SCMPDS_2:57
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A36, A39, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A40: s . (DataLoc ((s . a),k1)) < 0 ; :: thesis:

then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) < 0 by SCMPDS_3:6;
then A41: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) < 0 by SCMPDS_3:6;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A35, A40, SCMPDS_2:57;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A35, A41, SCMPDS_2:57; :: thesis:

end;

now :: thesis:

let b be Int_position; :: thesis:
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A35, SCMPDS_2:57
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A35, SCMPDS_2:57
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A37, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 7 ; :: thesis:

then consider a being Int_position, k1, k2 being Integer such that
A42: CurInstr (P,s) = (a,k1) := k2 by SCMPDS_2:33;

A43: now :: thesis:

let b be Int_position; :: thesis:

per cases ;

suppose A44: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b ; :: thesis:

then A45: DataLoc ((s . a),k1) = b by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = k2 by A42, A44, SCMPDS_2:46
.= (Exec ((CurInstr (P,s)),s)) . b by A42, A45, SCMPDS_2:46
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

suppose A46: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ; :: thesis:

then A47: DataLoc ((s . a),k1) <> b by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A42, A46, SCMPDS_2:46
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A42, A47, SCMPDS_2:46
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A42, SCMPDS_2:46;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A42, SCMPDS_2:46;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A43, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 8 ; :: thesis:

then consider a being Int_position, k1, k2 being Integer such that
A48: CurInstr (P,s) = AddTo (a,k1,k2) by SCMPDS_2:34;

A49: now :: thesis:

let b be Int_position; :: thesis:

per cases ;

suppose A50: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b ; :: thesis:

then A51: DataLoc ((s . a),k1) = b by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = ((s +* (Start-At (((IC s) + n),SCMPDS))) . b) + k2 by A48, A50, SCMPDS_2:48
.= (s . b) + k2 by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A48, A51, SCMPDS_2:48
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

suppose A52: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ; :: thesis:

then A53: DataLoc ((s . a),k1) <> b by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A48, A52, SCMPDS_2:48
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A48, A53, SCMPDS_2:48
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A48, SCMPDS_2:48;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A48, SCMPDS_2:48;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A49, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 9 ; :: thesis:

then consider a, b being Int_position, k1, k2 being Integer such that
A54: CurInstr (P,s) = AddTo (a,k1,b,k2) by SCMPDS_2:35;

A55: now :: thesis:

let c be Int_position; :: thesis:

per cases ;

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

then A57: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A58: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ;
hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) + (s . (DataLoc ((s . b),k2))) by A54, A56, A58, SCMPDS_2:49
.= (Exec ((CurInstr (P,s)),s)) . c by A54, A57, SCMPDS_2:49
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

suppose A59: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; :: thesis:

then A60: DataLoc ((s . a),k1) <> c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A54, A59, SCMPDS_2:49
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A54, A60, SCMPDS_2:49
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A54, SCMPDS_2:49;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A54, SCMPDS_2:49;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A55, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 10 ; :: thesis:

then consider a, b being Int_position, k1, k2 being Integer such that
A61: CurInstr (P,s) = SubFrom (a,k1,b,k2) by SCMPDS_2:36;

A62: now :: thesis:

let c be Int_position; :: thesis:

per cases ;

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

then A64: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A65: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ;
hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) - (s . (DataLoc ((s . b),k2))) by A61, A63, A65, SCMPDS_2:50
.= (Exec ((CurInstr (P,s)),s)) . c by A61, A64, SCMPDS_2:50
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

suppose A66: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; :: thesis:

then A67: DataLoc ((s . a),k1) <> c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A61, A66, SCMPDS_2:50
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A61, A67, SCMPDS_2:50
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A61, SCMPDS_2:50;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A61, SCMPDS_2:50;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A62, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 11 ; :: thesis:

then consider a, b being Int_position, k1, k2 being Integer such that
A68: CurInstr (P,s) = MultBy (a,k1,b,k2) by SCMPDS_2:37;

A69: now :: thesis:

let c be Int_position; :: thesis:

per cases ;

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

then A71: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A72: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ;
hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) * (s . (DataLoc ((s . b),k2))) by A68, A70, A72, SCMPDS_2:51
.= (Exec ((CurInstr (P,s)),s)) . c by A68, A71, SCMPDS_2:51
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

suppose A73: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; :: thesis:

then A74: DataLoc ((s . a),k1) <> c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A68, A73, SCMPDS_2:51
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A68, A74, SCMPDS_2:51
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A68, SCMPDS_2:51;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A68, SCMPDS_2:51;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A69, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 12 ; :: thesis:

then consider a, b being Int_position, k1, k2 being Integer such that
A75: CurInstr (P,s) = Divide (a,k1,b,k2) by SCMPDS_2:38;

A76: now :: thesis:

let c be Int_position; :: thesis:
A77: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ;
A78: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ;

per cases ;

suppose A79: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) = c ; :: thesis:

then A80: DataLoc ((s . b),k2) = c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . b),k2))) by A75, A77, A78, A79, SCMPDS_2:52
.= (Exec ((CurInstr (P,s)),s)) . c by A75, A80, SCMPDS_2:52
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

suppose A81: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) <> c ; :: thesis:

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

hereby :: thesis:

per cases ;

suppose A83: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; :: thesis:

then A84: DataLoc ((s . a),k1) <> c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A75, A81, A83, SCMPDS_2:52
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A75, A82, A84, SCMPDS_2:52
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

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

then A86: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) by A75, A77, A78, A81, A85, SCMPDS_2:52
.= (Exec ((CurInstr (P,s)),s)) . c by A75, A82, A86, SCMPDS_2:52
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A75, SCMPDS_2:52;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A75, SCMPDS_2:52;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A76, SCMPDS_2:44; :: thesis:

end;

suppose InsCode (CurInstr (P,s)) = 13 ; :: thesis:

then consider a, b being Int_position, k1, k2 being Integer such that
A87: CurInstr (P,s) = (a,k1) := (b,k2) by SCMPDS_2:39;

A88: now :: thesis:

let c be Int_position; :: thesis:

per cases ;

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

then A90: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by A87, A89, SCMPDS_2:47
.= s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A87, A90, SCMPDS_2:47
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

suppose A91: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; :: thesis:

then A92: DataLoc ((s . a),k1) <> c by SCMPDS_3:6;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A87, A91, SCMPDS_2:47
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A87, A92, SCMPDS_2:47
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A87, SCMPDS_2:47;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A87, SCMPDS_2:47;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A88, SCMPDS_2:44; :: thesis:

end;