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;