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
