[Prev][Next][Index]
How do I prove an asserted fact with LP?
Consider the following simple LP script
 declare sort S
 declare op s: > S
 declare var x: S
 assert x = s
 prove x = s
Executing this script results in the following fact:
 % display facts

 Formulas:

 user.1: x = s
and the proof is suspended:
 % display proof

 Conjecture user.2: x = s
 Attempting a proof by normalization

At this point, how can I make use of the fact `user.1' to prove the conjecture
`user.2'? I have tried the apply command, but that doesn't help: the system
still considers ``x = s'' to be in normal form.
I have found a workaround (although I hope there is another way): if I
assert ``(x = s) = true'' instead of ``x = s'' the proof succeeds

 Conjecture user.2
 [] Proved by normalization.

even though we seem to have the same facts
 % display facts

 Formulas:

 user.1: x = s
Patrice
FollowUp(s):