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;

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;

end;

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;hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A1; :: thesis: verum

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;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet 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;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

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;

end;A4: i = return a by SCMPDS_2:27;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet b be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A5:
a = b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;.= s2 . (DataLoc ((s2 . a),RetSP)) by A1, SCMPDS_3:2

.= (Exec (i,s2)) . b by A4, A5, SCMPDS_2:58 ;

:: thesis: verum

suppose A6:
a <> b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;.= s2 . b by A1, SCMPDS_4:8

.= (Exec (i,s2)) . b by A4, A6, SCMPDS_2:58 ;

:: thesis: verum

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;

end;A7: i = a := k1 by SCMPDS_2:28;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet b be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A8:
a = b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

hence (Exec (i,s1)) . b =
k1
by A7, SCMPDS_2:45

.= (Exec (i,s2)) . b by A7, A8, SCMPDS_2:45 ;

:: thesis: verum

end;.= (Exec (i,s2)) . b by A7, A8, SCMPDS_2:45 ;

:: thesis: verum

suppose A9:
a <> b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;.= s2 . b by A1, SCMPDS_4:8

.= (Exec (i,s2)) . b by A7, A9, SCMPDS_2:45 ;

:: thesis: verum

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;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet 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;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

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;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet 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;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

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;

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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet 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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet b be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A14:
DataLoc ((s1 . a),k1) = b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;thus (Exec (i,s1)) . b = k2 by A13, A14, SCMPDS_2:46

.= (Exec (i,s2)) . b by A13, A15, SCMPDS_2:46 ; :: thesis: verum

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

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet b be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A19:
DataLoc ((s1 . a),k1) = b
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

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

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet c be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A24:
DataLoc ((s1 . a),k1) = c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

suppose A26:
DataLoc ((s1 . a),k1) <> c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet c be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A29:
DataLoc ((s1 . a),k1) = c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

suppose A31:
DataLoc ((s1 . a),k1) <> c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet c be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A34:
DataLoc ((s1 . a),k1) = c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

suppose A36:
DataLoc ((s1 . a),k1) <> c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet c be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A39:
DataLoc ((s1 . b),k2) = c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

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

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

end;hereby :: thesis: verum
end;

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

end;

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;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

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;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

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;

end;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

hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by SCMPDS_4:8; :: thesis: verumlet c be Int_position; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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

end;

suppose A48:
DataLoc ((s1 . a),k1) = c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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

suppose A50:
DataLoc ((s1 . a),k1) <> c
; :: thesis: (Exec (i,s1)) . b_{1} = (Exec (i,s2)) . b_{1}

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;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