The Theory wf_rel

Parents

bin_rel

Constants

wf	('a 'a) SET SET
twf	('a 'a) SET SET

Definitions

wf	r r wf ( s ( x ( y (y, x) r y s) x s) ( x x s))
twf	r r twf r wf r Transitive

Theorems

Dom_rest_thm	f s Dom (s f) = s Dom f
rel_ext_Dom_thm	r s r = s Dom r = Dom s ( x x Dom r Dom s ( y (x, y) r (x, y) s))
tran_tc_thm	r r ⁺ Transitive
tran_tc_thm2	r x y z (x, y) r ⁺ (y, z) r ⁺ (x, z) r ⁺
_tc_thm	r r r ⁺
_tc_thm	r x y (x, y) r (x, y) r ⁺
tc_decomp_thm	r x y (x, y) r ⁺ (x, y) r ( z (x, z) r ⁺ (z, y) r)
tcwf_lemma1	s r r wf ( x ( y (y, x) r ⁺ ( z (z, y) r ⁺ z s) y s) ( y (y, x) r ⁺ y s))
tcwf_lemma2	r r wf ( s ( t ( u (u, t) r ⁺ u s) t s) ( e e s))
tc_wf_twf_thm	r r wf r ⁺ twf

V