Search for blocks/addresses/...

Proofgold Address

address
PUbuz5i3FBg4FyQ1n2WKjKVfYVpMxmqQg4Q
total
0
mg
-
conjpub
-
current assets
67feb../035a5.. bday: 4897 doc published by Pr6Pc..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition surjsurj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known bij_surjbij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2surj x0 x1 x2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param omegaomega : ι
Param SepSep : ι(ιο) → ι
Definition nInnIn := λ x0 x1 . not (x0x1)
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Theorem form100_22_v3form100_22_v3 : ∀ x0 : ι → ι . not (surj omega (prim4 omega) x0) (proof)
Param ccad8.. : ιιο
Known 536c8.. : ∀ x0 x1 . ccad8.. x0 x1∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Theorem 651e5.. : not (ccad8.. omega (prim4 omega)) (proof)
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Param ReplSepReplSep : ι(ιο) → (ιι) → ι
Known ReplSepIReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3x0x1 x3x2 x3ReplSep x0 x1 x2
Known ReplSepE_impredReplSepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3ReplSep x0 x1 x2∀ x4 : ο . (∀ x5 . x5x0x1 x5x3 = x2 x5x4)x4
Theorem form100_22_v2form100_22_v2 : ∀ x0 : ι → ι . not (inj (prim4 omega) omega x0) (proof)

previous assets