Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrQPb..
/
16fbf..
PULED..
/
8986a..
vout
PrQPb..
/
21f00..
19.87 bars
TMQA2..
/
3f58b..
ownership of
e3b51..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMH41..
/
c90e1..
ownership of
26b55..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPJA..
/
ad201..
ownership of
e157b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUZN..
/
5231b..
ownership of
815b9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbAK..
/
97fe8..
ownership of
8e102..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG8u..
/
09bdd..
ownership of
0da03..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFpD..
/
250ba..
ownership of
77076..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGSu..
/
19020..
ownership of
36ff5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHgU..
/
2936f..
ownership of
6ff04..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYhZ..
/
a8332..
ownership of
e125a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWbp..
/
13f03..
ownership of
17e44..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRdc..
/
cb2ea..
ownership of
e0eee..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJKG..
/
9970b..
ownership of
f16ac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYe8..
/
2b5fd..
ownership of
65312..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdrn..
/
6b6d0..
ownership of
7d9f7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaNX..
/
16704..
ownership of
67e2c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRCs..
/
83c9f..
ownership of
745b1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNqK..
/
7fd05..
ownership of
622c3..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaCG..
/
ff881..
ownership of
c7b84..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMeQ..
/
46de6..
ownership of
a93ca..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ6r..
/
692a2..
ownership of
7e80c..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
PUXmz..
/
c88a7..
doc published by
Pr6Pc..
Param
explicit_Ring_with_id
explicit_Ring_with_id
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
explicit_Ring_with_id_I
explicit_Ring_with_id_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x5
(
x3
x6
x7
)
=
x3
(
x3
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
=
x3
x6
x5
)
⟶
x1
∈
x0
⟶
(
∀ x5 .
x5
∈
x0
⟶
x3
x1
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∃ x6 .
and
(
x6
∈
x0
)
(
x3
x5
x6
=
x1
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x4
x6
x7
)
=
x4
(
x4
x5
x6
)
x7
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x4
x2
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x4
x5
x2
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x3
x6
x7
)
=
x3
(
x4
x5
x6
)
(
x4
x5
x7
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
(
x3
x5
x6
)
x7
=
x3
(
x4
x5
x7
)
(
x4
x6
x7
)
)
⟶
explicit_Ring_with_id
x0
x1
x2
x3
x4
Known
explicit_Ring_with_id_E
explicit_Ring_with_id_E
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 : ο .
(
explicit_Ring_with_id
x0
x1
x2
x3
x4
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x6
(
x3
x7
x8
)
=
x3
(
x3
x6
x7
)
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
=
x3
x7
x6
)
⟶
x1
∈
x0
⟶
(
∀ x6 .
x6
∈
x0
⟶
x3
x1
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∃ x7 .
and
(
x7
∈
x0
)
(
x3
x6
x7
=
x1
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x4
x7
x8
)
=
x4
(
x4
x6
x7
)
x8
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x6 : ο .
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
x4
x2
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
x4
x6
x2
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x3
x7
x8
)
=
x3
(
x4
x6
x7
)
(
x4
x6
x8
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
(
x3
x6
x7
)
x8
=
x3
(
x4
x6
x8
)
(
x4
x7
x8
)
)
⟶
x5
)
⟶
explicit_Ring_with_id
x0
x1
x2
x3
x4
⟶
x5
Param
nat_primrec
nat_primrec
:
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
Definition
explicit_Ring_with_id_exp_nat
explicit_Ring_with_id_exp_nat
:=
λ x0 x1 x2 .
λ x3 x4 :
ι →
ι → ι
.
λ x5 .
nat_primrec
x2
(
λ x6 .
x4
x5
)
Param
ap
ap
:
ι
→
ι
→
ι
Definition
explicit_Ring_with_id_eval_poly
explicit_Ring_with_id_eval_poly
:=
λ x0 x1 x2 .
λ x3 x4 :
ι →
ι → ι
.
λ x5 x6 x7 .
nat_primrec
x1
(
λ x8 .
x3
(
x4
(
ap
x6
x8
)
(
explicit_Ring_with_id_exp_nat
x0
x1
x2
x3
x4
x7
x8
)
)
)
x5
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
745b1..
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
explicit_Ring_with_id
x0
x1
x2
x3
x4
⟶
explicit_Ring_with_id
x0
x1
x2
x5
x6
...
Param
iff
iff
:
ο
→
ο
→
ο
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Theorem
explicit_Ring_with_id_repindep
explicit_Ring_with_id_repindep
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
iff
(
explicit_Ring_with_id
x0
x1
x2
x3
x4
)
(
explicit_Ring_with_id
x0
x1
x2
x5
x6
)
...
Param
explicit_CRing_with_id
explicit_CRing_with_id
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
Known
explicit_CRing_with_id_I
explicit_CRing_with_id_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x5
(
x3
x6
x7
)
=
x3
(
x3
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
=
x3
x6
x5
)
⟶
x1
∈
x0
⟶
(
∀ x5 .
x5
∈
x0
⟶
x3
x1
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∃ x6 .
and
(
x6
∈
x0
)
(
x3
x5
x6
=
x1
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x4
x6
x7
)
=
x4
(
x4
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
=
x4
x6
x5
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x4
x2
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x3
x6
x7
)
=
x3
(
x4
x5
x6
)
(
x4
x5
x7
)
)
⟶
explicit_CRing_with_id
x0
x1
x2
x3
x4
Known
explicit_CRing_with_id_E
explicit_CRing_with_id_E
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 : ο .
(
explicit_CRing_with_id
x0
x1
x2
x3
x4
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x6
(
x3
x7
x8
)
=
x3
(
x3
x6
x7
)
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
=
x3
x7
x6
)
⟶
x1
∈
x0
⟶
(
∀ x6 .
x6
∈
x0
⟶
x3
x1
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∃ x7 .
and
(
x7
∈
x0
)
(
x3
x6
x7
=
x1
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x4
x7
x8
)
=
x4
(
x4
x6
x7
)
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
=
x4
x7
x6
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x6 : ο .
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
x4
x2
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x3
x7
x8
)
=
x3
(
x4
x6
x7
)
(
x4
x6
x8
)
)
⟶
x5
)
⟶
explicit_CRing_with_id
x0
x1
x2
x3
x4
⟶
x5
Theorem
7d9f7..
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
explicit_CRing_with_id
x0
x1
x2
x3
x4
⟶
explicit_CRing_with_id
x0
x1
x2
x5
x6
...
Theorem
explicit_CRing_with_id_repindep
explicit_CRing_with_id_repindep
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
iff
(
explicit_CRing_with_id
x0
x1
x2
x3
x4
)
(
explicit_CRing_with_id
x0
x1
x2
x5
x6
)
...
Param
explicit_Field
explicit_Field
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
Known
explicit_Field_E
explicit_Field_E
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 : ο .
(
explicit_Field
x0
x1
x2
x3
x4
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x6
(
x3
x7
x8
)
=
x3
(
x3
x6
x7
)
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x6
x7
=
x3
x7
x6
)
⟶
x1
∈
x0
⟶
(
∀ x6 .
x6
∈
x0
⟶
x3
x1
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∃ x7 .
and
(
x7
∈
x0
)
(
x3
x6
x7
=
x1
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
∈
x0
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x4
x7
x8
)
=
x4
(
x4
x6
x7
)
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x6
x7
=
x4
x7
x6
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x6 : ο .
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
x4
x2
x6
=
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
(
x6
=
x1
⟶
∀ x7 : ο .
x7
)
⟶
∃ x7 .
and
(
x7
∈
x0
)
(
x4
x6
x7
=
x2
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x6
(
x3
x7
x8
)
=
x3
(
x4
x6
x7
)
(
x4
x6
x8
)
)
⟶
x5
)
⟶
explicit_Field
x0
x1
x2
x3
x4
⟶
x5
Known
explicit_Field_I
explicit_Field_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x5
(
x3
x6
x7
)
=
x3
(
x3
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
=
x3
x6
x5
)
⟶
x1
∈
x0
⟶
(
∀ x5 .
x5
∈
x0
⟶
x3
x1
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∃ x6 .
and
(
x6
∈
x0
)
(
x3
x5
x6
=
x1
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x4
x6
x7
)
=
x4
(
x4
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
=
x4
x6
x5
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x4
x2
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
(
x5
=
x1
⟶
∀ x6 : ο .
x6
)
⟶
∃ x6 .
and
(
x6
∈
x0
)
(
x4
x5
x6
=
x2
)
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x3
x6
x7
)
=
x3
(
x4
x5
x6
)
(
x4
x5
x7
)
)
⟶
explicit_Field
x0
x1
x2
x3
x4
Theorem
f16ac..
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
explicit_Field
x0
x1
x2
x3
x4
⟶
explicit_Field
x0
x1
x2
x5
x6
...
Theorem
explicit_Field_repindep
explicit_Field_repindep
:
∀ x0 x1 x2 .
∀ x3 x4 x5 x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x3
x7
x8
=
x5
x7
x8
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x4
x7
x8
=
x6
x7
x8
)
⟶
iff
(
explicit_Field
x0
x1
x2
x3
x4
)
(
explicit_Field
x0
x1
x2
x5
x6
)
...
Theorem
17e44..
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
explicit_Field
x0
x1
x2
x3
x4
⟶
explicit_CRing_with_id
x0
x1
x2
x3
x4
...
Param
pack_b_b_e_e
pack_b_b_e_e
:
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ι
→
ι
→
ι
Definition
struct_b_b_e_e
struct_b_b_e_e
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x2
⟶
∀ x5 .
x5
∈
x2
⟶
x3
x4
x5
∈
x2
)
⟶
∀ x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x2
⟶
∀ x6 .
x6
∈
x2
⟶
x4
x5
x6
∈
x2
)
⟶
∀ x5 .
x5
∈
x2
⟶
∀ x6 .
x6
∈
x2
⟶
x1
(
pack_b_b_e_e
x2
x3
x4
x5
x6
)
)
⟶
x1
x0
Param
unpack_b_b_e_e_o
unpack_b_b_e_e_o
:
ι
→
(
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ι
→
ι
→
ο
) →
ο
Known
unpack_b_b_e_e_o_eq
unpack_b_b_e_e_o_eq
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
(
ι →
ι → ι
)
→
ι →
ι → ο
.
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
∀ x4 x5 .
(
∀ x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
x2
x7
x8
=
x6
x7
x8
)
⟶
∀ x7 :
ι →
ι → ι
.
(
∀ x8 .
x8
∈
x1
⟶
∀ x9 .
x9
∈
x1
⟶
x3
x8
x9
=
x7
x8
x9
)
⟶
x0
x1
x6
x7
x4
x5
=
x0
x1
x2
x3
x4
x5
)
⟶
unpack_b_b_e_e_o
(
pack_b_b_e_e
x1
x2
x3
x4
x5
)
x0
=
x0
x1
x2
x3
x4
x5
Definition
Ring_with_id
Ring_with_id
:=
λ x0 .
and
(
struct_b_b_e_e
x0
)
(
unpack_b_b_e_e_o
x0
(
λ x1 .
λ x2 x3 :
ι →
ι → ι
.
λ x4 x5 .
explicit_Ring_with_id
x1
x4
x5
x2
x3
)
)
Known
prop_ext
prop_ext
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x0
=
x1
Theorem
Ring_with_id_unpack_eq
Ring_with_id_unpack_eq
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ι
.
∀ x3 x4 .
unpack_b_b_e_e_o
(
pack_b_b_e_e
x0
x1
x2
x3
x4
)
(
λ x6 .
λ x7 x8 :
ι →
ι → ι
.
λ x9 x10 .
explicit_Ring_with_id
x6
x9
x10
x7
x8
)
=
explicit_Ring_with_id
x0
x3
x4
x1
x2
...
Definition
CRing_with_id
CRing_with_id
:=
λ x0 .
and
(
struct_b_b_e_e
x0
)
(
unpack_b_b_e_e_o
x0
(
λ x1 .
λ x2 x3 :
ι →
ι → ι
.
λ x4 x5 .
explicit_CRing_with_id
x1
x4
x5
x2
x3
)
)
Theorem
CRing_with_id_unpack_eq
CRing_with_id_unpack_eq
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ι
.
∀ x3 x4 .
unpack_b_b_e_e_o
(
pack_b_b_e_e
x0
x1
x2
x3
x4
)
(
λ x6 .
λ x7 x8 :
ι →
ι → ι
.
λ x9 x10 .
explicit_CRing_with_id
x6
x9
x10
x7
x8
)
=
explicit_CRing_with_id
x0
x3
x4
x1
x2
...
Definition
Field
Field
:=
λ 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
)
)
Theorem
Field_unpack_eq
Field_unpack_eq
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ι
.
∀ x3 x4 .
unpack_b_b_e_e_o
(
pack_b_b_e_e
x0
x1
x2
x3
x4
)
(
λ x6 .
λ x7 x8 :
ι →
ι → ι
.
λ x9 x10 .
explicit_Field
x6
x9
x10
x7
x8
)
=
explicit_Field
x0
x3
x4
x1
x2
...
Known
explicit_CRing_with_id_Ring_with_id
explicit_CRing_with_id_Ring_with_id
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
explicit_CRing_with_id
x0
x1
x2
x3
x4
⟶
explicit_Ring_with_id
x0
x1
x2
x3
x4
Theorem
CRing_with_id_is_Ring_with_id
CRing_with_id_is_Ring_with_id
:
∀ x0 .
CRing_with_id
x0
⟶
Ring_with_id
x0
...
Theorem
Field_is_CRing_with_id
Field_is_CRing_with_id
:
∀ x0 .
Field
x0
⟶
CRing_with_id
x0
...