set w = the State of (SCM S);
consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def 18;
reconsider e = e as Element of S ;
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e));
A2: dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then A3: dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by TARSKI:def 2;
A4: InsCode (p := q) = 1
.= InsCode ((dl. (S,0)) := (dl. (S,1))) ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A5: dl. (S,0) in Data-Locations by SCMRING2:22;
dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by A2, TARSKI:def 2;
then A6: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,0)) by FUNCT_4:13
.= 0. S by AMI_3:10, FUNCT_4:63 ;
(Exec (((dl. (S,0)) := (dl. (S,1))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))))) . (dl. (S,0)) = ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) by SCMRING2:11
.= (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1)) by A3, FUNCT_4:13
.= e by FUNCT_4:63 ;
hence for b₁ being InsType of the InstructionsF of (SCM S) st b₁ = InsCode (p := q) holds
not b₁ is jump-only by A1, A4, A6, A5; :: thesis: verum