IC (SCM S) = IC SCM by AMI_3:4, SCMRING2:9;
then A1: ( 0. S <> 1_ S & dl. S,0 <> IC (SCM S) ) by AMI_3:57, LMOD_6:def 2;
consider w being State of (SCM S);
set t = w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S));
A2: InsCode (MultBy p,q) = 4 by RECDEF_2:def 1
.= InsCode (MultBy (dl. S,0 ),(dl. S,1)) by RECDEF_2:def 1 ;
A3: dom ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)) = {(dl. S,0 ),(dl. S,1)} by FUNCT_4:65;
then dl. S,0 in dom ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)) by TARSKI:def 2;
then A4: (w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S))) . (dl. S,0 ) = ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)) . (dl. S,0 ) by FUNCT_4:14
.= 1_ S by AMI_3:52, FUNCT_4:66 ;
dl. S,1 in dom ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)) by A3, TARSKI:def 2;
then A5: (w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S))) . (dl. S,1) = ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)) . (dl. S,1) by FUNCT_4:14
.= 0. S by FUNCT_4:66 ;
(Exec (MultBy (dl. S,0 ),(dl. S,1)),(w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S)))) . (dl. S,0 ) = ((w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S))) . (dl. S,0 )) * ((w +* ((dl. S,0 ),(dl. S,1) --> (1_ S),(0. S))) . (dl. S,1)) by SCMRING2:16
.= 0. S by A5, VECTSP_1:36 ;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (MultBy p,q) holds
not b₁ is jump-only by A2, A1, A4, AMISTD_1:def 3; :: thesis: verum