Search for blocks/addresses/...

Proofgold Asset

asset id
ef42f61ad3c4c174feeeec6a5597c68692d09542f7a72ba60620bf33bad558fe
asset hash
0e51138a30b3d021b6db24f8575b42465be63704d913d2babc2d1e5a27859b1a
bday / block
18009
tx
603d5..
preasset
doc published by Pr4zB..
Param ordsuccordsucc : ιι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Theorem neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0 (proof)
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Theorem neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0 (proof)
Known neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0
Theorem neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0 (proof)
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Theorem neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0 (proof)
Known neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0
Theorem neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0 (proof)
Known neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0
Theorem neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0 (proof)
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Theorem neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0 (proof)
Known neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0
Theorem neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0 (proof)
Known neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0
Theorem neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0 (proof)
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Theorem neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0 (proof)
Known neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0
Theorem neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0 (proof)
Known neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0
Theorem neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0 (proof)
Known neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0
Theorem neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0 (proof)
Known neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0
Theorem neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0 (proof)
Known neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0
Theorem neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0 (proof)
Known neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0
Theorem neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0 (proof)
Known neq_6_1neq_6_1 : u6 = u1∀ x0 : ο . x0
Theorem neq_6_1neq_6_1 : u6 = u1∀ x0 : ο . x0 (proof)
Known neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0
Theorem neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0 (proof)
Known neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0
Theorem neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0 (proof)
Known neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0
Theorem neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0 (proof)
Known neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0
Theorem neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0 (proof)
Known neq_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0
Theorem neq_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0 (proof)
Known neq_7_1neq_7_1 : u7 = u1∀ x0 : ο . x0
Theorem neq_7_1neq_7_1 : u7 = u1∀ x0 : ο . x0 (proof)
Known neq_7_2neq_7_2 : u7 = u2∀ x0 : ο . x0
Theorem neq_7_2neq_7_2 : u7 = u2∀ x0 : ο . x0 (proof)
Known neq_7_3neq_7_3 : u7 = u3∀ x0 : ο . x0
Theorem neq_7_3neq_7_3 : u7 = u3∀ x0 : ο . x0 (proof)
Known neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0
Theorem neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0 (proof)
Known neq_7_5neq_7_5 : u7 = u5∀ x0 : ο . x0
Theorem neq_7_5neq_7_5 : u7 = u5∀ x0 : ο . x0 (proof)
Known neq_7_6neq_7_6 : u7 = u6∀ x0 : ο . x0
Theorem neq_7_6neq_7_6 : u7 = u6∀ x0 : ο . x0 (proof)
Known neq_8_0neq_8_0 : u8 = 0∀ x0 : ο . x0
Theorem neq_8_0neq_8_0 : u8 = 0∀ x0 : ο . x0 (proof)
Known neq_8_1neq_8_1 : u8 = u1∀ x0 : ο . x0
Theorem neq_8_1neq_8_1 : u8 = u1∀ x0 : ο . x0 (proof)
Known neq_8_2neq_8_2 : u8 = u2∀ x0 : ο . x0
Theorem neq_8_2neq_8_2 : u8 = u2∀ x0 : ο . x0 (proof)
Known neq_8_3neq_8_3 : u8 = u3∀ x0 : ο . x0
Theorem neq_8_3neq_8_3 : u8 = u3∀ x0 : ο . x0 (proof)
Known neq_8_4neq_8_4 : u8 = u4∀ x0 : ο . x0
Theorem neq_8_4neq_8_4 : u8 = u4∀ x0 : ο . x0 (proof)
Known neq_8_5neq_8_5 : u8 = u5∀ x0 : ο . x0
Theorem neq_8_5neq_8_5 : u8 = u5∀ x0 : ο . x0 (proof)
Known neq_8_6neq_8_6 : u8 = u6∀ x0 : ο . x0
Theorem neq_8_6neq_8_6 : u8 = u6∀ x0 : ο . x0 (proof)
Known neq_8_7neq_8_7 : u8 = u7∀ x0 : ο . x0
Theorem neq_8_7neq_8_7 : u8 = u7∀ x0 : ο . x0 (proof)
Known neq_9_0neq_9_0 : u9 = 0∀ x0 : ο . x0
Theorem neq_9_0neq_9_0 : u9 = 0∀ x0 : ο . x0 (proof)
Known neq_9_1neq_9_1 : u9 = u1∀ x0 : ο . x0
Theorem neq_9_1neq_9_1 : u9 = u1∀ x0 : ο . x0 (proof)
Known neq_9_2neq_9_2 : u9 = u2∀ x0 : ο . x0
Theorem neq_9_2neq_9_2 : u9 = u2∀ x0 : ο . x0 (proof)
Known neq_9_3neq_9_3 : u9 = u3∀ x0 : ο . x0
Theorem neq_9_3neq_9_3 : u9 = u3∀ x0 : ο . x0 (proof)
Known neq_9_4neq_9_4 : u9 = u4∀ x0 : ο . x0
Theorem neq_9_4neq_9_4 : u9 = u4∀ x0 : ο . x0 (proof)
Known neq_9_5neq_9_5 : u9 = u5∀ x0 : ο . x0
Theorem neq_9_5neq_9_5 : u9 = u5∀ x0 : ο . x0 (proof)
Known neq_9_6neq_9_6 : u9 = u6∀ x0 : ο . x0
Theorem neq_9_6neq_9_6 : u9 = u6∀ x0 : ο . x0 (proof)
Known neq_9_7neq_9_7 : u9 = u7∀ x0 : ο . x0
Theorem neq_9_7neq_9_7 : u9 = u7∀ x0 : ο . x0 (proof)
Known neq_9_8neq_9_8 : u9 = u8∀ x0 : ο . x0
Theorem neq_9_8neq_9_8 : u9 = u8∀ x0 : ο . x0 (proof)
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Theorem 0e10e.. : u10 = 0∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contraordsucc_inj_contra : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)ordsucc x0 = ordsucc x1∀ x2 : ο . x2
Theorem d183f.. : u10 = u1∀ x0 : ο . x0 (proof)
Theorem e02d9.. : u10 = u2∀ x0 : ο . x0 (proof)
Theorem 68152.. : u10 = u3∀ x0 : ο . x0 (proof)
Theorem 33d16.. : u10 = u4∀ x0 : ο . x0 (proof)
Theorem a7d50.. : u10 = u5∀ x0 : ο . x0 (proof)
Theorem d0401.. : u10 = u6∀ x0 : ο . x0 (proof)
Theorem 7d7a8.. : u10 = u7∀ x0 : ο . x0 (proof)
Theorem 96175.. : u10 = u8∀ x0 : ο . x0 (proof)
Theorem 4fc31.. : u10 = u9∀ x0 : ο . x0 (proof)
Theorem 19f75.. : u11 = 0∀ x0 : ο . x0 (proof)
Theorem 618f7.. : u11 = u1∀ x0 : ο . x0 (proof)
Theorem 2c42c.. : u11 = u2∀ x0 : ο . x0 (proof)
Theorem b06e1.. : u11 = u3∀ x0 : ο . x0 (proof)
Theorem 6a6f1.. : u11 = u4∀ x0 : ο . x0 (proof)
Theorem 1b659.. : u11 = u5∀ x0 : ο . x0 (proof)
Theorem 949f2.. : u11 = u6∀ x0 : ο . x0 (proof)
Theorem 4abfa.. : u11 = u7∀ x0 : ο . x0 (proof)
Theorem b3a20.. : u11 = u8∀ x0 : ο . x0 (proof)
Theorem 4f03f.. : u11 = u9∀ x0 : ο . x0 (proof)
Theorem ebfb7.. : u11 = u10∀ x0 : ο . x0 (proof)
Theorem efdfc.. : u12 = 0∀ x0 : ο . x0 (proof)
Theorem ce0cd.. : u12 = u1∀ x0 : ο . x0 (proof)
Theorem 8158b.. : u12 = u2∀ x0 : ο . x0 (proof)
Theorem e015c.. : u12 = u3∀ x0 : ο . x0 (proof)
Theorem 7aa79.. : u12 = u4∀ x0 : ο . x0 (proof)
Theorem 07eba.. : u12 = u5∀ x0 : ο . x0 (proof)
Theorem 0bd83.. : u12 = u6∀ x0 : ο . x0 (proof)
Theorem 6a15f.. : u12 = u7∀ x0 : ο . x0 (proof)
Theorem a6a6c.. : u12 = u8∀ x0 : ο . x0 (proof)
Theorem 22885.. : u12 = u9∀ x0 : ο . x0 (proof)
Theorem 6c583.. : u12 = u10∀ x0 : ο . x0 (proof)
Theorem ab306.. : u12 = u11∀ x0 : ο . x0 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known cases_9cases_9 : ∀ x0 . x09∀ x1 : ι → ο . x1 0x1 1x1 2x1 3x1 4x1 5x1 6x1 7x1 8x1 x0
Theorem 44418.. : ∀ x0 . x0u10∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 x0 (proof)
Theorem 83484.. : ∀ x0 . x0u11∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 u10x1 x0 (proof)
Theorem 866c8.. : ∀ x0 . x0u12∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 x0 (proof)
Theorem 6de8d.. : ∀ x0 . x0u13∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 x0 (proof)