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 PtdSetHom^Hom_struct_e : ι → ι → ι → ο
Definition a80bc.. := λ x0 x1 x2 . and (PtdSetHom x0 x1 x2) (PtdSetHom x0 x1 x2)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param struct_e_e : ι → ο
Conjecture 5afbb.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_initial_p struct_e_e a80bc.. struct_id struct_comp x0 x2
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture f08a1.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p struct_e_e a80bc.. struct_id struct_comp x0 x2
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture d265a.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture ac9bb.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_coequalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture bcb44.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4
Param MetaCat_equalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture a3962.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4
Param MetaCat_pushout_buggy_constr_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 861a7.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_pullback_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture a0aa6.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_exp_constr_p^{product_exponent_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι) → ο
Conjecture ae3a5.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . ∃ x8 x10 : ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6 x8 x10 x12
Param MetaCat_subobject_classifier_buggy_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture fdc5f.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 . ∃ x8 : ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaCat_nno_p^nno_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → ι → (ι → ι → ι → ι) → ο
Conjecture 08690.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 x8 . ∃ x10 : ι → ι → ι → ι . MetaCat_nno_p struct_e_e a80bc.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Conjecture afe17.. : ∃ x0 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x4 x6 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_e_e a80bc.. struct_id struct_comp x0 x2 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x4 x6