let i be Instruction of SCMPDS ; :: thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 & InsCode i <> 3 holds
DataPart (Exec i,s1) = DataPart (Exec i,s2)
let s1, s2 be State of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 & InsCode i <> 3 implies DataPart (Exec i,s1) = DataPart (Exec i,s2) )
assume A1: ( DataPart s1 = DataPart s2 & InsCode i <> 3 ) ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

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

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

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

now

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

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

now

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

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

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

hence (Exec i,s1) . b = s1 . (DataLoc (s1 . a),RetSP ) by A3, SCMPDS_2:70
.= s2 . (DataLoc (s2 . a),RetSP ) by A1, SCMPDS_3:3
.= (Exec i,s2) . b by A3, A4, SCMPDS_2:70 ;
:: thesis: verum

end;

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

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

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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 = k1 by A6, SCMPDS_2:57
.= (Exec i,s2) . b by A6, A7, SCMPDS_2:57 ;
:: thesis: verum

end;

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

hence (Exec i,s1) . b = s1 . b by A6, SCMPDS_2:57
.= s2 . b by A1, SCMPDS_4:23
.= (Exec i,s2) . b by A6, A8, SCMPDS_2:57 ;
:: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

now

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

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

now

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

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

now

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

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A14: DataLoc (s2 . a),k1 = b by A1, SCMPDS_4:23;
thus (Exec i,s1) . b = k2 by A12, A13, SCMPDS_2:58
.= (Exec i,s2) . b by A12, A14, SCMPDS_2:58 ; :: thesis: verum

end;

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

then A16: DataLoc (s2 . a),k1 <> b by A1, SCMPDS_4:23;
thus (Exec i,s1) . b = s1 . b by A12, A15, SCMPDS_2:58
.= s2 . b by A1, SCMPDS_4:23
.= (Exec i,s2) . b by A12, A16, SCMPDS_2:58 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A19: DataLoc (s2 . a),k1 = b by A1, SCMPDS_4:23;
thus (Exec i,s1) . b = (s1 . (DataLoc (s1 . a),k1)) + k2 by A17, A18, SCMPDS_2:60
.= (s2 . (DataLoc (s2 . a),k1)) + k2 by A1, SCMPDS_3:3
.= (Exec i,s2) . b by A17, A19, SCMPDS_2:60 ; :: thesis: verum

end;

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

then A21: DataLoc (s2 . a),k1 <> b by A1, SCMPDS_4:23;
thus (Exec i,s1) . b = s1 . b by A17, A20, SCMPDS_2:60
.= s2 . b by A1, SCMPDS_4:23
.= (Exec i,s2) . b by A17, A21, SCMPDS_2:60 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A24: DataLoc (s2 . a),k1 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) + (s1 . (DataLoc (s1 . b),k2)) by A22, A23, SCMPDS_2:61
.= (s2 . (DataLoc (s2 . a),k1)) + (s1 . (DataLoc (s1 . b),k2)) by A1, SCMPDS_3:3
.= (s2 . (DataLoc (s2 . a),k1)) + (s2 . (DataLoc (s2 . b),k2)) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A22, A24, SCMPDS_2:61 ; :: thesis: verum

end;

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

then A26: DataLoc (s2 . a),k1 <> c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . c by A22, A25, SCMPDS_2:61
.= s2 . c by A1, SCMPDS_4:23
.= (Exec i,s2) . c by A22, A26, SCMPDS_2:61 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A29: DataLoc (s2 . a),k1 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) - (s1 . (DataLoc (s1 . b),k2)) by A27, A28, SCMPDS_2:62
.= (s2 . (DataLoc (s2 . a),k1)) - (s1 . (DataLoc (s1 . b),k2)) by A1, SCMPDS_3:3
.= (s2 . (DataLoc (s2 . a),k1)) - (s2 . (DataLoc (s2 . b),k2)) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A27, A29, SCMPDS_2:62 ; :: thesis: verum

end;

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

then A31: DataLoc (s2 . a),k1 <> c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . c by A27, A30, SCMPDS_2:62
.= s2 . c by A1, SCMPDS_4:23
.= (Exec i,s2) . c by A27, A31, SCMPDS_2:62 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A34: DataLoc (s2 . a),k1 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) * (s1 . (DataLoc (s1 . b),k2)) by A32, A33, SCMPDS_2:63
.= (s2 . (DataLoc (s2 . a),k1)) * (s1 . (DataLoc (s1 . b),k2)) by A1, SCMPDS_3:3
.= (s2 . (DataLoc (s2 . a),k1)) * (s2 . (DataLoc (s2 . b),k2)) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A32, A34, SCMPDS_2:63 ; :: thesis: verum

end;

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

then A36: DataLoc (s2 . a),k1 <> c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . c by A32, A35, SCMPDS_2:63
.= s2 . c by A1, SCMPDS_4:23
.= (Exec i,s2) . c by A32, A36, SCMPDS_2:63 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A39: DataLoc (s2 . b),k2 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2)) by A37, A38, SCMPDS_2:64
.= (s2 . (DataLoc (s2 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2)) by A1, SCMPDS_3:3
.= (s2 . (DataLoc (s2 . a),k1)) mod (s2 . (DataLoc (s2 . b),k2)) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A37, A39, SCMPDS_2:64 ; :: thesis: verum

end;

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

then A41: DataLoc (s2 . b),k2 <> c by A1, SCMPDS_4:23;

hereby :: thesis: verum

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

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

then A43: DataLoc (s2 . a),k1 <> c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . c by A37, A40, A42, SCMPDS_2:64
.= s2 . c by A1, SCMPDS_4:23
.= (Exec i,s2) . c by A37, A41, A43, SCMPDS_2:64 ; :: thesis: verum

end;

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

then A45: DataLoc (s2 . a),k1 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = (s1 . (DataLoc (s1 . a),k1)) div (s1 . (DataLoc (s1 . b),k2)) by A37, A40, A44, SCMPDS_2:64
.= (s2 . (DataLoc (s2 . a),k1)) div (s1 . (DataLoc (s1 . b),k2)) by A1, SCMPDS_3:3
.= (s2 . (DataLoc (s2 . a),k1)) div (s2 . (DataLoc (s2 . b),k2)) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A37, A41, A45, SCMPDS_2:64 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

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

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

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

then A48: DataLoc (s2 . a),k1 = c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . (DataLoc (s1 . b),k2) by A46, A47, SCMPDS_2:59
.= s2 . (DataLoc (s2 . b),k2) by A1, SCMPDS_3:3
.= (Exec i,s2) . c by A46, A48, SCMPDS_2:59 ; :: thesis: verum

end;

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

then A50: DataLoc (s2 . a),k1 <> c by A1, SCMPDS_4:23;
thus (Exec i,s1) . c = s1 . c by A46, A49, SCMPDS_2:59
.= s2 . c by A1, SCMPDS_4:23
.= (Exec i,s2) . c by A46, A50, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by SCMPDS_4:23; :: thesis: verum

end;

end;