let m, n be Element of NAT ; :: thesis: for s, s1 being State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st s = Computation (s1 +* (Initialized (stop J))),m holds
Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
let s, s1 be State of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS st s = Computation (s1 +* (Initialized (stop J))),m holds
Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
let J be parahalting shiftable Program of SCMPDS ; :: thesis: ( s = Computation (s1 +* (Initialized (stop J))),m implies Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n)) )
set pJ = stop J;
set IsJ = Initialized (stop J);
set s2 = s1 +* (Initialized (stop J));
set i = CurInstr s;
set ss = s +* (Start-At ((IC s) + n));
reconsider k = IC s as Element of NAT by ORDINAL1:def 13;
reconsider Nl = Next (IC s) as Instruction-Location of SCMPDS ;
A1: Next (IC (s +* (Start-At ((IC s) + n)))) = inspos ((k + n) + 1) by AMI_1:111
.= IC ((Exec (CurInstr s),s) +* (Start-At (Nl + n))) by AMI_1:111 ;
A2: Initialized (stop J) c= s1 +* (Initialized (stop J)) by FUNCT_4:26;
assume A3: s = Computation (s1 +* (Initialized (stop J))),m ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))
then A4: IC s in dom (stop J) by A2, SCMPDS_4:def 9;
reconsider n1 = IC s as Element of NAT by ORDINAL1:def 13;
set IEn = (IC (Exec (CurInstr s),s)) + n;
A5: IC (s +* (Start-At ((IC s) + n))) = (IC s) + n by AMI_1:111;

A6: now

let d be Instruction-Location of SCMPDS ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . d
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . d = (s +* (Start-At ((IC s) + n))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (Exec (CurInstr s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . d by AMI_1:112 ; :: thesis: verum

end;

stop J c= s by A3, A2, AMI_1:81, SCMPDS_4:57;
then A7: CurInstr s = (stop J) . (inspos n1) by A4, GRFUNC_1:8;
then A8: InsCode (CurInstr s) <> 1 by A4, SCMPDS_4:def 12;
A9: CurInstr s valid_at n1 by A4, A7, SCMPDS_4:def 12;
A10: InsCode (CurInstr s) <> 3 by A4, A7, SCMPDS_4:def 12;
A11: IC s = inspos n1 ;

per cases ( InsCode (CurInstr s) = 0 or InsCode (CurInstr s) = 2 or InsCode (CurInstr s) = 4 or InsCode (CurInstr s) = 5 or InsCode (CurInstr s) = 6 or InsCode (CurInstr s) = 7 or InsCode (CurInstr s) = 8 or InsCode (CurInstr s) = 9 or InsCode (CurInstr s) = 10 or InsCode (CurInstr s) = 11 or InsCode (CurInstr s) = 12 or InsCode (CurInstr s) = 13 ) by A8, A10, NAT_1:38, SCMPDS_2:15;

suppose InsCode (CurInstr s) = 0 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A15: now

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

end;

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

end;

suppose InsCode (CurInstr s) = 2 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A17: now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( a = b or a <> b ) ;

suppose A18: a = b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

suppose A19: a <> b ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 4 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A22: now

per cases ( s . (DataLoc (s . a),k1) <> 0 or s . (DataLoc (s . a),k1) = 0 ) ;

suppose A23: s . (DataLoc (s . a),k1) <> 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then A24: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A20, SCMPDS_2:67;
(s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) <> 0 by A23, SCMPDS_3:14;
then (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) <> 0 by SCMPDS_3:14;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A20, SCMPDS_2:67
.= (IC (Exec (CurInstr s),s)) + n by A5, A11, A21, A24, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ;
:: thesis: verum

end;

suppose A25: s . (DataLoc (s . a),k1) = 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) = 0 by SCMPDS_3:14;
then A26: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A20, A25, SCMPDS_2:67;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A1, A20, A26, SCMPDS_2:67; :: thesis: verum

end;

end;

end;

now

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

end;

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

end;

suppose InsCode (CurInstr s) = 5 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A29: now

per cases ( s . (DataLoc (s . a),k1) <= 0 or s . (DataLoc (s . a),k1) > 0 ) ;

suppose A30: s . (DataLoc (s . a),k1) <= 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then A31: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A27, SCMPDS_2:68;
(s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) <= 0 by A30, SCMPDS_3:14;
then (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) <= 0 by SCMPDS_3:14;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A27, SCMPDS_2:68
.= (IC (Exec (CurInstr s),s)) + n by A5, A11, A28, A31, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ;
:: thesis: verum

end;

suppose A32: s . (DataLoc (s . a),k1) > 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) > 0 by SCMPDS_3:14;
then A33: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) > 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A27, A32, SCMPDS_2:68;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A1, A27, A33, SCMPDS_2:68; :: thesis: verum

