coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Partial Witness

From: Roman Beslik <beroal AT ukr.net>
To: Jeff Terrell <jeff AT kc.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Partial Witness
Date: Sun, 01 Mar 2009 09:41:18 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi.

Why not? Do you mean a strict subset? I.e. (X p' <> Y ...) ?
Jeff Terrell wrote:

Unless the specification is wrong, the intention was for Y to contain a subset of the numbers in X, so that (X p') *wouldn't* be a valid witness for Y. What am I missing?

--
Best regards,
Roman Beslik.

Re: [Coq-Club] Partial Witness, Roman Beslik
- <Possible follow-ups>
- Re: [Coq-Club] Partial Witness, Matthew Brecknell
- Re: [Coq-Club] Partial Witness, Matthew Brecknell
  - Re: [Coq-Club] Partial Witness, Jeff Terrell
    - Re: [Coq-Club] Partial Witness, Adam Chlipala
      - Re: [Coq-Club] Partial Witness, Jeff Terrell
        
        Re: [Coq-Club] Partial Witness, Adam Chlipala
    - Re: [Coq-Club] Partial Witness, Matthew Brecknell
- Re: [Coq-Club] Partial Witness, Hugo Herbelin
  - Re: [Coq-Club] Partial Witness, Adam Chlipala
    - Re: [Coq-Club] Partial Witness, Hugo Herbelin