first_x_assum(qspec_then`1`mp_tac)
On Thu, Jul 10, 2014 at 3:02 PM, David Sanan <david.sa...@nus.edu.sg> wrote:
> Hi all,
>
>
> I am trying to prove this goal and n=1 in assumption 2 is a counterexample
> leading to ¬(¬TCn R n x x ∨ ∃n'. TCn R n' x x ∧ n' < n), where TCn is the
> NRC relation without reflexivity and ∀n. TCn R n x y ⇒ n>0.
>
> F
> ------------------------------------
> 0. unique_suc R
> 1. R⁺ x x
> 2. ∀n. ¬TCn R n x x ∨ ∃n'. TCn R n' x x ∧ n' < n
> 3. TCn R m x x
>
> Is it possible to provide a witness to produce a counterexample?
>
> Many thanks,
> David.
>
> ------------------------------------------------------------------------------
> Open source business process management suite built on Java and Eclipse
> Turn processes into business applications with Bonita BPM Community Edition
> Quickly connect people, data, and systems into organized workflows
> Winner of BOSSIE, CODIE, OW2 and Gartner awards
> http://p.sf.net/sfu/Bonitasoft
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
