let I be Instruction of SCMPDS; ( not I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
assume
I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} }
; ( InsCode I = 2 or InsCode I = 3 )
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A1:
I = [I1,{},<*d1,k1*>]
and
A2:
I1 in {2,3}
;
( I1 = 2 or I1 = 3 )
by A2, TARSKI:def 2;
hence
( InsCode I = 2 or InsCode I = 3 )
by A1; verum