let m, n be Element of 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 SCMPDS; :: 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 = succ (IC s) as Element of NAT ;
A1: succ (IC (s +* (Start-At (((IC s) + n),SCMPDS)))) = (k + n) + 1 by FUNCT_4:113
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At ((Nl + n),SCMPDS))) by FUNCT_4:113 ;
assume Z: stop J c= P ; :: thesis:
assume ZZ: s = Comput ((P1 +* (stop J)),s1,m) ; :: thesis:
stop J c= P1 +* (stop J) by FUNCT_4:25;
then A3: IC s in dom (stop J) by ZZ, SCMPDS_4:def 6;
reconsider n1 = IC s as Element of NAT ;
set IEn = (IC (Exec ((CurInstr (P,s)),s))) + n;
A4: 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 A3, A6, GRFUNC_1:2, Z;
then A8: InsCode (CurInstr (P,s)) <> 1 by A3, SCMPDS_4:def 9;
A9: CurInstr (P,s) valid_at n1 by A3, A7, SCMPDS_4:def 9;
A10: InsCode (CurInstr (P,s)) <> 3 by A3, A7, SCMPDS_4:def 9;

per cases by A8, A10, NAT_1:37, SCMPDS_2:6;

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

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

A14: now

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 A11, SCMPDS_2:54
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A11, 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 A11, SCMPDS_2:54
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A12, A13, 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 A14, SCMPDS_2:44; :: thesis:

end;

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

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

A16: now

let b be Int_position ; :: thesis:

per cases ;

suppose A17: a = b ; :: thesis:

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

end;

suppose A18: 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 A15, SCMPDS_2:45
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A15, A18, 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 A15, 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, A15, SCMPDS_2:45;
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)) = 4 ; :: thesis:

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

A21: now

per cases ;

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

then A23: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A19, SCMPDS_2:55;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <> 0 by A22, 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 A19, SCMPDS_2:55
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A20, A23, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A24: 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 A25: (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 A19, A24, 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, A19, A25, SCMPDS_2:55; :: thesis:

end;

now

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 A19, SCMPDS_2:55
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A19, 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 A21, SCMPDS_2:44; :: thesis:

end;

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

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

A28: now

per cases ;

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

then A30: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A26, SCMPDS_2:56;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <= 0 by A29, 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 A26, SCMPDS_2:56
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A27, A30, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A31: 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 A32: (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 A26, A31, 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, A26, A32, SCMPDS_2:56; :: thesis:

end;

now

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 A26, SCMPDS_2:56
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A26, 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 A28, SCMPDS_2:44; :: thesis:

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A33: CurInstr (P,s) = (a,k1) >=0_goto k2 and
A34: n1 + k2 >= 0 by A9, SCMPDS_4:def 8;

A35: now

per cases ;

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

then A37: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A33, SCMPDS_2:57;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) >= 0 by A36, 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 A33, SCMPDS_2:57
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A34, A37, SCMPDS_4:27
.= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ;
:: thesis:

end;

suppose A38: 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 A39: (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 A33, A38, 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, A33, A39, SCMPDS_2:57; :: thesis:

end;

now

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 A33, SCMPDS_2:57
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A33, 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 A35, SCMPDS_2:44; :: thesis:

end;

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

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

A41: now

let b be Int_position ; :: thesis:

per cases ;

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

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

end;

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 = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A40, A44, SCMPDS_2:46
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A40, A45, 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 A40, 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, A40, SCMPDS_2:46;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A41, SCMPDS_2:44; :: thesis:

end;

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

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

A47: now

let b be Int_position ; :: thesis:

per cases ;

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

then A49: 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 A46, A48, SCMPDS_2:48
.= (s . b) + k2 by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A46, A49, SCMPDS_2:48
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; :: thesis:

end;

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 by A46, A50, SCMPDS_2:48
.= s . b by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . b by A46, A51, 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 A46, 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, A46, SCMPDS_2:48;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A47, 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
A52: CurInstr (P,s) = AddTo (a,k1,b,k2) by SCMPDS_2:35;

A53: now

let c be Int_position ; :: thesis:

per cases ;

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

then A55: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A56: (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 A52, A54, A56, SCMPDS_2:49
.= (Exec ((CurInstr (P,s)),s)) . c by A52, A55, SCMPDS_2:49
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

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

then A58: 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 A52, A57, SCMPDS_2:49
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A52, A58, 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 A52, 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, A52, SCMPDS_2:49;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A53, 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
A59: CurInstr (P,s) = SubFrom (a,k1,b,k2) by SCMPDS_2:36;

A60: now

let c be Int_position ; :: thesis:

per cases ;

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

then A62: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A63: (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 A59, A61, A63, SCMPDS_2:50
.= (Exec ((CurInstr (P,s)),s)) . c by A59, A62, SCMPDS_2:50
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

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

then A65: 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 A59, A64, SCMPDS_2:50
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A59, A65, 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 A59, 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, A59, SCMPDS_2:50;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A60, 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
A66: CurInstr (P,s) = MultBy (a,k1,b,k2) by SCMPDS_2:37;

A67: now

let c be Int_position ; :: thesis:

per cases ;

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

then A69: DataLoc ((s . a),k1) = c by SCMPDS_3:6;
A70: (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 A66, A68, A70, SCMPDS_2:51
.= (Exec ((CurInstr (P,s)),s)) . c by A66, A69, SCMPDS_2:51
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ;
:: thesis:

end;

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

then A72: 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 A66, A71, SCMPDS_2:51
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A66, A72, 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 A66, 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, A66, SCMPDS_2:51;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A67, 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
A73: CurInstr (P,s) = Divide (a,k1,b,k2) by SCMPDS_2:38;

A74: now

let c be Int_position ; :: thesis:
A75: (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 ;
A76: (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 A77: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) = c ; :: thesis:

then A78: 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 A73, A75, A76, A77, SCMPDS_2:52
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A78, SCMPDS_2:52
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

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;

hereby :: thesis:

per cases ;

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

then A82: 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 A73, A79, A81, SCMPDS_2:52
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A80, A82, SCMPDS_2:52
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

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 . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) by A73, A75, A76, A79, A83, SCMPDS_2:52
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A80, A84, 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 A73, 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, A73, SCMPDS_2:52;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A74, 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
A85: CurInstr (P,s) = (a,k1) := (b,k2) by SCMPDS_2:39;

A86: now

let c be Int_position ; :: thesis:

per cases ;

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

then A88: 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 A85, A87, 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 A85, A88, SCMPDS_2:47
.= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; :: thesis:

end;

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))) . c by A85, A89, SCMPDS_2:47
.= s . c by SCMPDS_3:6
.= (Exec ((CurInstr (P,s)),s)) . c by A85, A90, 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 A85, 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, A85, SCMPDS_2:47;
hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A86, SCMPDS_2:44; :: thesis:

end;