consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def 19;
reconsider e = e as Element of S ;
consider w being State of (SCM S);
set t = w +* ((dl. S,0 ),(dl. S,1) --> (0. S),e);
A2: InsCode (AddTo p,q) = 2 by MCART_1:def 1
.= InsCode (AddTo (dl. S,0 ),(dl. S,1)) by MCART_1:def 1 ;
IC (SCM S) = IC SCM by AMI_3:4, SCMRING2:9;
then A3: dl. S,0 <> IC (SCM S) by AMI_3:57;
dom ((dl. S,0 ),(dl. S,1) --> (0. S),e) = {(dl. S,0 ),(dl. S,1)} by FUNCT_4:65;
then A4: ( dl. S,0 in dom ((dl. S,0 ),(dl. S,1) --> (0. S),e) & dl. S,1 in dom ((dl. S,0 ),(dl. S,1) --> (0. S),e) ) by TARSKI:def 2;
A5: dl. S,0 <> dl. S,1 by AMI_3:52;
A6: (w +* ((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 A4, FUNCT_4:14
.= 0. S by A5, FUNCT_4:66 ;
A7: (w +* ((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 A4, FUNCT_4:14
.= e by FUNCT_4:66 ;
(Exec (AddTo (dl. S,0 ),(dl. S,1)),(w +* ((dl. S,0 ),(dl. S,1) --> (0. S),e))) . (dl. S,0 ) = ((w +* ((dl. S,0 ),(dl. S,1) --> (0. S),e)) . (dl. S,0 )) + ((w +* ((dl. S,0 ),(dl. S,1) --> (0. S),e)) . (dl. S,1)) by SCMRING2:14
.= e by A6, A7, RLVECT_1:10 ;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (AddTo p,q) holds
not b₁ is jump-only by A1, A2, A3, A6, AMISTD_1:def 3; :: thesis: verum