let x be Element of SCM+FSA-Instr ; :: thesis: ( ( x in SCM-Instr & not not InsCode x = 0 & ... & not InsCode x = 8 ) or ( x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } & ( InsCode x = 11 or InsCode x = 12 ) ) )

( x in SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;

( x in SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;

per cases then
( x in SCM-Instr or x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } )
by XBOOLE_0:def 3;

end;

case
x in SCM-Instr
; :: thesis: not not InsCode x = 0 & ... & not InsCode x = 8

then
InsCode x <= 8
by SCM_INST:10;

then not not InsCode x = 0 & ... & not InsCode x = 8 by NAT_1:60;

hence not not InsCode x = 0 & ... & not InsCode x = 8 ; :: thesis: verum

end;then not not InsCode x = 0 & ... & not InsCode x = 8 by NAT_1:60;

hence not not InsCode x = 0 & ... & not InsCode x = 8 ; :: thesis: verum

case
x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} }
; :: thesis: ( InsCode x = 9 or InsCode x = 10 )

then consider J being Element of Segm 13, b, c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc such that

A1: x = [J,{},<*c,f,b*>] and

A2: J in {9,10} ;

InsCode x = J by A1;

hence ( InsCode x = 9 or InsCode x = 10 ) by A2, TARSKI:def 2; :: thesis: verum

end;A1: x = [J,{},<*c,f,b*>] and

A2: J in {9,10} ;

InsCode x = J by A1;

hence ( InsCode x = 9 or InsCode x = 10 ) by A2, TARSKI:def 2; :: thesis: verum

case
x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} }
; :: thesis: ( InsCode x = 11 or InsCode x = 12 )

then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that

A3: x = [K,{},<*c1,f1*>] and

A4: K in {11,12} ;

InsCode x = K by A3;

hence ( InsCode x = 11 or InsCode x = 12 ) by A4, TARSKI:def 2; :: thesis: verum

end;A3: x = [K,{},<*c1,f1*>] and

A4: K in {11,12} ;

InsCode x = K by A3;

hence ( InsCode x = 11 or InsCode x = 12 ) by A4, TARSKI:def 2; :: thesis: verum