Structure coalgAxiomsTheory

signature coalgAxiomsTheory =
sig
  type thm = Thm.thm
  
  (*  Axioms  *)
    val mapID : thm
    val mapO : thm
    val map_CONG : thm
    val relO : thm
    val set_map : thm
  
  (*  Definitions  *)
    val Fset_def : thm
    val bisim_def : thm
    val bisimilar_def : thm
    val bquot_def : thm
    val gbisim_def : thm
    val genS_def : thm
    val hom_def : thm
    val iso_def : thm
    val relF_def : thm
    val simple_def : thm
    val subsystem_def : thm
    val system_def : thm
  
  (*  Theorems  *)
    val BIJ_homs_iso : thm
    val Fpushout_def : thm
    val Fpushout_ind : thm
    val INJ_homs_mono : thm
    val SURJ_homs_epi : thm
    val UNIV_system : thm
    val bisim_RUNION : thm
    val bisim_gbisim : thm
    val bisim_system : thm
    val bisimilar_equivalence : thm
    val bisimulations_compose : thm
    val bounded_def : thm
    val bounded_ind : thm
    val bquot_coequalizer : thm
    val bquot_correct : thm
    val coequalizer_def : thm
    val coequalizer_ind : thm
    val coequalizer_thm : thm
    val epi_Fpushout : thm
    val epi_def : thm
    val epi_ind : thm
    val gbisim_equivalence : thm
    val genS_correct : thm
    val hom_ID : thm
    val hom_implies_restr : thm
    val hom_shom : thm
    val homs_compose : thm
    val iso_SYM : thm
    val iso_inj_hom : thm
    val lemma2_4_1 : thm
    val lemma2_4_2 : thm
    val lemma5_3 : thm
    val mapO' : thm
    val map_preserves_INJ : thm
    val map_preserves_funs : thm
    val prop5_1 : thm
    val prop5_7 : thm
    val prop5_8 : thm
    val prop5_9_1 : thm
    val prop5_9_2 : thm
    val prop6_1 : thm
    val prop6_2 : thm
    val relEQ : thm
    val relF_inv : thm
    val relO_EQ : thm
    val rel_monotone : thm
    val sbisimulation_projns_homo : thm
    val set_map' : thm
    val simple_eq3 : thm
    val simple_imp4 : thm
    val subsystem_ALT : thm
    val subsystem_INTER : thm
    val subsystem_INTER2 : thm
    val subsystem_UNION : thm
    val subsystem_refl : thm
    val subsystem_system : thm
    val system_members : thm
    val thm2_5 : thm
    val thm5_2 : thm
    val thm5_4 : thm
    val thm5_5 : thm
    val thm6_3_1 : thm
    val thm6_3_2 : thm
    val thm7_1 : thm
    val thm7_2 : thm
    val thm7_3 : thm
  
  val coalgAxioms_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [simpleSetCat] Parent theory of "coalgAxioms"
   
   [mapID]  Axiom
      
      [oracles: ] [axioms: mapID] [] ⊢ mapF (λx. x) = (λa. a)
   
   [mapO]  Axiom
      
      [oracles: ] [axioms: mapO] [] ⊢ mapF f ∘ mapF g = mapF (f ∘ g)
   
   [map_CONG]  Axiom
      
      [oracles: ] [axioms: map_CONG] []
      ⊢ ∀f g y. (∀x. x ∈ setF y ⇒ f x = g x) ⇒ mapF f y = mapF g y
   
   [relO]  Axiom
      
      [oracles: ] [axioms: relO] [] ⊢ relF R ∘ᵣ relF S ⊆ᵣ relF (R ∘ᵣ S)
   
   [set_map]  Axiom
      
      [oracles: ] [axioms: set_map] [] ⊢ setF ∘ mapF f = IMAGE f ∘ setF
   
   [Fset_def]  Definition
      
      ⊢ ∀A. Fset A = {af | setF af ⊆ A}
   
   [bisim_def]  Definition
      
      ⊢ ∀R A af B bf.
          bisim R (A,af) (B,bf) ⇔
          system (A,af) ∧ system (B,bf) ∧
          ∀a b. R a b ⇒ a ∈ A ∧ b ∈ B ∧ relF R (af a) (bf b)
   
   [bisimilar_def]  Definition
      
      ⊢ ∀As Bs. bisimilar As Bs ⇔ ∃R. bisim R As Bs
   
   [bquot_def]  Definition
      
      ⊢ ∀A af R.
          bquot (A,af) R =
          (partition R A,
           (λap. mapF (eps R A) (af (CHOICE ap)))⟨partition R A⟩)
   
   [gbisim_def]  Definition
      
      ⊢ ∀A af x y. gbisim (A,af) x y ⇔ ∃R. bisim R (A,af) (A,af) ∧ R x y
   
   [genS_def]  Definition
      
      ⊢ ∀As X. genS As X = BIGINTER {V | subsystem V As ∧ X ⊆ V}
   
   [hom_def]  Definition
      
      ⊢ ∀h A af B bf.
          hom h (A,af) (B,bf) ⇔
          system (A,af) ∧ system (B,bf) ∧
          (∀a. a ∈ A ⇒ h a ∈ B ∧ bf (h a) = mapF h (af a)) ∧
          ∀a. a ∉ A ⇒ h a = ARB
   
   [iso_def]  Definition
      
      ⊢ ∀A af B bf.
          iso (A,af) (B,bf) ⇔
          ∃f g.
            hom f (A,af) (B,bf) ∧ hom g (B,bf) (A,af) ∧
            (∀a. a ∈ A ⇒ g (f a) = a) ∧ ∀b. b ∈ B ⇒ f (g b) = b
   
   [relF_def]  Definition
      
      ⊢ ∀R x y.
          relF R x y ⇔ ∃z. setF z ⊆ Rᴾ ∧ mapF FST z = x ∧ mapF SND z = y
   
   [simple_def]  Definition
      
      ⊢ ∀A. simple A ⇔ ∀R. bisim R A A ⇒ ∀x y. R x y ⇒ x = y
   
   [subsystem_def]  Definition
      
      ⊢ ∀V A af.
          subsystem V (A,af) ⇔
          system (A,af) ∧ V ⊆ A ∧ ∃vf. hom (λx. x)⟨V⟩ (V,vf) (A,af)
   
   [system_def]  Definition
      
      ⊢ ∀A af.
          system (A,af) ⇔
          (∀a. a ∈ A ⇒ af a ∈ Fset A) ∧ ∀a. a ∉ A ⇒ af a = ARB
   
   [BIJ_homs_iso]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, mapID, map_CONG] []
      ⊢ hom f (A,af) (B,bf) ∧ BIJ f A B ⇒ iso (A,af) (B,bf)
   
   [Fpushout_def]  Theorem
      
      ⊢ Fpushout (A,af) (B,bf) (C',cf) f g ((P,pf),i1,i2) (:δ) ⇔
        hom f (A,af) (B,bf) ∧ hom g (A,af) (C',cf) ∧ hom i1 (B,bf) (P,pf) ∧
        hom i2 (C',cf) (P,pf) ∧ (i1 ∘ f)⟨A⟩ = (i2 ∘ g)⟨A⟩ ∧
        ∀Q qf j1 j2.
          hom j1 (B,bf) (Q,qf) ∧ hom j2 (C',cf) (Q,qf) ∧
          (j1 ∘ f)⟨A⟩ = (j2 ∘ g)⟨A⟩ ⇒
          ∃!u. hom u (P,pf) (Q,qf) ∧ (u ∘ i1)⟨B⟩ = j1 ∧ (u ∘ i2)⟨C'⟩ = j2
   
   [Fpushout_ind]  Theorem
      
      ⊢ ∀P'.
          (∀A af B bf C cf f g P pf i1 i2.
             P' (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:δ)) ⇒
          ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12.
            P' (v,v1) (v2,v3) (v4,v5) v6 v7 ((v8,v9),v10,v11) v12
   
   [INJ_homs_mono]  Theorem
      
      ⊢ hom f (A,af) (B,bf) ∧ INJ f A B ⇒
        ∀C cf g h.
          hom g (C,cf) (A,af) ∧ hom h (C,cf) (A,af) ∧ f ∘ g = f ∘ h ⇒ g = h
   
   [SURJ_homs_epi]  Theorem
      
      ⊢ hom f (A,af) (B,bf) ∧ SURJ f A B ⇒ epi f (A,af) (B,bf) (:γ)
   
   [UNIV_system]  Theorem
      
      ⊢ system (𝕌(:α),af)
   
   [bisim_RUNION]  Theorem
      
      ⊢ bisim R1 As Bs ∧ bisim R2 As Bs ⇒ bisim (R1 ∪ᵣ R2) As Bs
   
   [bisim_gbisim]  Theorem
      
      ⊢ system (A,af) ⇒ bisim (gbisim (A,af)) (A,af) (A,af)
   
   [bisim_system]  Theorem
      
      ⊢ bisim R As Bs ⇒ system As ∧ system Bs
   
   [bisimilar_equivalence]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
      ⊢ bisimilar equiv_on system
   
   [bisimulations_compose]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
      ⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒
        bisim (Q ∘ᵣ R) (A,af) (C,cf)
   
   [bounded_def]  Theorem
      
      ⊢ bounded (:α) (:β) ⇔
        ∀a A af. system (A,af) ∧ a ∈ A ⇒ ∃f V. INJ f (genS (A,af) {a}) V
   
   [bounded_ind]  Theorem
      
      ⊢ ∀P. P (:α) (:β) ⇒ ∀v v1. P v v1
   
   [bquot_coequalizer]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
      ⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
        ∃Rf.
          coequalizer (Rᴾ,Rf) (A,af) FST⟨Rᴾ⟩ SND⟨Rᴾ⟩
            (bquot (A,af) R,eps R A) (:δ)
   
   [bquot_correct]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapO, map_CONG] []
      ⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
        system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)
   
   [coequalizer_def]  Theorem
      
      ⊢ coequalizer (A,af) (B,bf) f1 f2 ((C',cf),g) (:δ) ⇔
        hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧
        hom g (B,bf) (C',cf) ∧ (g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩ ∧
        ∀h D df.
          hom h (B,bf) (D,df) ∧ (h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩ ⇒
          ∃!u. hom u (C',cf) (D,df) ∧ h = (u ∘ g)⟨B⟩
   
   [coequalizer_ind]  Theorem
      
      ⊢ ∀P. (∀A af B bf f1 f2 C cf g. P (A,af) (B,bf) f1 f2 ((C,cf),g) (:δ)) ⇒
            ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9.
              P (v,v1) (v2,v3) v4 v5 ((v6,v7),v8) v9
   
   [coequalizer_thm]  Theorem
      
      ⊢ coequalizer (A,af) (B,bf) f1 f2 (Cs,g) (:δ) ⇔
        hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧ hom g (B,bf) Cs ∧
        (g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩ ∧
        ∀h D df.
          hom h (B,bf) (D,df) ∧ (h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩ ⇒
          ∃!u. hom u Cs (D,df) ∧ h = (u ∘ g)⟨B⟩
   
   [epi_Fpushout]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, map_CONG] []
      ⊢ epi f (A,af) (B,bf) (:γ) ⇔
        Fpushout (A,af) (B,bf) (B,bf) f f ((B,bf),(λx. x)⟨B⟩,(λx. x)⟨B⟩)
          (:γ)
   
   [epi_def]  Theorem
      
      ⊢ epi f (A,af) (B,bf) (:γ) ⇔
        hom f (A,af) (B,bf) ∧
        ∀C cf g h.
          hom g (B,bf) (C,cf) ∧ hom h (B,bf) (C,cf) ∧
          (g ∘ f)⟨A⟩ = (h ∘ f)⟨A⟩ ⇒
          g = h
   
   [epi_ind]  Theorem
      
      ⊢ ∀P. (∀f A af B bf. P f (A,af) (B,bf) (:γ)) ⇒
            ∀v v1 v2 v3 v4 v5. P v (v1,v2) (v3,v4) v5
   
   [gbisim_equivalence]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
      ⊢ system (A,af) ⇒ gbisim (A,af) equiv_on A
   
   [genS_correct]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapO, mapID, map_CONG] []
      ⊢ system (A,af) ∧ X ⊆ A ⇒ subsystem (genS (A,af) X) (A,af)
   
   [hom_ID]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, map_CONG] []
      ⊢ system (A,af) ⇒ hom (λx. x)⟨A⟩ (A,af) (A,af)
   
   [hom_implies_restr]  Theorem
      
      ⊢ hom f (A,af) Bs ⇒ f⟨A⟩ = f
   
   [hom_shom]  Theorem
      
      ⊢ hom f (A,af) (B,bf) ⇒ shom f A B
   
   [homs_compose]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG] []
      ⊢ hom f As Bs ∧ hom g Bs Cs ⇒ hom (g ∘ f)⟨FST As⟩ As Cs
   
   [iso_SYM]  Theorem
      
      ⊢ iso As Bs ⇔ iso Bs As
   
   [iso_inj_hom]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG] []
      ⊢ iso (A,af) (B,bf) ∧ hom h (A,af) (C,cf) ∧ INJ h A C ⇒
        ∃j. hom j (B,bf) (C,cf) ∧ INJ j B C
   
   [lemma2_4_1]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO] []
      ⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom g (A,af) (B,bf) ∧ SURJ g A B ∧
        (∀b. b ∉ B ⇒ h b = ARB) ⇒
        hom h (B,bf) (C,cf)
   
   [lemma2_4_2]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, map_CONG, mapID, mapO] []
      ⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom h (B,bf) (C,cf) ∧
        (∀a. a ∈ A ⇒ g a ∈ B) ∧ (∀a. a ∉ A ⇒ g a = ARB) ∧ INJ h B C ⇒
        hom g (A,af) (B,bf)
   
   [lemma5_3]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapO] []
      ⊢ hom f (A,af) (B,bf) ∧ hom g (A,af) (C,cf) ⇒
        bisim (span A f g) (B,bf) (C,cf)
   
   [mapO']  Theorem
      
      [oracles: DISK_THM] [axioms: mapO] []
      ⊢ ∀x. mapF f (mapF g x) = mapF (f ∘ g) x
   
   [map_preserves_INJ]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, map_CONG, mapID, mapO] []
      ⊢ INJ f A B ⇒ INJ (mapF f) (Fset A) (Fset B)
   
   [map_preserves_funs]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map] []
      ⊢ (∀a. a ∈ A ⇒ f a ∈ B) ⇒ ∀af. af ∈ Fset A ⇒ mapF f af ∈ Fset B
   
   [prop5_1]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, set_map, mapID, map_CONG] []
      ⊢ system (A,af) ⇒ bisim (Δ A) (A,af) (A,af)
   
   [prop5_7]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, set_map, mapID, mapO, map_CONG] []
      ⊢ hom f (A,af) (B,bf) ⇒
        bisim (kernel A f) (A,af) (A,af) ∧ kernel A f equiv_on A
   
   [prop5_8]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapO, map_CONG] []
      ⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
        system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)
   
   [prop5_9_1]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
      ⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ⇒
        bisim (RIMAGE f A R) (B,bf) (B,bf)
   
   [prop5_9_2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
      ⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim Q (B,bf) (B,bf) ⇒
        bisim (RINV_IMAGE f A Q) (A,af) (A,af)
   
   [prop6_1]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, map_CONG] []
      ⊢ V ⊆ A ∧ hom (λx. x)⟨V⟩ (V,kf) (A,af) ∧ hom (λx. x)⟨V⟩ (V,lf) (A,af) ⇒
        kf = lf
   
   [prop6_2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ system (A,af) ⇒
        (subsystem V (A,af) ⇔ V ⊆ A ∧ bisim (Δ V) (A,af) (A,af))
   
   [relEQ]  Theorem
      
      [oracles: DISK_THM] [axioms: map_CONG, set_map, mapO, mapID] []
      ⊢ relF $= = $=
   
   [relF_inv]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
      ⊢ relF Rᵀ x y ⇔ relF R y x
   
   [relO_EQ]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
      ⊢ relF R ∘ᵣ relF S = relF (R ∘ᵣ S)
   
   [rel_monotone]  Theorem
      
      ⊢ (∀a b. R a b ⇒ S a b) ⇒ ∀A B. relF R A B ⇒ relF S A B
   
   [sbisimulation_projns_homo]  Theorem
      
      [oracles: DISK_THM] [axioms: map_CONG] []
      ⊢ bisim R (A,af) (B,bf) ⇔
        ∃Rf. hom FST⟨Rᴾ⟩ (Rᴾ,Rf) (A,af) ∧ hom SND⟨Rᴾ⟩ (Rᴾ,Rf) (B,bf)
   
   [set_map']  Theorem
      
      [oracles: DISK_THM] [axioms: set_map] []
      ⊢ ∀x x'. x' ∈ setF (mapF f x) ⇔ ∃x''. x' = f x'' ∧ x'' ∈ setF x
   
   [simple_eq3]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
      ⊢ simple As ⇔ ∀R. bisim R As As ∧ R equiv_on FST As ⇒ R = Δ (FST As)
   
   [simple_imp4]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapO] []
      ⊢ simple As ⇒ ∀Bs f g. hom f Bs As ∧ hom g Bs As ⇒ f = g
   
   [subsystem_ALT]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ subsystem V (A,af) ⇔
        V ⊆ A ∧ system (A,af) ∧ hom (λx. x)⟨V⟩ (V,af⟨V⟩) (A,af)
   
   [subsystem_INTER]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ∧ VS ≠ ∅ ⇒
        subsystem (BIGINTER VS) (A,af)
   
   [subsystem_INTER2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ system (A,af) ∧ subsystem V1 (A,af) ∧ subsystem V2 (A,af) ⇒
        subsystem (V1 ∩ V2) (A,af)
   
   [subsystem_UNION]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ⇒
        subsystem (BIGUNION VS) (A,af)
   
   [subsystem_refl]  Theorem
      
      [oracles: DISK_THM] [axioms: mapID, map_CONG] []
      ⊢ system (A,af) ⇒ subsystem A (A,af)
   
   [subsystem_system]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ subsystem V (A,af) ⇒ system (V,af⟨V⟩)
   
   [system_members]  Theorem
      
      ⊢ system (A,af) ⇒ ∀a b. a ∈ A ∧ b ∈ setF (af a) ⇒ b ∈ A
   
   [thm2_5]  Theorem
      
      [oracles: DISK_THM] [axioms: set_map, mapID, mapO, map_CONG] []
      ⊢ hom h (A,af) (B,bf) ⇔
        (∀a. a ∈ A ⇒ h a ∈ B) ∧ (∀a. a ∉ A ⇒ h a = ARB) ∧
        bisim (Gr h A) (A,af) (B,bf)
   
   [thm5_2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
      ⊢ bisim Rᵀ Bs As ⇔ bisim R As Bs
   
   [thm5_4]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
      ⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒
        bisim (Q ∘ᵣ R) (A,af) (C,cf)
   
   [thm5_5]  Theorem
      
      ⊢ (∀R. R ∈ Rs ⇒ bisim R As Bs) ∧ system As ∧ system Bs ⇒
        bisim (λa b. ∃R. R ∈ Rs ∧ R a b) As Bs
   
   [thm6_3_1]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, map_CONG, mapID, set_map] []
      ⊢ hom f (A,af) (B,bf) ∧ subsystem V (A,af) ⇒
        subsystem (IMAGE f V) (B,bf)
   
   [thm6_3_2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
      ⊢ hom f (A,af) (B,bf) ∧ subsystem W (B,bf) ⇒
        subsystem (PREIMAGE f W ∩ A) (A,af)
   
   [thm7_1]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, map_CONG, mapID, set_map] []
      ⊢ hom f (A,af) (B,bf) ⇒
        hom f (A,af) (IMAGE f A,bf⟨IMAGE f A⟩) ∧
        (∀g h C cf.
           hom g (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧
           hom h (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧ (h ∘ f)⟨A⟩ = (g ∘ f)⟨A⟩ ⇒
           h = g) ∧
        hom (eps (kernel A f) A) (A,af) (bquot (A,af) (kernel A f)) ∧
        hom (λx. x)⟨IMAGE f A⟩ (IMAGE f A,bf⟨IMAGE f A⟩) (B,bf) ∧
        iso (IMAGE f A,bf⟨IMAGE f A⟩) (bquot (A,af) (kernel A f)) ∧
        ∃mu.
          hom mu (bquot (A,af) (kernel A f)) (B,bf) ∧
          INJ mu (FST (bquot (A,af) (kernel A f))) B
   
   [thm7_2]  Theorem
      
      [oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
      ⊢ hom f (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ∧ R ⊆ᵣ kernel A f ∧
        R equiv_on A ⇒
        ∃!fbar. hom fbar (bquot (A,af) R) (B,bf) ∧ f = (fbar ∘ eps R A)⟨A⟩
   
   [thm7_3]  Theorem
      
      [oracles: DISK_THM] [axioms: relO, mapO, mapID, set_map, map_CONG] []
      ⊢ system (A,af) ∧ subsystem B (A,af) ∧ bisim R (A,af) (A,af) ∧
        R equiv_on A ∧ Abbrev (TR = {a | a ∈ A ∧ ∃b. b ∈ B ∧ R a b}) ⇒
        subsystem TR (A,af) ∧
        (let
           Q = CURRY (Rᴾ ∩ (B × B))
         in
           bisim Q (B,af⟨B⟩) (B,af⟨B⟩) ∧ Q equiv_on B ∧
           iso (bquot (B,af⟨B⟩) Q) (bquot (TR,af⟨TR⟩) R))
   
   
*)
end

HOL 4, Kananaskis-14