Fix sequence rules

[matt-j-griffin]

The sequencing rules (seq_*) describe execution of a list of BIL statements to completion.

However, the sequencing rules in this manual do not provide a means to reduce multiple statements in a single transition.

i.e. the step rule decodes a program (delta,w,var) into an instruction ({addr=w1; size=w2; code=bil}) and recursively reduces the bil sequence using the sequence rules:

 delta,w,var |-> {addr=w1; size=w2; code=bil}
 delta, w1.+w2 |- bil ~> delta',w3,{}
 ---------------------------------------------------------- :: step
 delta,w,var  ~> delta',w3,var

However, there is no matching sequence rule that can be applied to the second premise in the above inference rule (delta, w1.+w2 |- bil ~> delta',w3,{}).

The rules seq_rec or seq_last require a non-empty sequence of statements on the RHS ({s2; ..; sn}):

delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_rec
delta,word |- {s1; s2; ..; sn} ~> delta', word', {s2; ..; sn}

delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_last
delta,word |- {s1; s2} ~> delta', word', {s2}

The rules seq_one and seq_nil could match the premise, however it would require the sequence to have one (1) or no (0) elements.

 delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_one
 delta,word |- {s1} ~> delta', word', {}


 ------------------------------------------------------------- :: seq_nil
 delta,word |- {} ~> delta, word, {}

The proposed changes fix the syntax/semantics so that they correctly reduce by removing the sequence on the RHS of the transition and adding a recursive call to seq_rec.