let T be InsType of SCM+FSA-Instr; ( ( T = 11 or T = 12 ) implies JumpParts T = {{}} )
assume A1:
( T = 11 or T = 12 )
; JumpParts T = {{}}
then A2:
not T = 0 & ... & not T = 8
;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {{}} c= JumpParts T
let x be
object ;
( x in JumpParts T implies x in {{}} )assume
x in JumpParts T
;
x in {{}}then consider I being
Element of
SCM+FSA-Instr such that A3:
x = JumpPart I
and A4:
InsCode I = T
;
I 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, A4, Th7, A2;
then consider K being
Element of
Segm 13,
c1 being
Element of
SCM-Data-Loc ,
f1 being
Element of
SCM+FSA-Data*-Loc such that A5:
(
I = [K,{},<*c1,f1*>] &
K in {11,12} )
;
x = {}
by A3, A5;
hence
x in {{}}
by TARSKI:def 1;
verum
end;
set a = the Element of SCM-Data-Loc ;
set f = the Element of SCM+FSA-Data*-Loc ;
let x be object ; TARSKI:def 3 ( not x in {{}} or x in JumpParts T )
T in {11,12}
by A1, TARSKI:def 2;
then A6:
[T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>] in SCM+FSA-Instr
by Th5;
assume
x in {{}}
; x in JumpParts T
then
x = {}
by TARSKI:def 1;
then A7:
x = JumpPart [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>]
;
InsCode [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>] = T
;
hence
x in JumpParts T
by A7, A6; verum