set j = the State of (SCM S);
A1: InsCode (p := w) = 5
.= InsCode ((dl. (S,0)) := w) ;
the carrier of S <> {w} ;
then consider e being object such that
A2: e in the carrier of S and
A3: e <> w by ZFMISC_1:35;
Values (dl. (S,0)) = the carrier of S by Th1;
then reconsider e = e as Element of Values (dl. (S,0)) by A2;
reconsider v = (dl. (S,0)) .--> e as PartState of (SCM S) ;
set t = the State of (SCM S) +* v;
dl. (S,0) in dom ((dl. (S,0)) .--> e) by TARSKI:def 1;
then A4: ( the State of (SCM S) +* v) . (dl. (S,0)) = ((dl. (S,0)) .--> e) . (dl. (S,0)) by FUNCT_4:13
.= e by FUNCOP_1:72 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A5: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec (((dl. (S,0)) := w),( the State of (SCM S) +* v))) . (dl. (S,0)) = w by SCMRING2:17;
hence for b₁ being InsType of the InstructionsF of (SCM S) st b₁ = InsCode (p := w) holds
not b₁ is jump-only by A3, A1, A4, A5; :: thesis: verum