Re: HELP on proving SetBasics.lsl
email@example.com (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.