let i be Instruction of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT holds
Exec (i,s1), Exec (i,s2) equal_outside NAT
let s1, s2 be State of SCMPDS; :: thesis: ( s1,s2 equal_outside NAT implies Exec (i,s1), Exec (i,s2) equal_outside NAT )
assume A1: s1,s2 equal_outside NAT ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT
then A2: IC s1 = IC s2 by COMPOS_1:24;

per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by NAT_1:38, SCMPDS_2:15;

suppose InsCode i = 0 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider k1 being Integer such that
A3: i = goto k1 by SCMPDS_2:35;

A4: now

let a be Int_position ; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A3, SCMPDS_2:66
.= s2 . a by A1, Th13
.= (Exec (i,s2)) . a by A3, SCMPDS_2:66 ; :: thesis: verum

end;

IC (Exec (i,s1)) = ICplusConst (s1,k1) by A3, SCMPDS_2:66
.= ICplusConst (s2,k1) by A2, SCMPDS_3:2
.= IC (Exec (i,s2)) by A3, SCMPDS_2:66 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A4, Th11; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position such that
A5: i = return a by SCMPDS_2:36;

A6: now

let b be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

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

suppose A7: a = b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

hence (Exec (i,s1)) . b = s1 . (DataLoc ((s1 . a),RetSP)) by A5, SCMPDS_2:70
.= s2 . (DataLoc ((s2 . a),RetSP)) by A1, Th14
.= (Exec (i,s2)) . b by A5, A7, SCMPDS_2:70 ;
:: thesis: verum

end;

suppose A8: a <> b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

hence (Exec (i,s1)) . b = s1 . b by A5, SCMPDS_2:70
.= s2 . b by A1, Th13
.= (Exec (i,s2)) . b by A5, A8, SCMPDS_2:70 ;
:: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = (abs (s1 . (DataLoc ((s1 . a),RetIC)))) + 2 by A5, SCMPDS_2:70
.= (abs (s1 . (DataLoc ((s2 . a),RetIC)))) + 2 by A1, Th13
.= (abs (s2 . (DataLoc ((s2 . a),RetIC)))) + 2 by A1, Th13
.= IC (Exec (i,s2)) by A5, SCMPDS_2:70 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A6, Th11; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1 being Integer such that
A9: i = a := k1 by SCMPDS_2:37;

A10: now

let b be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

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

suppose A11: a = b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

hence (Exec (i,s1)) . b = k1 by A9, SCMPDS_2:57
.= (Exec (i,s2)) . b by A9, A11, SCMPDS_2:57 ;
:: thesis: verum

end;

suppose A12: a <> b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

hence (Exec (i,s1)) . b = s1 . b by A9, SCMPDS_2:57
.= s2 . b by A1, Th13
.= (Exec (i,s2)) . b by A9, A12, SCMPDS_2:57 ;
:: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A9, SCMPDS_2:57
.= IC (Exec (i,s2)) by A9, SCMPDS_2:57 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A10, Th11; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1 being Integer such that
A13: i = saveIC (a,k1) by SCMPDS_2:38;

A14: now

let b be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( b = DataLoc ((s1 . a),k1) or b <> DataLoc ((s1 . a),k1) ) ;

suppose A15: b = DataLoc ((s1 . a),k1) ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A16: b = DataLoc ((s2 . a),k1) by A1, Th13;
thus (Exec (i,s1)) . b = IC s2 by A2, A13, A15, SCMPDS_2:71
.= (Exec (i,s2)) . b by A13, A16, SCMPDS_2:71 ; :: thesis: verum

end;

suppose A17: b <> DataLoc ((s1 . a),k1) ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A18: b <> DataLoc ((s2 . a),k1) by A1, Th13;
thus (Exec (i,s1)) . b = s1 . b by A13, A17, SCMPDS_2:71
.= s2 . b by A1, Th13
.= (Exec (i,s2)) . b by A13, A18, SCMPDS_2:71 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A13, SCMPDS_2:71
.= IC (Exec (i,s2)) by A13, SCMPDS_2:71 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A14, Th11; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1, k2 being Integer such that
A19: i = (a,k1) <>0_goto k2 by SCMPDS_2:39;

A20: now

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

suppose A21: s1 . (DataLoc ((s1 . a),k1)) <> 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A22: s2 . (DataLoc ((s2 . a),k1)) <> 0 by A1, Th14;
thus IC (Exec (i,s1)) = ICplusConst (s1,k2) by A19, A21, SCMPDS_2:67
.= ICplusConst (s2,k2) by A2, SCMPDS_3:2
.= IC (Exec (i,s2)) by A19, A22, SCMPDS_2:67 ; :: thesis: verum

end;

suppose A23: s1 . (DataLoc ((s1 . a),k1)) = 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A24: s2 . (DataLoc ((s2 . a),k1)) = 0 by A1, Th14;
thus IC (Exec (i,s1)) = succ (IC s2) by A2, A19, A23, SCMPDS_2:67
.= IC (Exec (i,s2)) by A19, A24, SCMPDS_2:67 ; :: thesis: verum

end;

end;

end;

now

