coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)
chronological Thread
- From: Edsko de Vries <edskodevries AT gmail.com>
- To: Nils Anders Danielsson <nad AT cs.nott.ac.uk>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>, Agda List <agda AT lists.chalmers.se>
- Subject: Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)
- Date: Tue, 1 Sep 2009 14:49:46 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=GFRgATvLVl/08GdQGPHlDGN1QW2SCbhH1HnPmD+75TtKwI9OJqlmWkeZ91skDBKvwP sNCDNPeLfa1v1BpHV6taC3giQFboQliKJBfRGww8Rmnbvk6cpW33+O5RKfpaRN29mxfS eB63wMSqk3qxddx4uZCJIyMQxbRqq7BKX2lQE=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hmm, well, perhaps it's obvious to you, but it's not obvious to me that adding an inductive transitivity rule to an relation which is probably transitive is not sound..
-E
- Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof), Edsko de Vries
- Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof), Edsko de Vries
- Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof), Thorsten Altenkirch
Archive powered by MhonArc 2.6.16.