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 UnaryPredHom^Hom_struct_p : ι → ι → ι → ο
Param PtdSetHom^Hom_struct_e : ι → ι → ι → ο
Definition 3de88.. := λ x0 x1 x2 . and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param struct_c_u_p_e : ι → ο
Conjecture de30c.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_initial_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture ca9a9.. : ∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 46432.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 6a1dd.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_coequalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 84e44.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4
Param MetaCat_equalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 5ec2c.. : ∃ x0 x2 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4
Param MetaCat_pushout_buggy_constr_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 69bec.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_pullback_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture d2396.. : ∃ x0 x2 x4 : ι → ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6
Param MetaCat_exp_constr_p^{product_exponent_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι) → ο
Conjecture 364d8.. : ∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . ∃ x8 x10 : ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6 x8 x10 x12
Param MetaCat_subobject_classifier_buggy_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture afbe9.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 . ∃ x8 : ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaCat_nno_p^nno_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → ι → (ι → ι → ι → ι) → ο
Conjecture 38763.. : ∃ x0 . ∃ x2 : ι → ι . ∃ x4 x6 x8 . ∃ x10 : ι → ι → ι → ι . MetaCat_nno_p struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 x4 x6 x8 x10
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Conjecture eea2b.. : ∃ x0 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x4 x6 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_c_u_p_e 3de88.. struct_id struct_comp x0 x2 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x4 x6