This homework is a set of written and programming exercises due at the
beginning of class next Monday, 14 February.  You can email me your
solutions.

In the 1st lecture, we defined a small-step operational semantics
for IMP.  These questions concern the semantics given there.
Be very careful and very explicit in your proof.  State clearly
your induction hypotheses, bases cases, and inductive cases making
sure to appeal to the induction hypothesis.

(1) Prove that for all e and s there exists a unique i such that 
<e,s> -exp->* <i,s>.  That is, -exp->* defines a total function on
expressions and stores, and that function has no effect on the store.

(2) Prove that for all c and s there exists at most one s' such that
<c,s> ->* <skip,s'>.  That is, ->* defines a partial function on
commands and stores.


(3) Prove that for all c1, c2, c3 and s that <(c1;c2);c3,s> ->* <skip,s'>
iff <c1;(c2;c3),s> ->* <skip,s'>.

(4) Define a small-step semantics for the Greg86.  The Greg86 is 
a MIPS-like machine with the following properties:

(a) all values that are manipulated are 32-bit words
(b) the machine has 4 registers:  pc, sp, a, and b.
(c) the machine supports the following operations:
      r  := i         -- sign-extend and move 26-bit immediate into r
      rd := r1 + r2   -- rd gets sum of r1 and r2 registers
      rd := r1 - r2   -- rd gets difference of r1 and r2 registers
      rd := r1 * r2   -- rd gets product of r1 and r2 registers
      rd := Mem[r1]   -- load from memory
      Mem[r1] := r2   -- store into memory
      if r goto i     -- if r != 0, control transfers to address determined
                         by adding (sign-extended) 26-bit i to current pc.
      goto r          -- control transfers to address in register r
      gosub r         -- same as goto, but return address (current pc + 4) is
                         placed in b
(d) memory is a total map from words to words (i.e., we have all 4 gigabytes
of storage.) 
(e) You may assume that there is a function encode() which maps instances
of the instructions above to a 32-bit integer.  Note that not all integers
correspond to instances of instructions.
(f) For loads, stores, and jumps, the two least significant bits are ignored.