let s1, s2 be State of SCMPDS ; :: thesis: for n, m being Element of NAT
for i being Instruction of SCMPDS st IC s1 = inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
let n, m be Element of NAT ; :: thesis: for i being Instruction of SCMPDS st IC s1 = inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
let i be Instruction of SCMPDS ; :: thesis: ( IC s1 = inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 implies ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) ) )
assume that
A1: IC s1 = inspos m and
A2: i valid_at m and
A3: InsCode i <> 1 and
A4: InsCode i <> 3 and
A5: (IC s1) + n = IC s2 and
A6: DataPart s1 = DataPart s2 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
reconsider k1 = IC s1 as Element of NAT by ORDINAL1:def 13;
A8: (Next (IC s1)) + n = Next (IC s2) by A5;
set Ci = InsCode i;

A9: now

assume ( InsCode i <> 0 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 ) ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec i,s2)
then A10: not InsCode i in {0 ,1,4,5,6} by ENUMSET1:def 3;
then IC (Exec i,s1) = Next (IC s1) by Th6;
hence (IC (Exec i,s1)) + n = IC (Exec i,s2) by A8, A10, Th6; :: thesis: verum

end;

A11: now

let a be Int_position ; :: thesis: for k1 being Integer holds s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
let k1 be Integer; :: thesis: s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
thus s1 . (DataLoc (s1 . a),k1) = s1 . (DataLoc (s2 . a),k1) by A6, Th23
.= s2 . (DataLoc (s2 . a),k1) by A6, Th23 ; :: thesis: verum

end;

per cases ( InsCode i = 0 or InsCode i = 2 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 A3, A4, NAT_1:38, SCMPDS_2:15;

suppose InsCode i = 0 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

then consider k1 being Integer such that
A12: ( i = goto k1 & m + k1 >= 0 ) by A2, Def11;

A13: now

let a be Int_position ; :: thesis: (Exec i,s1) . a = (Exec i,s2) . a
thus (Exec i,s1) . a = s1 . a by A12, SCMPDS_2:66
.= s2 . a by A6, Th23
.= (Exec i,s2) . a by A12, SCMPDS_2:66 ; :: thesis: verum

end;

IC (Exec i,s1) = ICplusConst s1,k1 by A12, SCMPDS_2:66;
hence (IC (Exec i,s1)) + n = ICplusConst s2,k1 by A1, A5, A12, Th82
.= IC (Exec i,s2) by A12, SCMPDS_2:66 ;
:: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A13, Th23; :: thesis: verum

end;

suppose A14: InsCode i = 2 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A16: now

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

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

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

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

end;

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

hence (Exec i,s1) . b = s1 . b by A15, SCMPDS_2:57
.= s2 . b by A6, Th23
.= (Exec i,s2) . b by A15, A18, SCMPDS_2:57 ;
:: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A14; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A16, Th23; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

then consider a being Int_position , k1, k2 being Integer such that
A19: ( i = a,k1 <>0_goto k2 & m + k2 >= 0 ) by A2, Def11;

A20: 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 A6, Th23
.= (Exec i,s2) . a by A19, SCMPDS_2:67 ; :: thesis: verum

end;

hereby :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

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)) + n = IC (Exec i,s2)

then A22: s2 . (DataLoc (s2 . a),k1) <> 0 by A11;
IC (Exec i,s1) = ICplusConst s1,k2 by A19, A21, SCMPDS_2:67;
hence (IC (Exec i,s1)) + n = ICplusConst s2,k2 by A1, A5, A19, Th82
.= 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)) + n = IC (Exec i,s2)

then A24: s2 . (DataLoc (s2 . a),k1) = 0 by A11;
IC (Exec i,s1) = Next (IC s1) by A19, A23, SCMPDS_2:67;
hence (IC (Exec i,s1)) + n = IC (Exec i,s2) by A8, A19, A24, SCMPDS_2:67; :: thesis: verum

end;

end;

end;

thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A20, Th23; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

then consider a being Int_position , k1, k2 being Integer such that
A25: ( i = a,k1 <=0_goto k2 & m + k2 >= 0 ) by A2, Def11;

A26: 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 A6, Th23
.= (Exec i,s2) . a by A25, SCMPDS_2:68 ; :: thesis: verum

end;

hereby :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

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)) + n = IC (Exec i,s2)

