Re: How do I prove an asserted fact with LP?

The reason that the proof

    declare sort S
    declare op   s: -> S
    declare var  x: S
    assert  x = s
    prove   x = s

does not succeed automatically in LP is that the assertion "x = s" cannot be
oriented into a rewrite rule (because the left side of a rewrite rule cannot be
a variable, and the right side cannot introduce a variable that is not on the
left side).

The work-around succeeds because LP orients the assertion "(x = s) = true" into
the rewrite rule "x = s -> true", which normalizes the conjecture to "true".

The success of the work-around suggests that LP should automatically orient
formulas like "x = s" into rewrite rules "x = s -> true".  I will put that
suggestion on the agenda for a future release.

Another work-around that uses the original unorderable axiom is as follows:
    prove x = s by contradiction
      instantiate x by xc in formula