[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
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