Re: HELP on proving SetBasics.lsl

• Subject: Re: HELP on proving SetBasics.lsl
• From: "Stephen J. Garland" <garland@lcs.mit.edu>
• Date: 27 Nov 1995 13:48:48 GMT
• Newsgroups: comp.specification.larch
• Organization: MIT Laboratory for Computer Science
• References: <4949oe$gf4@leporello.cs.unibo.it>

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.

• HELP on proving SetBasics.lsl
• From: bassi@cs.unibo.it (Alberto Bassi)

• Prev: Basic LSL Questions
• Next: HELP on proving SetBasics.lsl
• Index: Larch archive index