let a be Int_position ; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A19, SCMPDS_2:67
.= s2 . a by A1, Th13
.= (Exec (i,s2)) . a by A19, SCMPDS_2:67 ; :: thesis: verum

end;

hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A20, Th11; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1, k2 being Integer such that
A25: i = (a,k1) <=0_goto k2 by SCMPDS_2:40;

A26: now

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

suppose A27: s1 . (DataLoc ((s1 . a),k1)) <= 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A28: s2 . (DataLoc ((s2 . a),k1)) <= 0 by A1, Th14;
thus IC (Exec (i,s1)) = ICplusConst (s1,k2) by A25, A27, SCMPDS_2:68
.= ICplusConst (s2,k2) by A2, SCMPDS_3:2
.= IC (Exec (i,s2)) by A25, A28, SCMPDS_2:68 ; :: thesis: verum

end;

suppose A29: s1 . (DataLoc ((s1 . a),k1)) > 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A30: s2 . (DataLoc ((s2 . a),k1)) > 0 by A1, Th14;
thus IC (Exec (i,s1)) = succ (IC s2) by A2, A25, A29, SCMPDS_2:68
.= IC (Exec (i,s2)) by A25, A30, SCMPDS_2:68 ; :: thesis: verum

end;

end;

end;

now

let a be Int_position ; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A25, SCMPDS_2:68
.= s2 . a by A1, Th13
.= (Exec (i,s2)) . a by A25, SCMPDS_2:68 ; :: thesis: verum

end;

hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A26, Th11; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1, k2 being Integer such that
A31: i = (a,k1) >=0_goto k2 by SCMPDS_2:41;

A32: now

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

suppose A33: s1 . (DataLoc ((s1 . a),k1)) >= 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A34: s2 . (DataLoc ((s2 . a),k1)) >= 0 by A1, Th14;
thus IC (Exec (i,s1)) = ICplusConst (s1,k2) by A31, A33, SCMPDS_2:69
.= ICplusConst (s2,k2) by A2, SCMPDS_3:2
.= IC (Exec (i,s2)) by A31, A34, SCMPDS_2:69 ; :: thesis: verum

end;

suppose A35: s1 . (DataLoc ((s1 . a),k1)) < 0 ; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))

then A36: s2 . (DataLoc ((s2 . a),k1)) < 0 by A1, Th14;
thus IC (Exec (i,s1)) = succ (IC s2) by A2, A31, A35, SCMPDS_2:69
.= IC (Exec (i,s2)) by A31, A36, SCMPDS_2:69 ; :: thesis: verum

end;

end;

end;

now

let a be Int_position ; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A31, SCMPDS_2:69
.= s2 . a by A1, Th13
.= (Exec (i,s2)) . a by A31, SCMPDS_2:69 ; :: thesis: verum

end;

hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A32, Th11; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1, k2 being Integer such that
A37: i = (a,k1) := k2 by SCMPDS_2:42;

A38: now

let b be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;

suppose A39: DataLoc ((s1 . a),k1) = b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A40: DataLoc ((s2 . a),k1) = b by A1, Th13;
thus (Exec (i,s1)) . b = k2 by A37, A39, SCMPDS_2:58
.= (Exec (i,s2)) . b by A37, A40, SCMPDS_2:58 ; :: thesis: verum

end;

suppose A41: DataLoc ((s1 . a),k1) <> b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A42: DataLoc ((s2 . a),k1) <> b by A1, Th13;
thus (Exec (i,s1)) . b = s1 . b by A37, A41, SCMPDS_2:58
.= s2 . b by A1, Th13
.= (Exec (i,s2)) . b by A37, A42, SCMPDS_2:58 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A37, SCMPDS_2:58
.= IC (Exec (i,s2)) by A37, SCMPDS_2:58 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A38, Th11; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a being Int_position , k1, k2 being Integer such that
A43: i = AddTo (a,k1,k2) by SCMPDS_2:43;

A44: now

let b be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;

suppose A45: DataLoc ((s1 . a),k1) = b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A46: DataLoc ((s2 . a),k1) = b by A1, Th13;
thus (Exec (i,s1)) . b = (s1 . (DataLoc ((s1 . a),k1))) + k2 by A43, A45, SCMPDS_2:60
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A1, Th14
.= (Exec (i,s2)) . b by A43, A46, SCMPDS_2:60 ; :: thesis: verum

end;

suppose A47: DataLoc ((s1 . a),k1) <> b ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A48: DataLoc ((s2 . a),k1) <> b by A1, Th13;
thus (Exec (i,s1)) . b = s1 . b by A43, A47, SCMPDS_2:60
.= s2 . b by A1, Th13
.= (Exec (i,s2)) . b by A43, A48, SCMPDS_2:60 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A43, SCMPDS_2:60
.= IC (Exec (i,s2)) by A43, SCMPDS_2:60 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A44, Th11; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a, b being Int_position , k1, k2 being Integer such that
A49: i = AddTo (a,k1,b,k2) by SCMPDS_2:44;

A50: now

let c be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;

