Search for blocks/addresses/...

Proofgold Asset

asset id
5082bb8ed3a7d8fd1aa27044a7194992c1cc7cfcbb2a7c2af103e12069a3e796
asset hash
636dfce838959fe06909a1a2a4b84ec22e8e7283edbfe73f6e1d6ad662e61002
bday / block
1605
tx
f69d8..
preasset
theory published by PrGxv..
Prim 0/5cb91.. : (ιο) → ι
Def False : ο := ∀ x0 : ο . x0
Def not : οο := λ x0 : ο . x0False
Def and : οοο := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Def or : οοο := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Def iff : οοο := λ x0 x1 : ο . and (x0x1) (x1x0)
Axiom prop_ext : ∀ x0 x1 : ο . iff x0 x1x0 = x1
Prim 1/6e234.. : ιιο
Def Subq : ιιο := λ x0 x1 . ∀ x2 . prim1 x2 x0prim1 x2 x1
Prim 2/f5912.. : ιιι
Def 91630.. : ιι := λ x0 . prim2 x0 x0
Prim 3/961fc.. : ιι
Def 7ee77.. : ιιι := λ x0 x1 . prim2 (prim2 x0 x1) (91630.. x0)
Def c2e41.. : ιιο := λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (and (∀ x4 . prim1 x4 x0∀ x5 : ο . (∀ x6 . and (prim1 x6 x1) (prim1 (7ee77.. x4 x6) x3)x5)x5) (∀ x4 . prim1 x4 x1∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (prim1 (7ee77.. x6 x4) x3)x5)x5)) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x3prim1 (7ee77.. x6 x7) x3iff (x4 = x6) (x5 = x7))x2)x2
Axiom Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (prim0 x0)
Axiom 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1))x0 = x1
Axiom 53c21.. : ∀ x0 x1 x2 . iff (prim1 x0 (prim2 x1 x2)) (or (x0 = x1) (x0 = x2))
Axiom UnionEq : ∀ x0 x1 . iff (prim1 x1 (prim3 x0)) (∀ x2 : ο . (∀ x3 . and (prim1 x1 x3) (prim1 x3 x0)x2)x2)
Axiom 113d7.. : ∀ x0 x1 . prim1 x1 x0∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (not (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (prim1 x5 x3)x4)x4))x2)x2
Axiom e8b3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 x4 . x1 x2 x3x1 x2 x4x3 = x4)∀ x2 : ο . (∀ x3 . (∀ x4 . iff (prim1 x4 x3) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (x1 x6 x4)x5)x5))x2)x2
Axiom adb47.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (prim1 x0 x2) (∀ x3 x4 . prim1 x3 x2Subq x4 x3prim1 x4 x2)) (∀ x3 . prim1 x3 x2∀ x4 : ο . (∀ x5 . and (prim1 x5 x2) (∀ x6 . Subq x6 x3prim1 x6 x5)x4)x4)) (∀ x3 . Subq x3 x2or (c2e41.. x3 x2) (prim1 x3 x2))x1)x1