Re: [isabelle] Coinduction and induction


On Wed, 2008-07-02 at 22:27 +0800, li yongjian wrote: 
> I may ask a stupid question, here I want to know the meanings of the
> saying "  Coinduction  and induction are a parir  of duals". Does this
> means that if we define
> a set S inductively, then we can define (-S) coinductively?

if f is a monotone function (on a Boolean algebra, say), then

  -(lfp f) = gfp g,

where g(x) := -f(-x).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.