suppose A51: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A52: DataLoc ((s2 . a),k1) = c by A1, Th13;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A49, A51, SCMPDS_2:61
.= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A1, Th14
.= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A1, Th14
.= (Exec (i,s2)) . c by A49, A52, SCMPDS_2:61 ; :: thesis: verum

end;

suppose A53: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A54: DataLoc ((s2 . a),k1) <> c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . c by A49, A53, SCMPDS_2:61
.= s2 . c by A1, Th13
.= (Exec (i,s2)) . c by A49, A54, SCMPDS_2:61 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A49, SCMPDS_2:61
.= IC (Exec (i,s2)) by A49, SCMPDS_2:61 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A50, Th11; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a, b being Int_position , k1, k2 being Integer such that
A55: i = SubFrom (a,k1,b,k2) by SCMPDS_2:45;

A56: now

let c be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;

suppose A57: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A58: DataLoc ((s2 . a),k1) = c by A1, Th13;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A55, A57, SCMPDS_2:62
.= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A1, Th14
.= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A1, Th14
.= (Exec (i,s2)) . c by A55, A58, SCMPDS_2:62 ; :: thesis: verum

end;

suppose A59: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A60: DataLoc ((s2 . a),k1) <> c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . c by A55, A59, SCMPDS_2:62
.= s2 . c by A1, Th13
.= (Exec (i,s2)) . c by A55, A60, SCMPDS_2:62 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A55, SCMPDS_2:62
.= IC (Exec (i,s2)) by A55, SCMPDS_2:62 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A56, Th11; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a, b being Int_position , k1, k2 being Integer such that
A61: i = MultBy (a,k1,b,k2) by SCMPDS_2:46;

A62: now

let c be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;

suppose A63: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A64: DataLoc ((s2 . a),k1) = c by A1, Th13;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A61, A63, SCMPDS_2:63
.= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A1, Th14
.= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A1, Th14
.= (Exec (i,s2)) . c by A61, A64, SCMPDS_2:63 ; :: thesis: verum

end;

suppose A65: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A66: DataLoc ((s2 . a),k1) <> c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . c by A61, A65, SCMPDS_2:63
.= s2 . c by A1, Th13
.= (Exec (i,s2)) . c by A61, A66, SCMPDS_2:63 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A61, SCMPDS_2:63
.= IC (Exec (i,s2)) by A61, SCMPDS_2:63 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A62, Th11; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a, b being Int_position , k1, k2 being Integer such that
A67: i = Divide (a,k1,b,k2) by SCMPDS_2:47;

A68: now

let c be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . b),k2) = c or DataLoc ((s1 . b),k2) <> c ) ;

suppose A69: DataLoc ((s1 . b),k2) = c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A70: DataLoc ((s2 . b),k2) = c by A1, Th13;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A67, A69, SCMPDS_2:64
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A1, Th14
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A1, Th14
.= (Exec (i,s2)) . c by A67, A70, SCMPDS_2:64 ; :: thesis: verum

end;

suppose A71: DataLoc ((s1 . b),k2) <> c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A72: DataLoc ((s2 . b),k2) <> c by A1, Th13;

hereby :: thesis: verum

per cases ( DataLoc ((s1 . a),k1) <> c or DataLoc ((s1 . a),k1) = c ) ;

suppose A73: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c

then A74: DataLoc ((s2 . a),k1) <> c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . c by A67, A71, A73, SCMPDS_2:64
.= s2 . c by A1, Th13
.= (Exec (i,s2)) . c by A67, A72, A74, SCMPDS_2:64 ; :: thesis: verum

end;

suppose A75: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c

then A76: DataLoc ((s2 . a),k1) = c by A1, Th13;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A67, A71, A75, SCMPDS_2:64
.= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A1, Th14
.= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A1, Th14
.= (Exec (i,s2)) . c by A67, A72, A76, SCMPDS_2:64 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A67, SCMPDS_2:64
.= IC (Exec (i,s2)) by A67, SCMPDS_2:64 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A68, Th11; :: thesis: verum

end;

suppose InsCode i = 13 ; :: thesis: Exec (i,s1), Exec (i,s2) equal_outside NAT

then consider a, b being Int_position , k1, k2 being Integer such that
A77: i = (a,k1) := (b,k2) by SCMPDS_2:48;

A78: now

let c be Int_position ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;

suppose A79: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A80: DataLoc ((s2 . a),k1) = c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . (DataLoc ((s1 . b),k2)) by A77, A79, SCMPDS_2:59
.= s2 . (DataLoc ((s2 . b),k2)) by A1, Th14
.= (Exec (i,s2)) . c by A77, A80, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A81: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b₁ = (Exec (i,s2)) . b₁

then A82: DataLoc ((s2 . a),k1) <> c by A1, Th13;
thus (Exec (i,s1)) . c = s1 . c by A77, A81, SCMPDS_2:59
.= s2 . c by A1, Th13
.= (Exec (i,s2)) . c by A77, A82, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

IC (Exec (i,s1)) = succ (IC s2) by A2, A77, SCMPDS_2:59
.= IC (Exec (i,s2)) by A77, SCMPDS_2:59 ;
hence Exec (i,s1), Exec (i,s2) equal_outside NAT by A78, Th11; :: thesis: verum

end;

end;