Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr445..
/
86b85..
PUMrV..
/
e2e85..
vout
Pr445..
/
55b8b..
0.98 bars
TMQYS..
/
527ec..
ownership of
ac364..
as prop with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
TMLRX..
/
6dc07..
ownership of
35386..
as prop with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
TMRe4..
/
56538..
ownership of
17fce..
as prop with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
TMUCP..
/
4947c..
ownership of
97a11..
as prop with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
TMQ6z..
/
d8141..
ownership of
e29a2..
as obj with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
TMcDM..
/
48821..
ownership of
4f4ed..
as obj with payaddr
PrCx1..
rights free controlledby
PrCx1..
upto 0
PUfuv..
/
89c2d..
doc published by
PrCx1..
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
)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
struct_u
struct_u
:
ι
→
ο
Param
unpack_u_o
unpack_u_o
:
ι
→
(
ι
→
(
ι
→
ι
) →
ο
) →
ο
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
Permutation
struct_u_bij
:=
λ x0 .
and
(
struct_u
x0
)
(
unpack_u_o
x0
(
λ x1 .
bij
x1
x1
)
)
Param
MetaCat
MetaCat
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Param
UnaryFuncHom
Hom_struct_u
:
ι
→
ι
→
ι
→
ο
Known
7ce95..
MetaCat_struct_u_gen
:
∀ x0 :
ι → ο
.
(
∀ x1 .
x0
x1
⟶
struct_u
x1
)
⟶
MetaCat
x0
UnaryFuncHom
(
λ x1 .
lam_id
(
ap
x1
0
)
)
(
λ x1 x2 x3 .
lam_comp
(
ap
x1
0
)
)
Theorem
17fce..
MetaCat_struct_u_bij
:
MetaCat
Permutation
UnaryFuncHom
struct_id
struct_comp
(proof)
Param
MetaFunctor
MetaFunctor
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
) →
ο
Param
True
True
:
ο
Param
HomSet
SetHom
:
ι
→
ι
→
ι
→
ο
Known
6eadb..
MetaCat_struct_u_Forgetful_gen
:
∀ x0 :
ι → ο
.
(
∀ x1 .
x0
x1
⟶
struct_u
x1
)
⟶
MetaFunctor
x0
UnaryFuncHom
(
λ 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
ac364..
MetaCat_struct_u_bij_Forgetful
:
MetaFunctor
Permutation
UnaryFuncHom
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_p
initial_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
(
ι
→
ι
) →
ο
Conjecture
955bd..
MetaCat_struct_u_bij_initial
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
MetaCat_initial_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_terminal_p
terminal_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
(
ι
→
ι
) →
ο
Conjecture
32041..
MetaCat_struct_u_bij_terminal
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
MetaCat_terminal_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_coproduct_constr_p
coproduct_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
fc15b..
MetaCat_struct_u_bij_coproduct_constr
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coproduct_constr_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_product_constr_p
product_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
6ce53..
MetaCat_struct_u_bij_product_constr
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_product_constr_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_coequalizer_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
d7632..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coequalizer_buggy_struct_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_equalizer_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
d5581..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_equalizer_buggy_struct_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_pushout_buggy_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
12e44..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pushout_buggy_constr_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_pullback_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
5bd29..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pullback_buggy_struct_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_exp_constr_p
product_exponent_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
c5610..
MetaCat_struct_u_bij_product_exponent
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x8 : ο .
(
∀ x9 :
ι →
ι → ι
.
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι → ι
.
(
∀ x12 : ο .
(
∀ x13 :
ι →
ι →
ι →
ι → ι
.
MetaCat_exp_constr_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
x9
x11
x13
⟶
x12
)
⟶
x12
)
⟶
x10
)
⟶
x10
)
⟶
x8
)
⟶
x8
)
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_subobject_classifier_buggy_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
(
ι
→
ι
) →
ι
→
ι
→
(
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
b92db..
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 .
(
∀ x6 : ο .
(
∀ x7 .
(
∀ x8 : ο .
(
∀ x9 :
ι →
ι →
ι → ι
.
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_subobject_classifier_buggy_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
x9
x11
⟶
x10
)
⟶
x10
)
⟶
x8
)
⟶
x8
)
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_nno_p
nno_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
(
ι
→
ι
) →
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
cdd84..
MetaCat_struct_u_bij_nno
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 .
(
∀ x6 : ο .
(
∀ x7 .
(
∀ x8 : ο .
(
∀ x9 .
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι →
ι → ι
.
MetaCat_nno_p
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
x5
x7
x9
x11
⟶
x10
)
⟶
x10
)
⟶
x8
)
⟶
x8
)
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaAdjunction_strict
MetaAdjunction_strict
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
) →
(
ι
→
ι
) →
ο
Conjecture
a69df..
MetaCat_struct_u_bij_left_adjoint_forgetful
:
∀ x0 : ο .
(
∀ x1 :
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι → ι
.
MetaAdjunction_strict
(
λ x8 .
True
)
HomSet
lam_id
(
λ x8 x9 x10 .
lam_comp
x8
)
Permutation
UnaryFuncHom
struct_id
struct_comp
x1
x3
(
λ x8 .
ap
x8
0
)
(
λ x8 x9 x10 .
x10
)
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0