JAVA+ITP:
********
Description of the commands can be found in the paper (see website),
otherwise the commands are explained by the examples below:

For all examples first do:
- start maude
- type: "in itp-tool.maude"
- type: "in java-es-flat.maude"

In a X.maude file the program and special functions that are necessary
are introduced, in the accompanying X.itp file we either create the
Hoare triples and then first order goals from there or immediately get
FO goals. The necessary commands to discharge the proof obligations are
part of these files and thus automatically executed.

If not otherwise instructed for each example the type:
- type: "in X.maude"
- type: "in X.itp"

----------------------------------------------------------------------
"absx", "facx" (loop included):
- see general explanation

"ht-facx", "ht-swap":
- see general explanation, these use the Hoare triple mechanism, but otherwise
  work the same way.


LARGER EXAMPLE:

"Choose" example:
- type "in ht-choose.maude"
- type "in ht-choose.itp", this creates the 4 Hoare triple goals
- type "in ht-choose-run.it", this will take up to 45 minutes to complete,
  it will create the respective first order goals for all Hoare triples and
  proof them one at a time. There will be one goal left.
- to show the remaining goal keep in mind that in the paper (linked on the
  website) we already mentioned that here we have A,B,C => X and get a non-
  termination. Our alternative is to show A => X and then by transitivity of 
  => we know that A,B,C => X should hold, but the underlying prover cannot show
  it.
  type "in ht-choose-specialcase.itp to see the last goal created again,
  it will be immediately discharged by the module. to create that goal
  we used our usual commands and so 4 goals were created, you can ignore
  the other 3, or if you want discharge them, by typing:
  "in ht-choose-specialcase-rest.itp