Freshness axioms & prove top-implies-fp

[nishantjr]

This PR contains the following changes:

1. Minor bug fixes and cleanups
2. Relaxing axioms that have a disjointness requirement. For each axiom there are usually two commits: first, rename the old axiom with a _disjoint suffix; second, introduce the new axiom and use it to prove the previous version.
3. Automation in Maude for proving many of this.
4. A test framework for Maude automation. I've not gone full TDD on this, but its very useful for debugging when side conditions don't apply etc.
5. Completion of top-implies-fp proof.

These are some issues that were encountered and will need to be addressed eventually.

1. The Maude SExpr has a constructor for each arity of SExpr needed. This is simple and works, but has reached its limits.

   • Since some theorem applications need us to enumerate the bound variables, we are using as many as 13(!) arguments.
   • It does not allow us to dynamically compute arguments to theorem applications. This is needed, list all the bound variables for the main_goal theorem.
   • Its butt ugly.

   • ... unfortunately, the square bracket syntax conflicts with the syntax in Maude's META-LEVEL module, so the fix needs some additional thought. Here is what the attempted fix looked like:

     -    sort MM0SExpr MM0Atom .
     -    subsort Qid < MM0Atom < MM0SExpr .
     +    sort MM0SExpr MM0Atom NeMM0SExprList MM0SExprList .
     +    subsort Qid < MM0Atom < MM0SExpr < NeMM0SExprList < MM0SExprList .
     
          --- We use square brackets instead of parens for S-Expressions since
          --- Maude treats parens specially.
     -    --- TODO: Consider using List{MM0SExpr}?
     -    op [ _ _ ]        : MM0SExpr MM0SExpr                             -> MM0SExpr .
     -    op [ _ _ _ ]      : MM0SExpr MM0SExpr MM0SExpr                    -> MM0SExpr .
     -    op [ _ _ _ _ ]    : MM0SExpr MM0SExpr MM0SExpr MM0SExpr           -> MM0SExpr .
     -    op [ _ _ _ _ _ ]  : MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr  -> MM0SExpr .
     -    op [ _ _ _ _ _ _ ]
     -                      : MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr  -> MM0SExpr .
     -    op [ _ _ _ _ _ _ _ ]
     -                      : MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr MM0SExpr  -> MM0SExpr .
     +    op nil : -> MM0SExprList [ctor] .
     +    op _ _ : MM0SExprList MM0SExprList -> MM0SExprList [ctor ditto].
     +    op _ _ : NeMM0SExprList MM0SExprList -> NeMM0SExprList [ctor ditto].
     +    op _ _ : MM0SExprList NeMM0SExprList -> NeMM0SExprList [ctor ditto].
     +
     +    op [ _ _ ] : Qid NeMM0SExprList -> MM0SExpr .
     
          sort MM0Decl MM0Binder .

2. The new Maude automation desugars notation internally, instead of calling the lemmas defined for each construct. For example, eFresh(phi or psi) will employ eFresh_not and eFresh_implies instead of directly calling eFresh_or. There is a penalty in the size of the proof, so we want to take care of this eventually.