Define ngraphOf and nagEval functions

- ngraphOf turns a program into a nested graph.
- nagEval evaluates a nested graph.

These are analogues of pcg_eval and graphOf in PseudoCPropsTheory.
Modify eval definition to keep completed commands under the Seq.

So, an evaluation might look like

  Seq [c1; c2; c3] --> Seq[c1'; c2; c3] --> Seq[Done; c2; c3] -->
  Seq [Done; c2'; c3] --> Seq [Done; Done; c3] -->
  Seq [Done; Done; Done] --> Done

This avoids the need to relabel sub-graphs when converting successive
stages into graphs. The difference with the Par is the side-condition
on the Seq rule which requires all predecessors of c0 to be Done
before it can start to be evaluated.

All the old theorems are still true (after tweaking tactics).

This is very similar to what was done in d328130.
Theorems about nested action graphs and their construction.