Search for blocks/addresses/...

Proofgold Asset

asset id
1dcfeee30f80e34894e6878e4003e6a2ebcd06a2a010ee1fe129838c7ca192bf
asset hash
7125f5da5fec68e01ce71bc8e60bda2ddddb725969994d72a194d749b3ddeed5
bday / block
4838
tx
90e2b..
preasset
doc published by PrGxv..
Param e5b72.. : ιι
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0prim1 x2 x1
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param 1216a.. : ι(ιο) → ι
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Known set_ext : ∀ x0 x1 . Subq x0 x1Subq x1 x0x0 = x1
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0x1 x2prim1 x2 (1216a.. x0 x1)
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0)Subq x1 x0
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1)x1 x2
Known d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0)
Theorem bda2b.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (e5b72.. x0)prim1 (x1 x2) (e5b72.. x0))(∀ x2 . prim1 x2 (e5b72.. x0)∀ x3 . prim1 x3 (e5b72.. x0)Subq x2 x3Subq (x1 x2) (x1 x3))∀ x2 : ο . (∀ x3 . and (prim1 x3 (e5b72.. x0)) (x1 x3 = x3)x2)x2 (proof)
Param 94f9e.. : ι(ιι) → ι
Known 3daee.. : ∀ x0 x1 . Subq x1 x0prim1 x1 (e5b72.. x0)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1)∀ x3 : ο . (∀ x4 . prim1 x4 x0x2 = x1 x4x3)x3
Theorem 61f1b.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0prim1 (x2 x3) x1)∀ x3 . prim1 x3 (e5b72.. x0)prim1 (94f9e.. x3 x2) (e5b72.. x1) (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 13e07.. : ∀ x0 : ι → ι . ∀ x1 x2 . Subq x1 x2Subq (94f9e.. x1 x0) (94f9e.. x2 x0) (proof)
Param 1ad11.. : ιιι
Known dcf34.. : ∀ x0 x1 . Subq (1ad11.. x0 x1) x0
Theorem 89704.. : ∀ x0 x1 . prim1 (1ad11.. x0 x1) (e5b72.. x0) (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known 017d4.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1)and (prim1 x2 x0) (nIn x2 x1)
Known 753c4.. : ∀ x0 x1 x2 . prim1 x2 x0nIn x2 x1prim1 x2 (1ad11.. x0 x1)
Theorem 60320.. : ∀ x0 x1 x2 . Subq x1 x2Subq (1ad11.. x0 x2) (1ad11.. x0 x1) (proof)
Definition inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)
Param c2e41.. : ιιο
Param If_i : οιιι
Param inv : ι(ιι) → ιι
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . prim1 x3 x1∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3)x4)x4)
Known c6ad4.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2c2e41.. x0 x1
Known and3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known f775d.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)∀ x3 . prim1 x3 x0inv x0 x2 (x2 x3) = x3
Known 26c23.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1)prim1 x2 x0
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known FalseE : False∀ x0 : ο . x0
Theorem c698c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . inj x0 x1 x2inj x1 x0 x3c2e41.. x0 x1 (proof)