Search for blocks/addresses/...

Proofgold Address

address
PUUdk3KAbWaBTLH6mj39vTZXmiwb7oZ1f8p
total
0
mg
-
conjpub
-
current assets
87f2a../c5e39.. bday: 2719 doc published by PrGxv..
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
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)
Definition 91630.. := λ x0 . prim2 x0 x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0)x1 = x0
Theorem b9ebd.. : ∀ x0 . 91630.. x0 = prim2 x0 x0 (proof)
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 9ffeb.. : ∀ x0 x1 . 91630.. x0 = x1and (prim1 x0 x1) (∀ x2 . prim1 x2 x1x2 = x0) (proof)
Definition 7ee77.. := λ x0 x1 . prim2 (prim2 x0 x1) (91630.. x0)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2)or (x0 = x1) (x0 = x2)
Known 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1)
Known 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1)
Theorem 6c815.. : ∀ x0 x1 x2 x3 . 7ee77.. x0 x1 = 7ee77.. x2 x3x0 = x2 (proof)
Theorem 9480e.. : ∀ x0 x1 x2 x3 . 7ee77.. x0 x1 = 7ee77.. x2 x3x1 = x3 (proof)
Theorem 76a5f.. : ∀ x0 x1 x2 x3 . 7ee77.. x0 x1 = 7ee77.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Definition iff := λ x0 x1 : ο . and (x0x1) (x1x0)
Definition 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
Param 94f9e.. : ι(ιι) → ι
Known and3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0prim1 (x1 x2) (94f9e.. x0 x1)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1)∀ x3 : ο . (∀ x4 . prim1 x4 x0x2 = x1 x4x3)x3
Known iffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem c6ad4.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2c2e41.. x0 x1 (proof)
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (prim0 x0)
Theorem 64d57.. : ∀ x0 x1 . c2e41.. x0 x1∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2 (proof)
Known and4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Theorem and5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (and (and (and x0 x1) x2) x3) x4 (proof)
Known and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3∀ x4 : ο . (x0x1x2x3x4)x4
Theorem and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4∀ x5 : ο . (x0x1x2x3x4x5)x5 (proof)
Known orIL : ∀ x0 x1 : ο . x0or x0 x1
Known or4I1 : ∀ x0 x1 x2 x3 : ο . x0or (or (or x0 x1) x2) x3
Theorem or5I1 : ∀ x0 x1 x2 x3 x4 : ο . x0or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I2 : ∀ x0 x1 x2 x3 : ο . x1or (or (or x0 x1) x2) x3
Theorem or5I2 : ∀ x0 x1 x2 x3 x4 : ο . x1or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I3 : ∀ x0 x1 x2 x3 : ο . x2or (or (or x0 x1) x2) x3
Theorem or5I3 : ∀ x0 x1 x2 x3 x4 : ο . x2or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I4 : ∀ x0 x1 x2 x3 : ο . x3or (or (or x0 x1) x2) x3
Theorem or5I4 : ∀ x0 x1 x2 x3 x4 : ο . x3or (or (or (or x0 x1) x2) x3) x4 (proof)
Known orIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem or5I5 : ∀ x0 x1 x2 x3 x4 : ο . x4or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3∀ x4 : ο . (x0x4)(x1x4)(x2x4)(x3x4)x4
Theorem or5E : ∀ x0 x1 x2 x3 x4 : ο . or (or (or (or x0 x1) x2) x3) x4∀ x5 : ο . (x0x5)(x1x5)(x2x5)(x3x5)(x4x5)x5 (proof)
Theorem and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0x1x2x3x4x5and (and (and (and (and x0 x1) x2) x3) x4) x5 (proof)
Theorem and6E : ∀ x0 x1 x2 x3 x4 x5 : ο . and (and (and (and (and x0 x1) x2) x3) x4) x5∀ x6 : ο . (x0x1x2x3x4x5x6)x6 (proof)
Theorem and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0x1x2x3x4x5x6and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6 (proof)
Theorem and7E : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6∀ x7 : ο . (x0x1x2x3x4x5x6x7)x7 (proof)

previous assets