let m, n be Element of NAT ; :: thesis:
let P, P1 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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 IsJ = Initialize (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:121
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At ((Nl + n),SCMPDS))) by FUNCT_4:121 ;
assume Z: stop J c= P ; :: thesis:
assume s = Comput ((P1 +* (stop J)),s1,m) ; :: thesis:
then A3: IC s in dom (stop J) by FUNCT_4:26, SCMPDS_4:def 9;
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:121;

A5: now

let d be Element of NAT ; :: thesis:
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . d = (s +* (Start-At (((IC s) + n),SCMPDS))) . d by AMI_1:def 13
.= s . d by COMPOS_1:20
.= (Exec ((CurInstr (P,s)),s)) . d by AMI_1:def 13
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . d by COMPOS_1:20 ; :: thesis:

end;

A6: P /. (IC s) = P . (IC s) by PBOOLE:158;
stop J c= P by Z;
then A7: CurInstr (P,s) = (stop J) . n1 by A3, A6, GRFUNC_1:8;
then A8: InsCode (CurInstr (P,s)) <> 1 by A3, SCMPDS_4:def 12;
A9: CurInstr (P,s) valid_at n1 by A3, A7, SCMPDS_4:def 12;
A10: InsCode (CurInstr (P,s)) <> 3 by A3, A7, SCMPDS_4:def 12;

per cases by A8, A10, NAT_1:38, SCMPDS_2:15;

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 11;
A13: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k1) by A11, SCMPDS_2:66;

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:66
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A11, SCMPDS_2:66
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: 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:66
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A12, A13, SCMPDS_4:82
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A14, SCMPDS_2:54; :: 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:37;

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:57
.= (Exec ((CurInstr (P,s)),s)) . b by A15, A17, SCMPDS_2:57
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ;
:: 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:57
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A15, A18, SCMPDS_2:57
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ;
:: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A15, SCMPDS_2:57;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A15, SCMPDS_2:57;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A16, SCMPDS_2:54; :: 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 11;

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:67;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <> 0 by A22, SCMPDS_3:14;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <> 0 by SCMPDS_3:14;
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:67
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A20, A23, SCMPDS_4:82
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: 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:14;
then A25: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = 0 by SCMPDS_3:14;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A19, A24, SCMPDS_2:67;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A19, A25, SCMPDS_2:67; :: 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:67
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A19, SCMPDS_2:67
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A21, SCMPDS_2:54; :: 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 11;

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:68;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <= 0 by A29, SCMPDS_3:14;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <= 0 by SCMPDS_3:14;
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:68
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A27, A30, SCMPDS_4:82
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: 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:14;
then A32: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) > 0 by SCMPDS_3:14;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A26, A31, SCMPDS_2:68;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A26, A32, SCMPDS_2:68; :: 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:68
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A26, SCMPDS_2:68
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A28, SCMPDS_2:54; :: 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 11;

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:69;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) >= 0 by A36, SCMPDS_3:14;
then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) >= 0 by SCMPDS_3:14;
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:69
.= (IC (Exec ((CurInstr (P,s)),s))) + n by A4, A34, A37, SCMPDS_4:82
.= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: 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:14;
then A39: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) < 0 by SCMPDS_3:14;
IC (Exec ((CurInstr (P,s)),s)) = Nl by A33, A38, SCMPDS_2:69;
hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A33, A39, SCMPDS_2:69; :: 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:69
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A33, SCMPDS_2:69
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A35, SCMPDS_2:54; :: 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:42;

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:14;
thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = k2 by A40, A42, SCMPDS_2:58
.= (Exec ((CurInstr (P,s)),s)) . b by A40, A43, SCMPDS_2:58
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: 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:14;
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:58
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A40, A45, SCMPDS_2:58
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A40, SCMPDS_2:58;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A40, SCMPDS_2:58;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A41, SCMPDS_2:54; :: 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:43;

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:14;
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:60
.= (s . b) + k2 by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A46, A49, SCMPDS_2:60
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: 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:14;
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:60
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . b by A46, A51, SCMPDS_2:60
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A46, SCMPDS_2:60;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A46, SCMPDS_2:60;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A47, SCMPDS_2:54; :: 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:44;

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:14;
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:14
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:14 ;
(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:14
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:14 ;
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:61
.= (Exec ((CurInstr (P,s)),s)) . c by A52, A55, SCMPDS_2:61
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ;
:: 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:14;
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:61
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A52, A58, SCMPDS_2:61
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A52, SCMPDS_2:61;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A52, SCMPDS_2:61;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A53, SCMPDS_2:54; :: 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:45;

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:14;
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:14
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:14 ;
(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:14
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:14 ;
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:62
.= (Exec ((CurInstr (P,s)),s)) . c by A59, A62, SCMPDS_2:62
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ;
:: 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:14;
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:62
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A59, A65, SCMPDS_2:62
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A59, SCMPDS_2:62;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A59, SCMPDS_2:62;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A60, SCMPDS_2:54; :: 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:46;

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:14;
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:14
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:14 ;
(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:14
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:14 ;
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:63
.= (Exec ((CurInstr (P,s)),s)) . c by A66, A69, SCMPDS_2:63
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ;
:: 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:14;
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:63
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A66, A72, SCMPDS_2:63
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A66, SCMPDS_2:63;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A66, SCMPDS_2:63;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A67, SCMPDS_2:54; :: 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:47;

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:14
.= s . (DataLoc ((s . a),k1)) by SCMPDS_3:14 ;
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:14
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:14 ;

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:14;
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:64
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A78, SCMPDS_2:64
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: 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:14;

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:14;
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:64
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A80, A82, SCMPDS_2:64
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: 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:14;
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:64
.= (Exec ((CurInstr (P,s)),s)) . c by A73, A80, A84, SCMPDS_2:64
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A73, SCMPDS_2:64;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A73, SCMPDS_2:64;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A74, SCMPDS_2:54; :: 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:48;

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:14;
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:59
.= s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:14
.= s . (DataLoc ((s . b),k2)) by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A85, A88, SCMPDS_2:59
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: 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:14;
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:59
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr (P,s)),s)) . c by A85, A90, SCMPDS_2:59
.= ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr (P,s)),s)) = Nl by A85, SCMPDS_2:59;
then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At (((IC (Exec ((CurInstr (P,s)),s))) + n),SCMPDS))) by A1, A85, SCMPDS_2:59;
hence Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = IncIC ((Following (P,s)),n) by A5, A86, SCMPDS_2:54; :: thesis:

end;