set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0));
A15: InsCode (MultBy (a,b)) = 4 by SCMFSA_2:21
.= InsCode (MultBy ((intloc 0),(intloc 1))) by SCMFSA_2:21 ;
A16: dom (((intloc 0),(intloc 1)) --> (1,0)) = {(intloc 0),(intloc 1)} by FUNCT_4:62;
then intloc 0 in dom (((intloc 0),(intloc 1)) --> (1,0)) by TARSKI:def 2;
then A17: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 0) = (((intloc 0),(intloc 1)) --> (1,0)) . (intloc 0) by FUNCT_4:13
.= 1 by AMI_3:10, FUNCT_4:63 ;
intloc 0 in Int-Locations by AMI_2:def 16;
then A18: intloc 0 in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
intloc 1 in dom (((intloc 0),(intloc 1)) --> (1,0)) by A16, TARSKI:def 2;
then A19: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 1) = (((intloc 0),(intloc 1)) --> (1,0)) . (intloc 1) by FUNCT_4:13
.= 0 by FUNCT_4:63 ;
(Exec ((MultBy ((intloc 0),(intloc 1))),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))))) . (intloc 0) = (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 0)) * (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 1)) by SCMFSA_2:66
.= 0 by A19 ;
hence for b₁ being InsType of the InstructionsF of SCM+FSA st b₁ = InsCode (MultBy (a,b)) holds
not b₁ is jump-only by A15, A17, A18; :: thesis: verum