ObjectKind (intloc 0 ) = INT by SCMFSA_2:26;
then reconsider D = 1 as Element of ObjectKind (intloc 0 ) by INT_1:def 1;
reconsider DWA = 2 as Element of INT by INT_1:def 1;
consider w being State of SCM+FSA ;
A8: InsCode (f,a := b) = 10 by SCMFSA_2:51
.= InsCode ((fsloc 0 ),(intloc 1) := (intloc 0 )) by SCMFSA_2:51 ;
ObjectKind (intloc 1) = INT by SCMFSA_2:26;
then reconsider E = 1 as Element of ObjectKind (intloc 1) by INT_1:def 1;
A9: fsloc 0 <> IC SCM+FSA by SCMFSA_2:82;
<*DWA*> in INT * by FINSEQ_1:def 11;
then reconsider F = <*2*> as Element of ObjectKind (fsloc 0 ) by SCMFSA_2:27;
set t = ((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E);
consider k being Element of NAT such that
A10: k = abs ((((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (intloc 1)) and
A11: (Exec ((fsloc 0 ),(intloc 1) := (intloc 0 )),(((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E))) . (fsloc 0 ) = ((((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (fsloc 0 )) +* k,((((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (intloc 0 )) by SCMFSA_2:99;
(((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (intloc 1) = E by FUNCT_7:96;
then A12: k = 1 by A10, ABSVALUE:def 1;
A13: F <> <*D*> by FINSEQ_1:97;
A14: (((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (fsloc 0 ) = F by Lm8, Lm9, FUNCT_7:116;
(((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E)) . (intloc 0 ) = D by AMI_3:52, BVFUNC14:15;
then (Exec ((fsloc 0 ),(intloc 1) := (intloc 0 )),(((w +* ((fsloc 0 ) .--> F)) +* ((intloc 0 ) .--> D)) +* ((intloc 1) .--> E))) . (fsloc 0 ) = <*D*> by A14, A11, A12, FUNCT_7:97;
hence for b₁ being InsType of SCM+FSA st b₁ = InsCode (f,a := b) holds
not b₁ is jump-only by A8, A9, A14, A13, AMISTD_1:def 3; :: thesis: verum