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

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

then consider k1 being Element of INT such that
A1: I = [0 ,<*k1*>] ;
thus InsCode I <= 13 by A1, MCART_1:7; :: thesis: verum

end;

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

then consider d1 being Element of SCM-Data-Loc such that
A2: I = [1,<*d1*>] ;
I `1 = 1 by A2, MCART_1:7;
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
A3: I = [I1,<*d1,k1*>] and
A4: I1 in {2,3} ;
A5: ( I1 = 2 or I1 = 3 ) by A4, TARSKI:def 2;
I `1 = I1 by A3, MCART_1:7;
hence InsCode I <= 13 by A5; :: 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
A6: I = [I1,<*d1,k1,k2*>] and
A7: I1 in {4,5,6,7,8} ;
A8: ( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A7, ENUMSET1:def 3;
I `1 = I1 by A6, MCART_1:7;
hence InsCode I <= 13 by A8; :: 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
A9: I = [I1,<*d1,d2,k1,k2*>] and
A10: I1 in {9,10,11,12,13} ;
A11: ( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A10, ENUMSET1:def 3;
I `1 = I1 by A9, MCART_1:7;
hence InsCode I <= 13 by A11; :: thesis: verum

end;

end;