let f be object ; FINSEQ_1:def 18 ( not f in proj2 SCM-Instr or f is set )
assume
f in proj2 SCM-Instr
; f is set
then consider y being object such that
A1:
[y,f] in SCM-Instr
by XTUPLE_0:def 13;
set x = [y,f];
per cases
( [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 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} } or [y,f] in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } )
by A1, XBOOLE_0:def 3;
suppose A2:
[y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 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} }
;
f is set per cases
( [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } or [y,f] 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 A2, XBOOLE_0:def 3;
end; end; suppose
[y,f] in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} }
;
f is set end; end;