Entry	Value
Package Name	relation-well-founded-thm
Count	9
Theorems	WF_EQ : !r. WF r <=> (!p. (?x. p x) <=> (?x. p x /\ (!y. r y x ==> ~p y))) WF_IND : !r. WF r <=> (!p. (!x. (!y. r y x ==> p y) ==> p x) ==> (!x. p x)) WF_LEX : !r s. WF r /\ WF s ==> WF (\(x1,y1) (x2,y2). r x1 x2 \/ x1 = x2 /\ s y1 y2) WF_LEX_DEPENDENT : !r s. WF r /\ (!a. WF (s a)) ==> WF (\(x1,y1) (x2,y2). r x1 x2 \/ x1 = x2 /\ s x1 y1 y2) WF_MEASURE_GEN : !r m. WF r ==> WF (\x y. r (m x) (m y)) WF_POINTWISE : !r s. WF r /\ WF s ==> WF (\(x1,y1) (x2,y2). r x1 x2 /\ s y1 y2) wellfounded_emptyr : WF emptyr wellfounded_irreflexive : !r. WF r ==> irreflexive r wellfounded_subrelation : !r s. subrelation r s /\ WF s ==> WF r

Back to main package page