[Prev][Next][Index]

# Re: HELP on proving SetBasics.lsl

bassi@cs.unibo.it (Alberto Bassi) wrote:
>I'm a beginner in LP (Larch Prover) and I'm not able to prove the implies
>part of the SetBasics.lsl library trait.
>Can someone help me?

To prove the implied equations, try instantiating the deduction rule LP
obtains from "C partitioned by \in".  To prove the "converts", try induction.

>Where can I find the demonstrations of the standard library trait?

The on-line documentation for LP (Version 3.1) contains sample proofs
based on the axioms in SetBasics.



Reference(s):