let I be Instruction of SCMPDS; :: thesis: ( InsCode I = 14 implies ex k1 being Integer st I = goto k1 )
assume A1: InsCode I = 14 ; :: thesis: ex k1 being Integer st I = goto k1
( I in {[0,{},{}]} or I in { [14,{},<*k1*>] where k1 is Element of INT : verum } or I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider k1 being Element of INT such that
A2: I = [14,{},<*k1*>] by A1, Lm3, Lm4, Lm5, Lm6, Lm7;
take k1 ; :: thesis: I = goto k1
thus I = goto k1 by A2; :: thesis: verum