Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEMz../2c6c8..
PUShf../d8dbb..
vout
PrEMz../e6605.. 99.97 bars
TMShM../3a53f.. negprop ownership controlledby PrKYB.. upto 0
TMYGx../9b7ba.. negprop ownership controlledby PrKYB.. upto 0
TMVtN../2de69.. negprop ownership controlledby PrKYB.. upto 0
TMMJQ../cbbf6.. negprop ownership controlledby PrKYB.. upto 0
TMFcU../0a24e.. ownership of 62ee6.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMd4W../8af30.. ownership of cbb88.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMNtM../cacb8.. ownership of e5932.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMMkw../8ced4.. ownership of 53e90.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMXV1../a93d8.. ownership of e6a94.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMdum../65355.. ownership of 40480.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMWcs../828ae.. ownership of 87240.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMFV6../922a9.. ownership of 4b5c9.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMdmF../3e180.. ownership of 27155.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
TMMVt../f7a86.. ownership of 57c1a.. as prop with payaddr PrKYB.. rightscost 0.00 controlledby PrKYB.. upto 0
PUURq../2e7b2.. doc published by PrKYB..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 27155.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι → ι . (∀ x3 . x3x0∀ x4 . x4x0x1 x3 x4 = x2 x3 x4)and (∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x2 (x2 x4 x5) x6 = x2 x4 (x2 x5 x6)) (∀ x4 : ο . (∀ x5 . and (x5x0) (∀ x6 . x6x0and (x2 x6 x5 = x6) (x2 x5 x6 = x6))x4)x4) = and (∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 (x1 x4 x5) x6 = x1 x4 (x1 x5 x6)) (∀ x4 : ο . (∀ x5 . and (x5x0) (∀ x6 . x6x0and (x1 x6 x5 = x6) (x1 x5 x6 = x6))x4)x4) (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition MetaCat_initial_pinitial_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6and (x1 x4 x6 (x5 x6)) (∀ x7 . x1 x4 x6 x7x7 = x5 x6))
Param pack_bpack_b : ιCT2 ι
Definition struct_bstruct_b := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)x1 (pack_b x2 x3))x1 x0
Param unpack_b_ounpack_b_o : ι(ι(ιιι) → ο) → ο
Definition Monoidstruct_b_monoid := λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (∀ x3 . x3x1∀ x4 . x4x1∀ x5 . x5x1x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)) (∀ x3 : ο . (∀ x4 . and (x4x1) (∀ x5 . x5x1and (x2 x5 x4 = x5) (x2 x4 x5 = x5))x3)x3)))
Param MagmaHomHom_struct_b : ιιιο
Param struct_idstruct_id : ιι
Param lamSigma : ι(ιι) → ι
Param apap : ιιι
Definition lam_complam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Known unpack_b_o_equnpack_b_o_eq : ∀ x0 : ι → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . x4x1∀ x5 . x5x1x2 x4 x5 = x3 x4 x5)x0 x1 x3 = x0 x1 x2)unpack_b_o (pack_b x1 x2) x0 = x0 x1 x2
Param ordsuccordsucc : ιι
Param SNoSNo : ιο
Param mul_SNomul_SNo : ιιι
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 2cd8d..Hom_struct_b_pack : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 . MagmaHom (pack_b x0 x2) (pack_b x1 x3) x4 = and (x4setexp x1 x0) (∀ x6 . x6x0∀ x7 . x7x0ap x4 (x2 x6 x7) = x3 (ap x4 x6) (ap x4 x7))
Known neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Known lam_Pilam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x2 x3x1 x3)lam x0 x2Pi x0 x1
Known In_1_2In_1_2 : 12
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known SNo_1SNo_1 : SNo 1
Known In_0_2In_0_2 : 02
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known SNo_0SNo_0 : SNo 0
Known pack_struct_b_Ipack_struct_b_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)struct_b (pack_b x0 x1)
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known cases_2cases_2 : ∀ x0 . x02∀ x1 : ι → ο . x1 0x1 1x1 x0
Param omegaomega : ι
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Param nat_pnat_p : ιο
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known nat_2nat_2 : nat_p 2
Theorem 87240.. : not (∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p Monoid MagmaHom struct_id struct_comp x1 x3x2)x2)x0)x0) (proof)
Definition MetaCat_equalizer_pequalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11∀ x12 . x1 x11 x4 x12x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13x3 x11 x8 x4 x9 x13 = x12x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_pequalizer_constr_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7x0 x8∀ x9 x10 . x1 x7 x8 x9x1 x7 x8 x10MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Known pack_b_0_eq2pack_b_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = ap (pack_b x0 x1) 0
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known In_0_1In_0_1 : 01
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Theorem e6a94.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p Monoid MagmaHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0) (proof)
Definition MetaCat_pullback_ppullback_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13∀ x14 . x1 x13 x4 x14∀ x15 . x1 x13 x5 x15x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16x3 x13 x9 x4 x10 x16 = x14x3 x13 x9 x5 x11 x16 = x15x16 = x12 x13 x14 x15))
Definition MetaCat_pullback_struct_ppullback_constr_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8x0 x9x0 x10∀ x11 x12 . x1 x8 x10 x11x1 x9 x10 x12MetaCat_pullback_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12)
Known and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Theorem e5932.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p Monoid MagmaHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0) (proof)
Param MetaAdjunction_strictMetaAdjunction_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Param TrueTrue : ο
Param HomSetSetHom : ιιιο
Definition lam_idlam_id := λ x0 . lam x0 (λ x1 . x1)
Known 80cab..MetaCatSet_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . True) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x1 x3x2)x2)x0)x0
Known 09501.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 . ∀ x15 : ι → ι . MetaCat_initial_p x0 x1 x2 x3 x14 x15∀ x16 : ο . (∀ x17 : ι → ι . MetaCat_initial_p x4 x5 x6 x7 (x8 x14) x17x16)x16
Theorem 62ee6.. : not (∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) Monoid MagmaHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0) (proof)