Entry	Value
Package Name	relation-natural-thm
Count	18
Theorems	MEASURE_LE : !m a b. (!y. MEASURE m y a ==> MEASURE m y b) <=> m a <= m b WF_DCHAIN : !r. WF r <=> ~(?f. !n. r (f (SUC n)) (f n)) WF_EREC : !r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?!f. !x. f x = h f x)) WF_FINITE : !r. (!x. ~r x x) /\ (!x y z. r x y /\ r y z ==> r x z) /\ (!x. FINITE {y | r y x}) ==> WF r WF_MEASURE : !m. WF (MEASURE m) WF_REC : !r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?f. !x. f x = h f x)) WF_REC_INVARIANT : !r. WF r ==> (!h s. (!f g x. (!z. r z x ==> f z = g z /\ s z (f z)) ==> h f x = h g x /\ s x (h f x)) ==> (?f. !x. f x = h f x)) WF_REC_TAIL : !p g h. ?f. !x. f x = (if p x then f (g x) else h x) WF_REC_WF : !r. (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?f. !x. f x = h f x)) ==> WF r WF_UREC : !r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (!f g. (!x. f x = h f x) /\ (!x. g x = h g x) ==> f = g)) WF_UREC_WF : !r. (!h. (!f g x. (!z. r z x ==> (f z <=> g z)) ==> (h f x <=> h g x)) ==> (!f g. (!x. f x <=> h f x) /\ (!x. g x <=> h g x) ==> f = g)) ==> WF r WF_num : WF (<) irreflexive_successor : irreflexive successor subrelation_successor_lt : subrelation successor (<) transitive_closure_successor_lt : transitive_closure successor = (<) transitive_lt : transitive (<) transitive_successor_lt : !r. subrelation successor r /\ transitive r ==> subrelation (<) r wellfounded_successor : WF successor

Back to main package page