Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr3v3../a3e3c..
PUKTb../ad8fd..
vout
Pr3v3../adf1f.. 80.42 bars
TMae7../ca7af.. ownership of 0a2f5.. as prop with payaddr PrCx1.. rightscost 0.00 controlledby PrCx1.. upto 0
TMZKK../770c2.. ownership of e1ddd.. as prop with payaddr PrCx1.. rightscost 0.00 controlledby PrCx1.. upto 0
TMbE7../45a35.. ownership of 6f034.. as prop with payaddr PrCx1.. rightscost 0.00 controlledby PrCx1.. upto 0
TMQ2t../46a2d.. ownership of 8f936.. as prop with payaddr PrCx1.. rightscost 0.00 controlledby PrCx1.. upto 0
PUcLi../12939.. doc published by PrCx1..
Param lam_idlam_id : ιι
Param apap : ιιι
Definition struct_idstruct_id := λ x0 . lam_id (ap x0 0)
Param lam_complam_comp : ιιιι
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param struct_b_b_e_estruct_b_b_e_e : ιο
Param unpack_b_b_e_e_ounpack_b_b_e_e_o : ι(ι(ιιι) → (ιιι) → ιιο) → ο
Param explicit_Fieldexplicit_Field : ιιι(ιιι) → (ιιι) → ο
Definition FieldField := λ x0 . and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3))
Param Hom_b_b_e_eHom_struct_b_b_e_e : ιιιο
Known 936d9..MetaCat_struct_b_b_e_e_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_b_b_e_e x1)MetaCat x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 6f034..MetaCat_struct_b_b_e_e_field : MetaCat Field Hom_b_b_e_e struct_id struct_comp (proof)
Param MetaFunctorMetaFunctor : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param TrueTrue : ο
Param HomSetSetHom : ιιιο
Known 72690..MetaCat_struct_b_b_e_e_Forgetful_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_b_b_e_e x1)MetaFunctor x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3)
Theorem 0a2f5..MetaCat_struct_b_b_e_e_field_Forgetful : MetaFunctor Field Hom_b_b_e_e struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param MetaCat_initial_pinitial_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture 088b7..MetaCat_struct_b_b_e_e_field_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p Field Hom_b_b_e_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_terminal_pterminal_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture c07a0..MetaCat_struct_b_b_e_e_field_terminal : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Field Hom_b_b_e_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_coproduct_constr_pcoproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture ad01d..MetaCat_struct_b_b_e_e_field_coproduct_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 80dff..MetaCat_struct_b_b_e_e_field_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_coequalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture b352a.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_equalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture 6d351.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_pushout_buggy_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 7f107.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_pullback_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 41de2.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_exp_constr_pproduct_exponent_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιιιι) → ο
Conjecture 65da8..MetaCat_struct_b_b_e_e_field_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7 x9 x11 x13x12)x12)x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_subobject_classifier_buggy_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ιι(ιιιι) → (ιιιιιιι) → ο
Conjecture aeae1.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_nno_pnno_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ιιι(ιιιι) → ο
Conjecture 38f47..MetaCat_struct_b_b_e_e_field_nno : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p Field Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaAdjunction_strictMetaAdjunction_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Conjecture 1ef6e..MetaCat_struct_b_b_e_e_field_left_adjoint_forgetful : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) Field Hom_b_b_e_e struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0