What Happens Next?
Verify extensibility to other domains, particularly automata theory and code verification
Refine notion of trivial proof
Determine which of logically equivalent forms of expressions to use
Continue to explore gap between information needed for proof and information needed for communication