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_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (Divide (a,b)) holds

not b_{1} is jump-only
by A20, A22, A24; :: thesis: verum

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

not b