[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
well foundedness properties
Hi!
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