let m, n be Element 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 +* (stop J);
set i = CurInstr ((ProgramPart s),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 ((ProgramPart s),s)),s)) +* (Start-At ((Nl + n),SCMPDS))) by FUNCT_4:121 ;
assume A3: s = Comput ((ProgramPart (s1 +* (stop J))),(s1 +* (stop J)),m) ; :: thesis:
then A4: 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 ((ProgramPart s),s)),s))) + n;
A5: IC (s +* (Start-At (((IC s) + n),SCMPDS))) = (IC s) + n by FUNCT_4:121;

A6: now

let d be Element of NAT ; :: thesis:
thus (Exec ((CurInstr ((ProgramPart s),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 ((ProgramPart s),s)),s)) . d by AMI_1:def 13
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . d by COMPOS_1:20 ; :: thesis:

end;

Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
stop J c= s by A3, AMI_1:81, FUNCT_4:26;
then A7: CurInstr ((ProgramPart s),s) = (stop J) . n1 by A4, Y, GRFUNC_1:8;
then A8: InsCode (CurInstr ((ProgramPart s),s)) <> 1 by A4, SCMPDS_4:def 12;
A9: CurInstr ((ProgramPart s),s) valid_at n1 by A4, A7, SCMPDS_4:def 12;
A10: InsCode (CurInstr ((ProgramPart s),s)) <> 3 by A4, A7, SCMPDS_4:def 12;

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

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

then consider k1 being Integer such that
A12: CurInstr ((ProgramPart s),s) = goto k1 and
A13: n1 + k1 >= 0 by A9, SCMPDS_4:def 11;
A14: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = ICplusConst (s,k1) by A12, SCMPDS_2:66;

A15: now

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

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k1) by A12, SCMPDS_2:66
.= (IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n by A5, A13, A14, SCMPDS_4:82
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A15, SCMPDS_2:54; :: thesis:

end;

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

then consider a being Int_position , k1 being Integer such that
A16: CurInstr ((ProgramPart s),s) = a := k1 by SCMPDS_2:37;

A17: now

let b be Int_position ; :: thesis:

per cases ;

suppose A18: a = b ; :: thesis:

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

end;

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

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

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A16, SCMPDS_2:57;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A16, SCMPDS_2:57;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A17, SCMPDS_2:54; :: thesis:

end;

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

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

A22: now

per cases ;

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

then A24: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = ICplusConst (s,k2) by A20, SCMPDS_2:67;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <> 0 by A23, 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 ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A20, SCMPDS_2:67
.= (IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n by A5, A21, A24, SCMPDS_4:82
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: thesis:

end;

suppose A25: 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 A26: (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 ((ProgramPart s),s)),s)) = Nl by A20, A25, SCMPDS_2:67;
hence IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A20, A26, SCMPDS_2:67; :: thesis:

end;

now

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

end;

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

end;

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

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

A29: now

per cases ;

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

then A31: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = ICplusConst (s,k2) by A27, SCMPDS_2:68;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <= 0 by A30, 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 ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A27, SCMPDS_2:68
.= (IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n by A5, A28, A31, SCMPDS_4:82
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: thesis:

end;

suppose A32: 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 A33: (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 ((ProgramPart s),s)),s)) = Nl by A27, A32, SCMPDS_2:68;
hence IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A27, A33, SCMPDS_2:68; :: thesis:

end;

now

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

end;

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

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

A36: now

per cases ;

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

then A38: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = ICplusConst (s,k2) by A34, SCMPDS_2:69;
(s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) >= 0 by A37, 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 ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A34, SCMPDS_2:69
.= (IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n by A5, A35, A38, SCMPDS_4:82
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by FUNCT_4:121 ;
:: thesis:

end;

suppose A39: 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 A40: (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 ((ProgramPart s),s)),s)) = Nl by A34, A39, SCMPDS_2:69;
hence IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A34, A40, SCMPDS_2:69; :: thesis:

end;

