let x be set ; :: thesis: for a2 being Nat

for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

let a2 be Nat; :: thesis: for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

let b2 be Element of SCM-Data-Loc ; :: thesis: ( x in {7,8} implies [x,<*a2*>,<*b2*>] in SCM-Instr )

assume A1: x in {7,8} ; :: thesis: [x,<*a2*>,<*b2*>] in SCM-Instr

then ( x = 7 or x = 8 ) by TARSKI:def 2;

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

[x,<*a2*>,<*b2*>] in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by A1;

then [x,<*a2*>,<*b2*>] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by XBOOLE_0:def 3;

hence [x,<*a2*>,<*b2*>] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum

for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

let a2 be Nat; :: thesis: for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

let b2 be Element of SCM-Data-Loc ; :: thesis: ( x in {7,8} implies [x,<*a2*>,<*b2*>] in SCM-Instr )

assume A1: x in {7,8} ; :: thesis: [x,<*a2*>,<*b2*>] in SCM-Instr

then ( x = 7 or x = 8 ) by TARSKI:def 2;

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

[x,<*a2*>,<*b2*>] in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by A1;

then [x,<*a2*>,<*b2*>] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by XBOOLE_0:def 3;

hence [x,<*a2*>,<*b2*>] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum