The Theory fixp
 Parents
 hol
 Constants
 monotonic ('a SET → 'b SET) → BOOL lfp ('a SET → 'a SET) → 'a SET gfp ('a SET → 'a SET) → 'a SET cc2monof ('a → 'b) × ('a → 'b SET) → 'b SET → 'b SET closure ('a → 'b) × ('a → 'b SET) → 'b SET IndPair (BOOL → 'a) → ('a LIST → ONE + 'b) × ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b IndInL (BOOL → 'a) → ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b IndInR (BOOL → 'a) → ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b IndSum (BOOL → 'a) → ('a LIST → ONE + 'b) + ('a LIST → ONE + 'b) → 'a LIST → ONE + 'b IndList (ℕ → 'a) → ('a LIST → ONE + 'b) LIST → 'a LIST → ONE + 'b
 Definitions
 monotonic ⊢ ∀ f• monotonic f ⇔ (∀ x y• x ⊆ y ⇒ f x ⊆ f y) lfp ⊢ ∀ f• lfp f = ⋂ {X|f X ⊆ X} gfp ⊢ ∀ f• gfp f = ⋃ {X|X ⊆ f X} cc2monof ⊢ ∀ tor tent • cc2monof (tor, tent) = (λ s • s ∪ {t|∃ u v• u = tent v ∧ u ⊆ s ∧ t = tor v}) closure ⊢ ∀ tor tent • closure (tor, tent) = lfp (cc2monof (tor, tent)) IndPair ⊢ ∀ i l r h t • IndPair i (l, r) [] = InL One ∧ IndPair i (l, r) (Cons h t) = (if h = i F then l t else if h = i T then r t else InL One) IndInL ⊢ ∀ i j h t • IndInL i j [] = InL One ∧ IndInL i j (Cons h t) = (if h = i F then j t else InL One) IndInR ⊢ ∀ i j h t • IndInR i j [] = InL One ∧ IndInR i j (Cons h t) = (if h = i T then j t else InL One) IndSum ⊢ ∀ i j h t • IndSum i j [] = InL One ∧ IndSum i j (Cons h t) = (if IsL j then if h = i F then OutL j t else InL One else if h = i T then OutR j t else InL One) IndList ⊢ ∀ i ha ta hb tb • IndList i [] tb = InL One ∧ IndList i (Cons ha ta) [] = InL One ∧ IndList i (Cons ha ta) (Cons hb tb) = (if ∃ j• hb = i j ∧ j < Length ta then IndList i ta (Cons hb tb) else if hb = i (Length ta) then ha tb else InL One)
 Theorems
 least_fixpoint_thm ⊢ ∀ h• monotonic h ⇒ h (lfp h) = lfp h lfp_min_thm ⊢ ∀ h• monotonic h ⇒ (∀ g• h g = g ⇒ lfp h ⊆ g) lfp_induction_thm ⊢ ∀ h• monotonic h ⇒ (∀ s• h s ⊆ s ⇒ lfp h ⊆ s) greatest_fixpoint_thm ⊢ ∀ h• monotonic h ⇒ h (gfp h) = gfp h gfp_max_thm ⊢ ∀ h• monotonic h ⇒ (∀ g• h g = g ⇒ g ⊆ gfp h) gfp_coinduction_thm ⊢ ∀ h• monotonic h ⇒ (∀ s• s ⊆ h s ⇒ s ⊆ gfp h) mono_cc2monof_thm ⊢ ∀ tor tent• monotonic (cc2monof (tor, tent)) closure_thm1 ⊢ ∀ tor tent s x y • tent x = s ∧ s ⊆ closure (tor, tent) ∧ y = tor x ⇒ y ∈ closure (tor, tent) closure_induction_thm ⊢ ∀ tor tent p • (∀ x• (∃ y• tor y = x ∧ tent y ⊆ p) ⇒ x ∈ p) ⇒ closure (tor, tent) ⊆ p