The Theory wf_rel
Parents
bin_rel
Constants
wf
('a ↔ 'a) ℘
twf
('a ↔ 'a) ℘
Definitions
wf
⊢ ∀ r
fill• r ∈ wf
fill⇔ (∀ s
fill• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s)
fill⇒ (∀ 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
fill• r = s
fill⇔ Dom r = Dom s
fill∧ (∀ x
fill• x ∈ Dom r ∩ Dom s
fill⇒ (∀ y• (x, y) ∈ r ⇔ (x, y) ∈ s))
tran_tc_thm
⊢ ∀ r• r + ∈ Transitive
tran_tc_thm2
⊢ ∀ r x y z
fill• (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
fill• (x, y) ∈ r + ∧ ¬ (x, y) ∈ r
fill⇒ (∃ z• (x, z) ∈ r + ∧ (z, y) ∈ r)
tcwf_lemma1
⊢ ∀ s r
fill• r ∈ wf
fill⇒ (∀ x
fill• (∀ y
fill• (y, x) ∈ r +
fill⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s)
fill⇒ y ∈ s)
fill⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s))
tcwf_lemma2
⊢ ∀ r
fill• r ∈ wf
fill⇒ (∀ s
fill• (∀ t• (∀ u• (u, t) ∈ r + ⇒ u ∈ s) ⇒ t ∈ s)
fill⇒ (∀ e• e ∈ s))
tc_wf_twf_thm
⊢ ∀ r• r ∈ wf ⇒ r + ∈ twf

up quick index

privacy policy

Created:

V