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

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

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

not b