$respects
fixed_below
→ ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL
fixed_at
→ ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL
fix
relmap
| 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 |
