Search for blocks/addresses/...

Proofgold Asset

asset id
26905e56504040e6388a87daed709f7256b046623266271e995b2fc438917913
asset hash
eb4a0fc35ad9b9ca5726506afa9feb165514d410d7575cca25f38f913b1e8949
bday / block
1745
tx
a68ac..
preasset
doc published by PrGxv..
Definition False := ∀ x0 : ο . x0
Definition True := ∀ x0 : ο . x0x0
Definition not := λ x0 : ο . x0False
Theorem FalseE : False∀ x0 : ο . x0 (proof)
Theorem TrueI : True (proof)
Theorem notI : ∀ x0 : ο . (x0False)not x0 (proof)
Theorem notE : ∀ x0 : ο . not x0x0False (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Theorem andI : ∀ x0 x1 : ο . x0x1and x0 x1 (proof)
Theorem andEL : ∀ x0 x1 : ο . and x0 x1x0 (proof)
Theorem andER : ∀ x0 x1 : ο . and x0 x1x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Theorem orIL : ∀ x0 x1 : ο . x0or x0 x1 (proof)
Theorem orIR : ∀ x0 x1 : ο . x1or x0 x1 (proof)
Theorem orE : ∀ x0 x1 x2 : ο . (x0x2)(x1x2)or x0 x1x2 (proof)
Definition iff := λ x0 x1 : ο . and (x0x1) (x1x0)
Theorem iffEL : ∀ x0 x1 : ο . iff x0 x1x0x1 (proof)
Theorem iffER : ∀ x0 x1 : ο . iff x0 x1x1x0 (proof)
Theorem iffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1 (proof)
Theorem iff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Theorem pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2x1 x2)(∀ x2 . x1 x2x0 x2)x0 = x1 (proof)
Theorem pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2))x0 = x1 (proof)
Definition 8ac9a.. := λ x0 . False
Definition de327.. := λ x0 : ι → ο . λ x1 x2 . or (x0 x2) (x2 = x1)
Theorem 0998e.. : ∀ x0 : ι → ο . ∀ x1 x2 . x0 x2de327.. x0 x1 x2 (proof)
Theorem f147c.. : ∀ x0 : ι → ο . ∀ x1 . de327.. x0 x1 x1 (proof)
Theorem 8bcd6.. : ∀ x0 : ι → ο . ∀ x1 x2 . de327.. x0 x1 x2∀ x3 : ο . (x0 x2x3)(x2 = x1x3)x3 (proof)