then A28: s2 . (DataLoc (s2 . a),k1) <= 0 by A11;
IC (Exec i,s1) = ICplusConst s1,k2 by A25, A27, SCMPDS_2:68;
hence (IC (Exec i,s1)) + n = ICplusConst s2,k2 by A1, A5, A25, Th82
.= 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)) + n = IC (Exec i,s2)

then A30: s2 . (DataLoc (s2 . a),k1) > 0 by A11;
IC (Exec i,s1) = Next (IC s1) by A25, A29, SCMPDS_2:68;
hence (IC (Exec i,s1)) + n = IC (Exec i,s2) by A8, A25, A30, SCMPDS_2:68; :: thesis: verum

end;

end;

end;

thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A26, Th23; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

then consider a being Int_position , k1, k2 being Integer such that
A31: ( i = a,k1 >=0_goto k2 & m + k2 >= 0 ) by A2, Def11;

A32: 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 A6, Th23
.= (Exec i,s2) . a by A31, SCMPDS_2:69 ; :: thesis: verum

end;

hereby :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

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)) + n = IC (Exec i,s2)

then A34: s2 . (DataLoc (s2 . a),k1) >= 0 by A11;
IC (Exec i,s1) = ICplusConst s1,k2 by A31, A33, SCMPDS_2:69;
hence (IC (Exec i,s1)) + n = ICplusConst s2,k2 by A1, A5, A31, Th82
.= 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)) + n = IC (Exec i,s2)

then A36: s2 . (DataLoc (s2 . a),k1) < 0 by A11;
IC (Exec i,s1) = Next (IC s1) by A31, A35, SCMPDS_2:69;
hence (IC (Exec i,s1)) + n = IC (Exec i,s2) by A8, A31, A36, SCMPDS_2:69; :: thesis: verum

end;

end;

end;

thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A32, Th23; :: thesis: verum

end;

suppose A37: InsCode i = 7 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A39: 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 A40: DataLoc (s1 . a),k1 = b ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A41: DataLoc (s2 . a),k1 = b by A6, Th23;
thus (Exec i,s1) . b = k2 by A38, A40, SCMPDS_2:58
.= (Exec i,s2) . b by A38, A41, SCMPDS_2:58 ; :: thesis: verum

end;

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

then A43: DataLoc (s2 . a),k1 <> b by A6, Th23;
thus (Exec i,s1) . b = s1 . b by A38, A42, SCMPDS_2:58
.= s2 . b by A6, Th23
.= (Exec i,s2) . b by A38, A43, SCMPDS_2:58 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A37; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A39, Th23; :: thesis: verum

end;

suppose A44: InsCode i = 8 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A46: 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 A47: DataLoc (s1 . a),k1 = b ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A48: DataLoc (s2 . a),k1 = b by A6, Th23;
thus (Exec i,s1) . b = (s1 . (DataLoc (s1 . a),k1)) + k2 by A45, A47, SCMPDS_2:60
.= (s2 . (DataLoc (s2 . a),k1)) + k2 by A11
.= (Exec i,s2) . b by A45, A48, SCMPDS_2:60 ; :: thesis: verum

end;

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

then A50: DataLoc (s2 . a),k1 <> b by A6, Th23;
thus (Exec i,s1) . b = s1 . b by A45, A49, SCMPDS_2:60
.= s2 . b by A6, Th23
.= (Exec i,s2) . b by A45, A50, SCMPDS_2:60 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A44; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A46, Th23; :: thesis: verum

end;

suppose A51: InsCode i = 9 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A53: 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 A54: DataLoc (s1 . a),k1 = c ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A55: DataLoc (s2 . a),k1 = c by A6, Th23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) + (s1 . (DataLoc (s1 . b),k2)) by A52, A54, SCMPDS_2:61
.= (s2 . (DataLoc (s2 . a),k1)) + (s1 . (DataLoc (s1 . b),k2)) by A11
.= (s2 . (DataLoc (s2 . a),k1)) + (s2 . (DataLoc (s2 . b),k2)) by A11
.= (Exec i,s2) . c by A52, A55, SCMPDS_2:61 ; :: thesis: verum

end;

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

then A57: DataLoc (s2 . a),k1 <> c by A6, Th23;
thus (Exec i,s1) . c = s1 . c by A52, A56, SCMPDS_2:61
.= s2 . c by A6, Th23
.= (Exec i,s2) . c by A52, A57, SCMPDS_2:61 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A51; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A53, Th23; :: thesis: verum

end;

