let I be Instruction of SCM+FSA; ( InsCode I <= 8 implies I is Instruction of SCM )
assume A1:
InsCode I <= 8
; I is Instruction of SCM
now not I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } assume
I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} }
;
contradictionthen consider K being
Element of
Segm 13,
dC being
Element of
SCM+FSA-Data-Loc ,
fB being
Element of
SCM+FSA-Data*-Loc such that A2:
I = [K,{},<*dC,fB*>]
and A3:
K in {11,12}
;
A4:
I `1_3 = K
by A2;
(
K = 12 or
K = 11 )
by A3, TARSKI:def 2;
hence
contradiction
by A1, A4;
verum end;
then A5:
I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }
by XBOOLE_0:def 3;
now not I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } assume
I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }
;
contradictionthen consider L being
Element of
Segm 13,
dA,
dB being
Element of
SCM+FSA-Data-Loc ,
fA being
Element of
SCM+FSA-Data*-Loc such that A6:
I = [L,{},<*dB,fA,dA*>]
and A7:
L in {9,10}
;
A8:
I `1_3 = L
by A6;
(
L = 9 or
L = 10 )
by A7, TARSKI:def 2;
hence
contradiction
by A1, A8;
verum end;
hence
I is Instruction of SCM
by A5, XBOOLE_0:def 3; verum