Proofgold Signed Transaction

Param lam_id^lam_id : ι → ι
Param ap^ap : ι → ι → ι
Definition struct_id^struct_id := λ x0 . lam_id (ap x0 0)
Param lam_comp^lam_comp : ι → ι → ι → ι
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param and^and : ο → ο → ο
Param PreContinuousHom^Hom_struct_c : ι → ι → ι → ο
Param PtdSetHom^Hom_struct_e : ι → ι → ι → ο
Definition 57c9e.. := λ x0 x1 x2 . and (PreContinuousHom x0 x1 x2) (PtdSetHom x0 x1 x2)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param struct_c_e : ι → ο
Conjecture 2346b.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_initial_p struct_c_e 57c9e.. struct_id struct_comp x0 x2
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture 25cb7.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p struct_c_e 57c9e.. struct_id struct_comp x0 x2
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 0447b.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture d51a4.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_coequalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture eb475.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4
Param MetaCat_equalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 30628.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4
Param MetaCat_pushout_buggy_constr_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture fa713.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_pullback_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture be05f.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_exp_constr_p^{product_exponent_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι) → ο
Conjecture adcbd.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . ∃ x8 x10 : ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6 x8 x10 x12
Param MetaCat_subobject_classifier_buggy_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture a531c.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 . ∃ x8 : ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaCat_nno_p^nno_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → ι → (ι → ι → ι → ι) → ο
Conjecture d25e4.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 x8 . ∃ x10 : ι → ι → ι → ι . MetaCat_nno_p struct_c_e 57c9e.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Conjecture 073d6.. : ∃ x0 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x4 x6 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_c_e 57c9e.. struct_id struct_comp x0 x2 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x4 x6