Skip to Content.
Sympa Menu

coq-club - Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)

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: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
  • To: Edsko de Vries <edskodevries AT gmail.com>
  • Cc: Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>, Agda list <agda AT lists.chalmers.se>, Coq Club <coq-club AT pauillac.inria.fr>
  • 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:59:39 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
It is sound but useless.

T.

On 1 Sep 2009, at 14:49, Edsko de Vries wrote:

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
_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.



Archive powered by MhonArc 2.6.16.

Top of Page