let I be Instruction of SCMPDS; :: thesis: InsCode I <= 13

per cases ( 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 Lm2;

suppose I in { [0,{},<*k1*>] where k1 is Element of INT : verum } ; :: thesis: InsCode I <= 13

then ex k1 being Element of INT st I = [0,{},<*k1*>] ;
hence InsCode I <= 13 by RECDEF_2:def 1; :: thesis: verum

end;

suppose I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; :: thesis: InsCode I <= 13

then ex d1 being Element of SCM-Data-Loc st I = [1,{},<*d1*>] ;
then I `1_3 = 1 by RECDEF_2:def 1;
hence InsCode I <= 13 ; :: thesis: verum

end;

suppose 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} } ; :: thesis: InsCode I <= 13

then consider I1 being Element of Segm 14, 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} ;
A3: I `1_3 = I1 by A1, RECDEF_2:def 1;
( I1 = 2 or I1 = 3 ) by A2, TARSKI:def 2;
hence InsCode I <= 13 by A3; :: thesis: verum

end;

suppose 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} } ; :: thesis: InsCode I <= 13

then consider I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A4: I = [I1,{},<*d1,k1,k2*>] and
A5: I1 in {4,5,6,7,8} ;
A6: I `1_3 = I1 by A4, RECDEF_2:def 1;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A5, ENUMSET1:def 3;
hence InsCode I <= 13 by A6; :: thesis: verum

end;

suppose 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} } ; :: thesis: InsCode I <= 13

then consider I1 being Element of Segm 14, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A7: I = [I1,{},<*d1,d2,k1,k2*>] and
A8: I1 in {9,10,11,12,13} ;
A9: I `1_3 = I1 by A7, RECDEF_2:def 1;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A8, ENUMSET1:def 3;
hence InsCode I <= 13 by A9; :: thesis: verum

end;

end;