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_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (MultBy (p,q)) holds

not b_{1} is jump-only
by A2, A1, A4, A6; :: thesis: verum

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

not b