let x be set ; :: thesis: for c being Element of SCM-Data-Loc

for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

let c be Element of SCM-Data-Loc ; :: thesis: for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

let f be Element of SCM+FSA-Data*-Loc ; :: thesis: ( x in {11,12} implies [x,{},<*c,f*>] in SCM+FSA-Instr )

assume A1: x in {11,12} ; :: thesis: [x,{},<*c,f*>] in SCM+FSA-Instr

then ( x = 11 or x = 12 ) by TARSKI:def 2;

then reconsider x = x as Element of Segm 13 by NAT_1:44;

[x,{},<*c,f*>] 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 A1;

then [x,{},<*c,f*>] in (SCM-Instr \/ { [J,{},<*c2,f2,b*>] where J is Element of Segm 13, b, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [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;

then [x,{},<*c,f*>] in (SCM-Instr \/ { [J,{},<*c2,f2,b*>] where J is Element of Segm 13, b, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [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} } ;

hence [x,{},<*c,f*>] in SCM+FSA-Instr ; :: thesis: verum

for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

let c be Element of SCM-Data-Loc ; :: thesis: for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

let f be Element of SCM+FSA-Data*-Loc ; :: thesis: ( x in {11,12} implies [x,{},<*c,f*>] in SCM+FSA-Instr )

assume A1: x in {11,12} ; :: thesis: [x,{},<*c,f*>] in SCM+FSA-Instr

then ( x = 11 or x = 12 ) by TARSKI:def 2;

then reconsider x = x as Element of Segm 13 by NAT_1:44;

[x,{},<*c,f*>] 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 A1;

then [x,{},<*c,f*>] in (SCM-Instr \/ { [J,{},<*c2,f2,b*>] where J is Element of Segm 13, b, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [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;

then [x,{},<*c,f*>] in (SCM-Instr \/ { [J,{},<*c2,f2,b*>] where J is Element of Segm 13, b, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [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} } ;

hence [x,{},<*c,f*>] in SCM+FSA-Instr ; :: thesis: verum