set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1));
A1: InsCode (a := b) =
1
by SCMFSA_2:18
.=
InsCode ((intloc 0) := (intloc 1))
by SCMFSA_2:18
;
A2:
dom (((intloc 0),(intloc 1)) --> (0,1)) = {(intloc 0),(intloc 1)}
by FUNCT_4:62;
then A3:
intloc 1 in dom (((intloc 0),(intloc 1)) --> (0,1))
by TARSKI:def 2;
intloc 0 in dom (((intloc 0),(intloc 1)) --> (0,1))
by A2, TARSKI:def 2;
then A4: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (intloc 0) =
(((intloc 0),(intloc 1)) --> (0,1)) . (intloc 0)
by FUNCT_4:13
.=
0
by AMI_3:10, FUNCT_4:63
;
intloc 0 in Int-Locations
by AMI_2:def 16;
then A5:
intloc 0 in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
(Exec (((intloc 0) := (intloc 1)),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))))) . (intloc 0) =
( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (intloc 1)
by SCMFSA_2:63
.=
(((intloc 0),(intloc 1)) --> (0,1)) . (intloc 1)
by A3, FUNCT_4:13
.=
1
by FUNCT_4:63
;
hence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a := b) holds
not b1 is jump-only
by A1, A4, A5; verum