set w = the State of SCM;
set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3));
A20: InsCode (Divide (a,b)) = 5
.= InsCode (Divide ((dl. 0),(dl. 1))) ;
A21: dom (((dl. 0),(dl. 1)) --> (7,3)) = {(dl. 0),(dl. 1)} by FUNCT_4:62;
then dl. 0 in dom (((dl. 0),(dl. 1)) --> (7,3)) by TARSKI:def 2;
then A22: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (7,3)) . (dl. 0) by FUNCT_4:13
.= 7 by AMI_3:10, FUNCT_4:63 ;
A23: 7 = (2 * 3) + 1 ;
A24: dl. 0 in Data-Locations by AMI_3:28;
dl. 1 in dom (((dl. 0),(dl. 1)) --> (7,3)) by A21, TARSKI:def 2;
then ( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))) . (dl. 1) = (((dl. 0),(dl. 1)) --> (7,3)) . (dl. 1) by FUNCT_4:13
.= 3 by FUNCT_4:63 ;
then (Exec ((Divide ((dl. 0),(dl. 1))),( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))))) . (dl. 0) = 7 div 3 by A22, Lm2, AMI_3:6
.= 2 by A23, NAT_D:def 1 ;
hence for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (Divide (a,b)) holds
not b₁ is jump-only by A20, A22, A24; :: thesis: verum