now

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

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A41: CurInstr ((ProgramPart s),s) = (a,k1) := k2 by SCMPDS_2:42;

A42: now

let b be Int_position ; :: thesis:

per cases ;

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

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

end;

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

then A46: DataLoc ((s . a),k1) <> b by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A41, A45, SCMPDS_2:58
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . b by A41, A46, SCMPDS_2:58
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A41, SCMPDS_2:58;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A41, SCMPDS_2:58;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A42, SCMPDS_2:54; :: thesis:

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A47: CurInstr ((ProgramPart s),s) = AddTo (a,k1,k2) by SCMPDS_2:43;

A48: now

let b be Int_position ; :: thesis:

per cases ;

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

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

end;

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

then A52: DataLoc ((s . a),k1) <> b by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A47, A51, SCMPDS_2:60
.= s . b by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . b by A47, A52, SCMPDS_2:60
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . b by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A47, SCMPDS_2:60;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A47, SCMPDS_2:60;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A48, SCMPDS_2:54; :: thesis:

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A53: CurInstr ((ProgramPart s),s) = AddTo (a,k1,b,k2) by SCMPDS_2:44;

A54: now

let c be Int_position ; :: thesis:

per cases ;

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

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

end;

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

then A59: DataLoc ((s . a),k1) <> c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A53, A58, SCMPDS_2:61
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A53, A59, SCMPDS_2:61
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A53, SCMPDS_2:61;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A53, SCMPDS_2:61;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A54, SCMPDS_2:54; :: thesis:

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A60: CurInstr ((ProgramPart s),s) = SubFrom (a,k1,b,k2) by SCMPDS_2:45;

A61: now

let c be Int_position ; :: thesis:

per cases ;

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

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

end;

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

then A66: DataLoc ((s . a),k1) <> c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A60, A65, SCMPDS_2:62
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A60, A66, SCMPDS_2:62
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A60, SCMPDS_2:62;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A60, SCMPDS_2:62;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A61, SCMPDS_2:54; :: thesis:

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A67: CurInstr ((ProgramPart s),s) = MultBy (a,k1,b,k2) by SCMPDS_2:46;

A68: now

let c be Int_position ; :: thesis:

per cases ;

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

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

end;

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

then A73: DataLoc ((s . a),k1) <> c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A67, A72, SCMPDS_2:63
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A67, A73, SCMPDS_2:63
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A67, SCMPDS_2:63;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A67, SCMPDS_2:63;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A68, SCMPDS_2:54; :: thesis:

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A74: CurInstr ((ProgramPart s),s) = Divide (a,k1,b,k2) by SCMPDS_2:47;

A75: now

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

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

end;

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

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

hereby :: thesis:

per cases ;

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

then A83: DataLoc ((s . a),k1) <> c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A74, A80, A82, SCMPDS_2:64
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A74, A81, A83, SCMPDS_2:64
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

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

then A85: DataLoc ((s . a),k1) = c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) by A74, A76, A77, A80, A84, SCMPDS_2:64
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A74, A81, A85, SCMPDS_2:64
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = Nl by A74, SCMPDS_2:64;
then IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) by A1, A74, SCMPDS_2:64;
hence Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + n),SCMPDS)) by A6, A75, SCMPDS_2:54; :: thesis:

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A86: CurInstr ((ProgramPart s),s) = (a,k1) := (b,k2) by SCMPDS_2:48;

A87: now

let c be Int_position ; :: thesis:

per cases ;

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

then A89: DataLoc ((s . a),k1) = c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),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 A86, A88, 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 ((ProgramPart s),s)),s)) . c by A86, A89, SCMPDS_2:59
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

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

then A91: DataLoc ((s . a),k1) <> c by SCMPDS_3:14;
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A86, A90, SCMPDS_2:59
.= s . c by SCMPDS_3:14
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . c by A86, A91, SCMPDS_2:59
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + n),SCMPDS))) . c by SCMPDS_3:14 ; :: thesis:

end;

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

end;