let m, n be Element of NAT ; :: thesis:
let s, s1 be State of SCMPDS ; :: thesis:
let J be parahalting shiftable Program of SCMPDS ; :: thesis:
set pJ = stop J;
set IsJ = Initialized (stop J);
set s2 = s1 +* (Initialized (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 AMI_1:111
.= IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At (Nl + n),SCMPDS )) by AMI_1:111 ;
A2: Initialized (stop J) c= s1 +* (Initialized (stop J)) by FUNCT_4:26;
assume A3: s = Comput (ProgramPart (s1 +* (Initialized (stop J)))),(s1 +* (Initialized (stop J))),m ; :: thesis:
then A4: IC s in dom (stop J) by A2, 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 AMI_1:111;

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 AMI_1:112
.= (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 AMI_1:112 ; :: thesis:

end;

Y: (ProgramPart s) /. (IC s) = s . (IC s) by AMI_1:150;
stop J c= s by A3, A2, AMI_1:81, SCMPDS_4:57;
then A7: CurInstr (ProgramPart s),s = (stop J) . n1 by A4, GRFUNC_1:8, Y;
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 AMI_1:111 ;
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 AMI_1:111 ;
:: 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 AMI_1:111 ;
:: 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 AMI_1:111 ;
:: 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:
thus verum ; :: 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;