let I be Instruction of SCM+FSA ; :: thesis: InsCode I <= 12
A1: ( I in SCM-Instr \/ { [L,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or I in { [K,<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;

per cases ( I in SCM-Instr or I in { [L,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or I in { [K,<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by A1, XBOOLE_0:def 3;

suppose I in SCM-Instr ; :: thesis: InsCode I <= 12

then reconsider i = I as Instruction of SCM ;
InsCode i <= 8 by AMI_5:36;
hence InsCode I <= 12 by XXREAL_0:2; :: thesis: verum

end;

suppose I in { [L,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; :: thesis: InsCode I <= 12

then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A2: I = [L,<*dB,fA,dA*>] and
A3: L in {9,10} ;
A4: ( L = 9 or L = 10 ) by A3, TARSKI:def 2;
I `1 = L by A2, MCART_1:7;
hence InsCode I <= 12 by A4; :: thesis: verum

end;

suppose I in { [K,<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: InsCode I <= 12

then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A5: I = [K,<*dC,fB*>] and
A6: K in {11,12} ;
A7: ( K = 11 or K = 12 ) by A6, TARSKI:def 2;
I `1 = K by A5, MCART_1:7;
hence InsCode I <= 12 by A7; :: thesis: verum

end;

end;