Theory companion

⊢ ∀s r b B.
    B_join (s,r) b B ⇔
    function (endo (s,r)) (endo (s,r)) B ∧ monotonic (endo_lift (s,r)) B ∧
    ∀g x.
      lub (s,r) {f x | endo (s,r) f ∧ lift_rel (s,r) (f ∘ b) (b ∘ g)}
        (B g x)

⊢ ∀s r b t.
    companion (s,r) b t ⇔
    function s s t ∧ ∀x. lub (s,r) {f x | compatible (s,r) b f} (t x)

⊢ ∀s r b f.
    compatible (s,r) b f ⇔
    function s s f ∧ monotonic (s,r) f ∧ lift_rel (s,r) (f ∘ b) (b ∘ f)

⊢ ∀s r f.
    endo (s,r) f ⇔
    monotonic (s,r) f ∧ ∀x. if s x then s (f x) else f x = @y. ¬s y

⊢ ∀s r. endo_lift (s,r) = (endo (s,r),lift_rel (s,r))

⊢ ∀fn b.
    higher_compat fn b ⇔
    (∀f. monotone f ⇒ monotone (fn f)) ∧ higher_monotone fn ∧
    ∀f X. monotone f ⇒ fn (set_B b f) X ⊆ set_B b (fn f) X

⊢ ∀fn.
    higher_monotone fn ⇔
    ∀f g. monotone f ∧ monotone g ∧ (∀X. f X ⊆ g X) ⇒ ∀X. fn f X ⊆ fn g X

⊢ ∀s r f g. lift_rel (s,r) f g ⇔ ∀x. s x ⇒ r (f x) (g x)

⊢ ∀b. set_B b = (λg X. BIGUNION {f X | monotone f ∧ ∀Y. f (b Y) ⊆ b (g Y)})

⊢ ∀b. set_T b =
      (λf X. BIGUNION {fn f X | fn | monotone (fn f) ∧ higher_compat fn b})

⊢ ∀b X. set_companion b X = BIGUNION {f X | set_compatible b f}

⊢ ∀b f. set_compatible b f ⇔ monotone f ∧ ∀X. f (b X) ⊆ b (f X)

⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) t ∧ companion (s,r) b t ∧
  B_join (s,r) b B ⇒
  po_gfp (endo_lift (s,r)) B t

⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) f ∧ B_join (s,r) b B ⇒
  lift_rel (s,r) (B f ∘ b) (b ∘ f)

⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ∧ endo (s,r) t ∧
  companion (s,r) b t ∧ companion (endo_lift (s,r)) B T' ∧
  bottom (endo_lift (s,r)) bot ∧ endo (s,r) f ⇒
  T' f ∘ T' f = T' f

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ bottom (s,r) bot ∧
  po_gfp (s,r) b gfix ∧ companion (s,r) b t ⇒
  t bot = gfix

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ companion (s,r) b t ∧
  po_gfp (s,r) b gfix ∧ s x ∧ r x ((b ∘ t) x) ⇒
  r x gfix

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ companion (s,r) b t ∧
  s x ⇒
  r x (t x)

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ companion (s,r) b t ∧
  s x ⇒
  t (t x) = t x

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ companion (s,r) b t ⇒
  monotonic (s,r) t

⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ∧ endo (s,r) f ⇒
  (lift_rel (s,r) f (B f) ⇔ lift_rel (s,r) (f ∘ b) (b ∘ f))

⊢ poset (s,r) ∧ compatible (s,r) b f ∧ companion (s,r) b t ⇒
  lift_rel (s,r) f t

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ companion (s,r) b t ⇒
  compatible (s,r) b t

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ compatible (s,r) b f ∧
  compatible (s,r) b g ⇒
  compatible (s,r) b (f ∘ g)

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧ po_gfp (s,r) b fp ⇒
  compatible (s,r) b (K fp)

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ⇒ compatible (s,r) b I

⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ⇒ compatible (s,r) b b

⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ⇒
  compatible (endo_lift (s,r)) B (λf. f ∘ f)

⊢ endo (s,r) f ∧ endo (s,r) g ⇒ endo (s,r) (f ∘ g)

⊢ endo (s,r) f ⇒ function s s f

⊢ endo (s,r) t ∧ s x ⇒ s (t x)

⊢ poset (s,r) ⇒ poset (endo_lift (s,r))

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ po_gfp (s,r) b gfix ∧
  companion (s,r) b t ∧ po_gfp (s,r) (b ∘ t) efix ⇒
  efix = gfix

⊢ poset (s,r) ∧ function s s g ∧ function s s f ∧ function s s f' ∧
  function s s g' ∧ monotonic (s,r) f ∧ monotonic (s,r) f' ∧
  lift_rel (s,r) f f' ∧ lift_rel (s,r) g g' ⇒
  lift_rel (s,r) (f ∘ g) (f' ∘ g')

⊢ poset (s,r) ∧ function s s f ∧ monotonic (s,r) f ∧
  lub (s,r) {x | r x (f x)} l ⇒
  po_gfp (s,r) f l

⊢ complete (s,r) ∧ complete (endo_lift (s,r)) ∧ poset (s,r) ∧
  endo (s,r) b ∧ companion (s,r) b t ∧ endo (s,r) t ∧ B_join (s,r) b B ∧
  companion (endo_lift (s,r)) B T' ∧ po_gfp (s,r) b gfix ∧ s x ∧ s y ∧
  lub (s,r) {x; y} xy ⇒
  r y (b (t xy)) ⇒
  r y (t x)

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ companion (s,r) b t ⇒
  s x ∧ s y ∧ r y x ⇒
  r y (t x)

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ bottom (s,r) bot ∧
  po_gfp (s,r) b gfix ∧ companion (s,r) b t ⇒
  r x (t bot) ⇒
  r x gfix

⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧ companion (s,r) b t ⇒
  function s s f ∧ (∀x. r (f x) (t x)) ⇒
  s x ∧ s y ∧ r y (f (t x)) ⇒
  r y (t x)

⊢ companion (𝕌(:α -> bool),$SUBSET) b (set_companion b)

⊢ monotone b ∧ X ⊆ (b ∘ set_companion b) X ⇒ X ⊆ gfp b

⊢ monotone b ⇒ set_compatible b (set_companion b)

⊢ set_compatible b f ⇒ compatible (𝕌(:α -> bool),$SUBSET) b f

⊢ monotone b ⇒
  set_compatible b f ∧ set_compatible b g ⇒
  set_compatible b (f ∘ g)

⊢ monotone b ∧ set_compatible b f ∧ Y ⊆ f X ⇒ Y ⊆ set_companion b X

⊢ monotone b ⇒ set_compatible b I

⊢ monotone b ⇒ set_compatible b b

⊢ monotone b ⇒ gfp b ⊆ set_companion b x

⊢ complete (endo_lift (𝕌(:α -> bool),$SUBSET))

⊢ monotone b ⇒ Y ⊆ b (set_companion b (X ∪ Y)) ⇒ Y ⊆ set_companion b X

⊢ monotone b ∧ Y ⊆ X ⇒ Y ⊆ set_companion b X

⊢ monotone b ∧ X ⊆ set_companion b ∅ ⇒ X ⊆ gfp b

⊢ monotone b ∧ (∀X. f X ⊆ set_companion b X) ∧ Y ⊆ f (set_companion b X) ⇒
  Y ⊆ set_companion b X

⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) t ∧ companion (s,r) b t ∧
  B_join (s,r) b B ∧ bottom (endo_lift (s,r)) bot ∧
  companion (endo_lift (s,r)) B T' ∧ endo (s,r) f ⇒
  lift_rel (s,r) t (T' f)