[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

well foundedness properties


Has anyone developed theories around well founded relations?

Or does anyone know of such a library available to users?

For example, I would need the lemmas:
- a well founded relation is irreflexive (obvious);
- the transitive closure of a well founded relation is well founded
(less obvious).

In addition, it might be interesting to relate PVS definition of well
founded to that of mathematicians, which is close to: a relation R in
type T is well founded if there is no infinitely decreasing sequence,
i.e., no f:[nat->T] such that
   (FORALL (n: nat): R(f(n+1),f(n))) .

Thank you for your help: it may save me some proofs!
Paul Y Gloess
   E.N.S.E.R.B.:   http://www.enserb.u-bordeaux.fr/~gloess
          LaBRI:   http://dept-info.labri.u-bordeaux.fr/~gloess