let
I
be
Instruction
of
(
STC
N
)
;
:: thesis:
I
is
ins-loc-free
I
in
the
InstructionsF
of
(
STC
N
)
;
then
I
in
{
[
0
,
0
,
0
]
,
[
1,
0
,
0
]
}
by
Def7
;
then
(
I
=
[
0
,
0
,
0
]
or
I
=
[
1,
0
,
0
]
)
by
TARSKI:def 2
;
hence
JumpPart
I
is
empty
;
:: according to
COMPOS_0:def 8
:: thesis:
verum