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)
fill→ ('a → 'a → BOOL)
fill→ ('a → 'b)
fill→ 'a
fill→ BOOL
fixed_at
(('a → 'b) → 'a → 'b)
fill→ ('a → 'a → BOOL)
fill→ ('a → 'b)
fill→ 'a
fill→ 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
fill• f respects r
fill⇔ (∀ g h x
fill• (∀ y• tc r y x ⇒ g y = h y) ⇒ f g x = f h x)
fixed_below
⊢ ∀ f r g x
fill• fixed_below f r g x ⇔ (∀ y• tc r y x ⇒ f g y = g y)
fixed_at
⊢ ∀ f r g x
fill• fixed_at f r g x
fill⇔ fixed_below f r g x ∧ f g x = g x
fix
⊢ ∀ f r
fill• 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
fill• well_founded r ∧ f respects r
fill⇒ (∀ x g y
fill• fixed_below f r g x ∧ tc r y x
fill⇒ fixed_below f r g y)
fixed_at_lemma1
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x g
fill• fixed_below f r g x ⇒ fixed_at f r (f g) x)
fixed_at_lemma2
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x g
fill• fixed_below f r g x
fill⇒ (∀ y• tc r y x ⇒ fixed_at f r g y))
fixed_at_lemma3
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x g
fill• (∀ y• tc r y x ⇒ fixed_at f r g y)
fill⇒ fixed_below f r g x)
fixed_below_lemma2
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x g h
fill• fixed_below f r g x ∧ fixed_below f r h x
fill⇒ (∀ z• tc r z x ⇒ h z = g z))
fixed_at_lemma4
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ g x
fill• fixed_at f r g x
fill⇒ (∀ y• tc r y x ⇒ fixed_at f r g y))
fixed_at_lemma5
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ g h x
fill• fixed_at f r g x ∧ fixed_at f r h x
fill⇒ g x = h x)
fixed_below_lemma3
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x
fill• (∀ y• tc r y x ⇒ (∃ g• fixed_at f r g y))
fill⇒ (∃ g• fixed_below f r g x))
fixed_below_lemma4
⊢ ∀ r f
fill• well_founded r ∧ f respects r
fill⇒ (∀ x• ∃ g• fixed_below f r g x)
fixed_at_lemma6
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x• ∃ g• fixed_at f r g x)
fixed_lemma1
⊢ ∀ f r
fill• well_founded r ∧ f respects r
fill⇒ (∀ x
fill• fixed_at
fillf
fillr
fill(λ x• (ε h• fixed_at f r h x) x)
fillx)
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

up quick index

privacy policy

Created:

V