let I be Instruction of SCMPDS ; :: thesis: ( InsCode I = 10 implies ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 )
assume A1: InsCode I = 10 ; :: thesis: ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2
( I in { [0 ,{} ,<*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 14, 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 14, 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 14, 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 I1 being Element of Segm 14, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{} ,<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm8;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def 3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [10,{} ,<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def 1;
reconsider a = d1, b = d2 as Int_position by Def2;
take a ; :: thesis: ex b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2
take b ; :: thesis: ex k1, k2 being Integer st I = SubFrom a,k1,b,k2
take k1 ; :: thesis: ex k2 being Integer st I = SubFrom a,k1,b,k2
take k2 ; :: thesis: I = SubFrom a,k1,b,k2
thus I = SubFrom a,k1,b,k2 by A4; :: thesis: verum