suppose A58: InsCode i = 10 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A60: 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 A61: DataLoc (s1 . a),k1 = c ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A62: DataLoc (s2 . a),k1 = c by A6, Th23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) - (s1 . (DataLoc (s1 . b),k2)) by A59, A61, SCMPDS_2:62
.= (s2 . (DataLoc (s2 . a),k1)) - (s1 . (DataLoc (s1 . b),k2)) by A11
.= (s2 . (DataLoc (s2 . a),k1)) - (s2 . (DataLoc (s2 . b),k2)) by A11
.= (Exec i,s2) . c by A59, A62, SCMPDS_2:62 ; :: thesis: verum

end;

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

then A64: DataLoc (s2 . a),k1 <> c by A6, Th23;
thus (Exec i,s1) . c = s1 . c by A59, A63, SCMPDS_2:62
.= s2 . c by A6, Th23
.= (Exec i,s2) . c by A59, A64, SCMPDS_2:62 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A58; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A60, Th23; :: thesis: verum

end;

suppose A65: InsCode i = 11 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A67: 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 A68: DataLoc (s1 . a),k1 = c ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A69: DataLoc (s2 . a),k1 = c by A6, Th23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) * (s1 . (DataLoc (s1 . b),k2)) by A66, A68, SCMPDS_2:63
.= (s2 . (DataLoc (s2 . a),k1)) * (s1 . (DataLoc (s1 . b),k2)) by A11
.= (s2 . (DataLoc (s2 . a),k1)) * (s2 . (DataLoc (s2 . b),k2)) by A11
.= (Exec i,s2) . c by A66, A69, SCMPDS_2:63 ; :: thesis: verum

end;

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

then A71: DataLoc (s2 . a),k1 <> c by A6, Th23;
thus (Exec i,s1) . c = s1 . c by A66, A70, SCMPDS_2:63
.= s2 . c by A6, Th23
.= (Exec i,s2) . c by A66, A71, SCMPDS_2:63 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A65; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A67, Th23; :: thesis: verum

end;

suppose A72: InsCode i = 12 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A74: 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 A75: DataLoc (s1 . b),k2 = c ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A76: DataLoc (s2 . b),k2 = c by A6, Th23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2)) by A73, A75, SCMPDS_2:64
.= (s2 . (DataLoc (s2 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2)) by A11
.= (s2 . (DataLoc (s2 . a),k1)) mod (s2 . (DataLoc (s2 . b),k2)) by A11
.= (Exec i,s2) . c by A73, A76, SCMPDS_2:64 ; :: thesis: verum

end;

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

then A78: DataLoc (s2 . b),k2 <> c by A6, Th23;

hereby :: thesis: verum

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

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

then A80: DataLoc (s2 . a),k1 <> c by A6, Th23;
thus (Exec i,s1) . c = s1 . c by A73, A77, A79, SCMPDS_2:64
.= s2 . c by A6, Th23
.= (Exec i,s2) . c by A73, A78, A80, SCMPDS_2:64 ; :: thesis: verum

end;

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

then A82: DataLoc (s2 . a),k1 = c by A6, Th23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) div (s1 . (DataLoc (s1 . b),k2)) by A73, A77, A81, SCMPDS_2:64
.= (s2 . (DataLoc (s2 . a),k1)) div (s1 . (DataLoc (s1 . b),k2)) by A11
.= (s2 . (DataLoc (s2 . a),k1)) div (s2 . (DataLoc (s2 . b),k2)) by A11
.= (Exec i,s2) . c by A73, A78, A82, SCMPDS_2:64 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A72; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A74, Th23; :: thesis: verum

end;

suppose A83: InsCode i = 13 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

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

A85: 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 A86: DataLoc (s1 . a),k1 = c ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A87: DataLoc (s2 . a),k1 = c by A6, Th23;
thus (Exec i,s1) . c = s1 . (DataLoc (s1 . b),k2) by A84, A86, SCMPDS_2:59
.= s2 . (DataLoc (s2 . b),k2) by A11
.= (Exec i,s2) . c by A84, A87, SCMPDS_2:59 ; :: thesis: verum

end;

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

then A89: DataLoc (s2 . a),k1 <> c by A6, Th23;
thus (Exec i,s1) . c = s1 . c by A84, A88, SCMPDS_2:59
.= s2 . c by A6, Th23
.= (Exec i,s2) . c by A84, A89, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

thus (IC (Exec i,s1)) + n = IC (Exec i,s2) by A9, A83; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
thus DataPart (Exec i,s1) = DataPart (Exec i,s2) by A85, Th23; :: thesis: verum

end;

end;