[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):