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