Library CoLoR.Util.Relation.NotSN_IS

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-08-08
~SN terms give infinite sequences (using classical logic and dependent choice)

Set Implicit Arguments.

Section S.

  Variables (A : Type) (R : relation A).

  Lemma notSN_NT : forall a, ~SN R a -> NT R a.

  Lemma notNT_SN : forall a, ~NT R a -> SN R a.

  Lemma notWF_EIS : ~WF R -> EIS R.

  Lemma SN_notNT_eq : forall x, SN R x <-> ~NT R x.

  Lemma WF_notIS_eq : WF R <-> forall f, ~IS R f.

  Lemma notWF_EIS_eq : ~WF R <-> EIS R.

End S.