The Theory wf_recp
 Parents
 wf_relp
 Children
 ord
 Constants
 \$respects (('a → 'b) → 'a → 'b) → ('a → 'a → BOOL) → BOOL fixed_below (('a → 'b) → 'a → 'b) → ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL fixed_at (('a → 'b) → 'a → 'b) → ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL fix (('a → 'b) → 'a → 'b) → 'a → 'b relmap ('a → 'a → BOOL) → ('a → 'b) → 'a → 'a → 'b → BOOL
 Fixity
 Right Infix 240: respects
 Definitions
 respects ⊢ ∀ f r • f respects r ⇔ (∀ g h x • (∀ y• tc r y x ⇒ g y = h y) ⇒ f g x = f h x) fixed_below ⊢ ∀ f r g x • fixed_below f r g x ⇔ (∀ y• tc r y x ⇒ f g y = g y) fixed_at ⊢ ∀ f r g x • fixed_at f r g x ⇔ fixed_below f r g x ∧ f g x = g x fix ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ f (fix f) = fix f relmap ⊢ ∀ r f• relmap r f = (λ x y z• r y x ∧ z = f y)
 Theorems
 fixed_below_lemma1 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x g y • fixed_below f r g x ∧ tc r y x ⇒ fixed_below f r g y) fixed_at_lemma1 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x g • fixed_below f r g x ⇒ fixed_at f r (f g) x) fixed_at_lemma2 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x g • fixed_below f r g x ⇒ (∀ y• tc r y x ⇒ fixed_at f r g y)) fixed_at_lemma3 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x g • (∀ y• tc r y x ⇒ fixed_at f r g y) ⇒ fixed_below f r g x) fixed_below_lemma2 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x g h • fixed_below f r g x ∧ fixed_below f r h x ⇒ (∀ z• tc r z x ⇒ h z = g z)) fixed_at_lemma4 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ g x • fixed_at f r g x ⇒ (∀ y• tc r y x ⇒ fixed_at f r g y)) fixed_at_lemma5 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ g h x • fixed_at f r g x ∧ fixed_at f r h x ⇒ g x = h x) fixed_below_lemma3 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x • (∀ y• tc r y x ⇒ (∃ g• fixed_at f r g y)) ⇒ (∃ g• fixed_below f r g x)) fixed_below_lemma4 ⊢ ∀ r f • well_founded r ∧ f respects r ⇒ (∀ x• ∃ g• fixed_below f r g x) fixed_at_lemma6 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x• ∃ g• fixed_at f r g x) fixed_lemma1 ⊢ ∀ f r • well_founded r ∧ f respects r ⇒ (∀ x • fixed_at f r (λ x• (ε h• fixed_at f r h x) x) x) fixp_thm1 ⊢ ∀ f r• well_founded r ∧ f respects r ⇒ (∃ g• f g = g) relmap_respect_thm ⊢ ∀ r g• (λ f• g o relmap r f) respects r