IC = IC by AMI_3:1, SCMRING2:8;
then A1: ( 0. S <> 1_ S & dl. (S,0) <> IC ) by AMI_3:13, LMOD_6:def 1;
set w = the State of (SCM S);
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)));
A2: InsCode (MultBy (p,q)) = 4
.= InsCode (MultBy ((dl. (S,0)),(dl. (S,1)))) ;
A3: dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by TARSKI:def 2;
then A4: ( the State of (SCM S) +* (((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:13
.= 1_ S by AMI_3:10, FUNCT_4:63 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by A3, TARSKI:def 2;
then A5: ( the State of (SCM S) +* (((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:13
.= 0. S by FUNCT_4:63 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A6: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec ((MultBy ((dl. (S,0)),(dl. (S,1)))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))))) . (dl. (S,0)) = (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,0))) * (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,1))) by SCMRING2:14
.= 0. S by A5 ;
hence for b₁ being InsType of the InstructionsF of (SCM S) st b₁ = InsCode (MultBy (p,q)) holds
not b₁ is jump-only by A2, A1, A4, A6; :: thesis: verum