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));
A3: InsCode (SubFrom (p,q)) =
3
.=
InsCode (SubFrom ((dl. (S,0)),(dl. (S,1))))
;
A4:
dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))}
by FUNCT_4:62;
then
dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))
by TARSKI:def 2;
then A5: ( 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
;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))
by A4, TARSKI:def 2;
then A6: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) =
(((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1))
by FUNCT_4:13
.=
e
by FUNCT_4:63
;
dl. (S,0) in Data-Locations
by SCMRING2:1;
then A7:
dl. (S,0) in Data-Locations
by SCMRING2:22;
(Exec ((SubFrom ((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,0))) - (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)))
by SCMRING2:13
.=
- e
by A5, A6, RLVECT_1:14
;
hence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (SubFrom (p,q)) holds
not b1 is jump-only
by A3, A5, A2, A7; verum