consider j being State of (SCM S);
A1: InsCode (p := w) = 5 by RECDEF_2:def 1
.= InsCode ((dl. (S,0)) := w) by RECDEF_2:def 1 ;
the carrier of S <> {w} ;
then consider e being set such that
A2: e in the carrier of S and
A3: e <> w by ZFMISC_1:41;
reconsider e = e as Element of S by A2;
ObjectKind (dl. (S,0)) = the carrier of S by Th1;
then reconsider v = (dl. (S,0)) .--> e as FinPartState of (SCM S) by COMPOS_1:5;
set t = j +* v;
dom ((dl. (S,0)) .--> e) = {(dl. (S,0))} by FUNCOP_1:19;
then dl. (S,0) in dom ((dl. (S,0)) .--> e) by TARSKI:def 1;
then A4: (j +* v) . (dl. (S,0)) = ((dl. (S,0)) .--> e) . (dl. (S,0)) by FUNCT_4:14
.= e by FUNCOP_1:87 ;
dl. (S,0) in Data-Locations SCM by SCMRING2:1;
then XX: dl. (S,0) in Data-Locations (SCM S) by SCMRING2:31;
(Exec (((dl. (S,0)) := w),(j +* v))) . (dl. (S,0)) = w by SCMRING2:19;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (p := w) holds
not b₁ is jump-only by A3, A1, A4, AMISTD_1:def 3, XX; :: thesis: verum