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 that
A1: DataPart s1 = DataPart s2 and
A2: InsCode i <> 3 ; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
not not InsCode i = 0 & ... & not InsCode i = 14 by SCMPDS_2:6;

per cases then ( InsCode i = 0 or InsCode i = 14 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 A2;

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

then ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by SCMPDS_2:86;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A1; :: thesis: verum

end;

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

then A3: ex k1 being Integer st i = goto k1 by SCMPDS_2:26;

now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a

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:54
.= s2 . a by A1, SCMPDS_4:8
.= (Exec (i,s2)) . a by A3, SCMPDS_2:54 ; :: thesis: verum

end;

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

end;

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

then consider a being Int_position such that
A4: i = return a by SCMPDS_2:27;

now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b

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

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

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

hence (Exec (i,s1)) . b = s1 . (DataLoc ((s1 . a),RetSP)) by A4, SCMPDS_2:58
.= s2 . (DataLoc ((s2 . a),RetSP)) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . b by A4, A5, SCMPDS_2:58 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . b = s1 . b by A4, SCMPDS_2:58
.= s2 . b by A1, SCMPDS_4:8
.= (Exec (i,s2)) . b by A4, A6, SCMPDS_2:58 ;
:: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A7: i = a := k1 by SCMPDS_2:28;

now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b

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

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

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

hence (Exec (i,s1)) . b = k1 by A7, SCMPDS_2:45
.= (Exec (i,s2)) . b by A7, A8, SCMPDS_2:45 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . b = s1 . b by A7, SCMPDS_2:45
.= s2 . b by A1, SCMPDS_4:8
.= (Exec (i,s2)) . b by A7, A9, SCMPDS_2:45 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then A10: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <>0_goto k2 by SCMPDS_2:30;

now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a

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:55
.= s2 . a by A1, SCMPDS_4:8
.= (Exec (i,s2)) . a by A10, SCMPDS_2:55 ; :: thesis: verum

end;

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

end;

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

then A11: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <=0_goto k2 by SCMPDS_2:31;

now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a

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:56
.= s2 . a by A1, SCMPDS_4:8
.= (Exec (i,s2)) . a by A11, SCMPDS_2:56 ; :: thesis: verum

end;

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

end;

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

then A12: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) >=0_goto k2 by SCMPDS_2:32;

now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a

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:57
.= s2 . a by A1, SCMPDS_4:8
.= (Exec (i,s2)) . a by A12, SCMPDS_2:57 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A13: i = (a,k1) := k2 by SCMPDS_2:33;

now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b

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

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

end;

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

then A17: DataLoc ((s2 . a),k1) <> b by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . b = s1 . b by A13, A16, SCMPDS_2:46
.= s2 . b by A1, SCMPDS_4:8
.= (Exec (i,s2)) . b by A13, A17, SCMPDS_2:46 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A18: i = AddTo (a,k1,k2) by SCMPDS_2:34;

now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b

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

then A20: DataLoc ((s2 . a),k1) = b by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . b = (s1 . (DataLoc ((s1 . a),k1))) + k2 by A18, A19, SCMPDS_2:48
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A1, SCMPDS_3:2
.= (Exec (i,s2)) . b by A18, A20, SCMPDS_2:48 ; :: thesis: verum

end;

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

then A22: DataLoc ((s2 . a),k1) <> b by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . b = s1 . b by A18, A21, SCMPDS_2:48
.= s2 . b by A1, SCMPDS_4:8
.= (Exec (i,s2)) . b by A18, A22, SCMPDS_2:48 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A23: i = AddTo (a,k1,b,k2) by SCMPDS_2:35;

now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c

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

then A25: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A23, A24, SCMPDS_2:49
.= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2
.= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A23, A25, SCMPDS_2:49 ; :: thesis: verum

end;

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

then A27: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . c by A23, A26, SCMPDS_2:49
.= s2 . c by A1, SCMPDS_4:8
.= (Exec (i,s2)) . c by A23, A27, SCMPDS_2:49 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A28: i = SubFrom (a,k1,b,k2) by SCMPDS_2:36;

now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c

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

then A30: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A28, A29, SCMPDS_2:50
.= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2
.= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A28, A30, SCMPDS_2:50 ; :: thesis: verum

end;

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

then A32: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . c by A28, A31, SCMPDS_2:50
.= s2 . c by A1, SCMPDS_4:8
.= (Exec (i,s2)) . c by A28, A32, SCMPDS_2:50 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A33: i = MultBy (a,k1,b,k2) by SCMPDS_2:37;

now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c

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

then A35: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A33, A34, SCMPDS_2:51
.= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2
.= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A33, A35, SCMPDS_2:51 ; :: thesis: verum

end;

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

then A37: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . c by A33, A36, SCMPDS_2:51
.= s2 . c by A1, SCMPDS_4:8
.= (Exec (i,s2)) . c by A33, A37, SCMPDS_2:51 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A38: i = Divide (a,k1,b,k2) by SCMPDS_2:38;

now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c

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

then A40: DataLoc ((s2 . b),k2) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A38, A39, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A38, A40, SCMPDS_2:52 ; :: thesis: verum

end;

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

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

hereby :: thesis: verum

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

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

then A44: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . c by A38, A41, A43, SCMPDS_2:52
.= s2 . c by A1, SCMPDS_4:8
.= (Exec (i,s2)) . c by A38, A42, A44, SCMPDS_2:52 ; :: thesis: verum

end;

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

then A46: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A38, A41, A45, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2
.= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A38, A42, A46, SCMPDS_2:52 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; :: 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
A47: i = (a,k1) := (b,k2) by SCMPDS_2:39;

now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c

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

then A49: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . (DataLoc ((s1 . b),k2)) by A47, A48, SCMPDS_2:47
.= s2 . (DataLoc ((s2 . b),k2)) by A1, SCMPDS_3:2
.= (Exec (i,s2)) . c by A47, A49, SCMPDS_2:47 ; :: thesis: verum

end;

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

then A51: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8;
thus (Exec (i,s1)) . c = s1 . c by A47, A50, SCMPDS_2:47
.= s2 . c by A1, SCMPDS_4:8
.= (Exec (i,s2)) . c by A47, A51, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

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

end;

end;