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
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