let f be object ; :: according to FINSEQ_1:def 18 :: thesis: ( not f in proj2 SCM-Instr or f is set )
assume f in proj2 SCM-Instr ; :: thesis: 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} } ; :: thesis: 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;
suppose A3: [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: f is set
per cases ( [y,f] in {[SCM-Halt,{},{}]} or [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) by A3, XBOOLE_0:def 3;
suppose [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: f is set
then ex J being Element of Segm 9 ex a being Nat st
( [y,f] = [J,<*a*>,{}] & J = 6 ) ;
hence f is FinSequence by XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose [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} } ; :: thesis: f is set
then ex K being Element of Segm 9 ex a1 being Nat ex b1 being Element of SCM-Data-Loc st
( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
hence f is FinSequence by XTUPLE_0:1; :: thesis: verum
end;
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} } ; :: thesis: f is set
then ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( [y,f] = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence f is FinSequence by XTUPLE_0:1; :: thesis: verum
end;
end;