consider j being State of (SCM S);
A1: InsCode (p := w) = 5 by MCART_1:def 1
.= InsCode ((dl. S,0 ) := w) by MCART_1: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 AMI_1:59;
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 ;
IC (SCM S) = IC SCM by AMI_3:4, SCMRING2:9;
then A5: dl. S,0 <> IC (SCM S) by AMI_3:57;
(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, A5, A4, AMISTD_1:def 3; :: thesis: verum