end;

end;

end;

now

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

end;

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

end;

suppose InsCode (CurInstr s) = 6 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A36: now

per cases ( s . (DataLoc (s . a),k1) >= 0 or s . (DataLoc (s . a),k1) < 0 ) ;

suppose A37: s . (DataLoc (s . a),k1) >= 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then A38: IC (Exec (CurInstr s),s) = ICplusConst s,k2 by A34, SCMPDS_2:69;
(s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) >= 0 by A37, SCMPDS_3:14;
then (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) >= 0 by SCMPDS_3:14;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = ICplusConst (s +* (Start-At ((IC s) + n))),k2 by A34, SCMPDS_2:69
.= (IC (Exec (CurInstr s),s)) + n by A5, A11, A35, A38, SCMPDS_4:82
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by AMI_1:111 ;
:: thesis: verum

end;

suppose A39: s . (DataLoc (s . a),k1) < 0 ; :: thesis: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n)))

then (s +* (Start-At ((IC s) + n))) . (DataLoc (s . a),k1) < 0 by SCMPDS_3:14;
then A40: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) < 0 by SCMPDS_3:14;
IC (Exec (CurInstr s),s) = Nl by A34, A39, SCMPDS_2:69;
hence IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) by A1, A34, A40, SCMPDS_2:69; :: thesis: verum

end;

end;

end;

now

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

end;

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

end;

suppose InsCode (CurInstr s) = 7 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A42: now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ) ;

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

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

end;

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

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 8 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A48: now

let b be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = b or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> b ) ;

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

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

end;

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

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 9 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A54: now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

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

then A56: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A57: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) + (s . (DataLoc (s . b),k2)) by A53, A55, A57, SCMPDS_2:61
.= (Exec (CurInstr s),s) . c by A53, A56, SCMPDS_2:61
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A58: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 10 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A61: now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

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

then A63: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A64: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) - (s . (DataLoc (s . b),k2)) by A60, A62, A64, SCMPDS_2:62
.= (Exec (CurInstr s),s) . c by A60, A63, SCMPDS_2:62
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A65: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 11 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A68: now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

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

then A70: DataLoc (s . a),k1 = c by SCMPDS_3:14;
A71: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;
(s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s . (DataLoc (s . a),k1)) * (s . (DataLoc (s . b),k2)) by A67, A69, A71, SCMPDS_2:63
.= (Exec (CurInstr s),s) . c by A67, A70, SCMPDS_2:63
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ;
:: thesis: verum

end;

suppose A72: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 12 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A75: now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁
A76: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1) by SCMPDS_3:14
.= s . (DataLoc (s . a),k1) by SCMPDS_3:14 ;
A77: (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) = s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14 ;

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 <> c ) ;

suppose A78: DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2 = c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

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

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

hereby :: thesis: verum

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c ) ;

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

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

end;

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

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

end;

end;

end;

end;

end;

end;

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

end;

suppose InsCode (CurInstr s) = 13 ; :: thesis: Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

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

A87: now

let c be Int_position ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

per cases ( DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 = c or DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ) ;

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

then A89: DataLoc (s . a),k1 = c by SCMPDS_3:14;
thus (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . c = (s +* (Start-At ((IC s) + n))) . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by A86, A88, SCMPDS_2:59
.= s . (DataLoc ((s +* (Start-At ((IC s) + n))) . b),k2) by SCMPDS_3:14
.= s . (DataLoc (s . b),k2) by SCMPDS_3:14
.= (Exec (CurInstr s),s) . c by A86, A89, SCMPDS_2:59
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . c by SCMPDS_3:14 ; :: thesis: verum

end;

suppose A90: DataLoc ((s +* (Start-At ((IC s) + n))) . a),k1 <> c ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + n)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + n))) . b₁

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

end;

end;

end;

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

end;

end;