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 UnaryFuncHom^Hom_struct_u : ι → ι → ι → ο
Param BinRelnHom^Hom_struct_r : ι → ι → ι → ο
Definition edc2c.. := λ x0 x1 x2 . and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param struct_c_u_r_r : ι → ο
Conjecture 947f4.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_initial_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture 0ac44.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 87b5c.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 6828b.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_coequalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 8aa32.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4
Param MetaCat_equalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture b9583.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4
Param MetaCat_pushout_buggy_constr_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 6a787.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_pullback_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 1fd6d.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_exp_constr_p^{product_exponent_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι) → ο
Conjecture 33b16.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . ∃ x8 x10 : ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6 x8 x10 x12
Param MetaCat_subobject_classifier_buggy_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture dc254.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 . ∃ x8 : ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaCat_nno_p^nno_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → ι → (ι → ι → ι → ι) → ο
Conjecture f08b8.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 x8 . ∃ x10 : ι → ι → ι → ι . MetaCat_nno_p struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Conjecture e6f58.. : ∃ x0 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x4 x6 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_c_u_r_r edc2c.. struct_id struct_comp x0 x2 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x4 x6