set j = the 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:35;
ObjectKind (dl. (S,0)) = the carrier of S by Th1;
then reconsider e = e as Element of ObjectKind (dl. (S,0)) by A2;
reconsider v = (dl. (S,0)) .--> e as PartState of (SCM S) ;
set t = the State of (SCM S) +* v;
dom ((dl. (S,0)) .--> e) = {(dl. (S,0))} by FUNCOP_1:13;
then dl. (S,0) in dom ((dl. (S,0)) .--> e) by TARSKI:def 1;
then A4: ( the State of (SCM S) +* v) . (dl. (S,0)) = ((dl. (S,0)) .--> e) . (dl. (S,0)) by FUNCT_4:13
.= e by FUNCOP_1:72 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A5: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec (((dl. (S,0)) := w),( the State of (SCM S) +* v))) . (dl. (S,0)) = w by SCMRING2:17;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (p := w) holds
not b₁ is jump-only by A3, A1, A4, A5, AMISTD_1:def 1; :: thesis: verum