Search for blocks/addresses/...

Proofgold Address

address
PUJmjqUJpJsE5eZNAnYHKR4K6zRuFXmvGAC
total
0
mg
-
conjpub
-
current assets
2acf1../ee74f.. bday: 31271 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
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known 179f3.. : 0u21
Theorem c34a2.. : 0u22 (proof)
Known 07fdb.. : u1u21
Theorem 617e2.. : u1u22 (proof)
Known c25ea.. : u2u21
Theorem a7839.. : u2u22 (proof)
Known 0750b.. : u3u21
Theorem 9018e.. : u3u22 (proof)
Known 701a9.. : u4u21
Theorem 540e6.. : u4u22 (proof)
Known 0dc69.. : u5u21
Theorem 8a085.. : u5u22 (proof)
Known 1d1d3.. : u6u21
Theorem 8f513.. : u6u22 (proof)
Known 0b77c.. : u7u21
Theorem 3224f.. : u7u22 (proof)
Known 5fc29.. : u8u21
Theorem e5453.. : u8u22 (proof)
Known 4b046.. : u9u21
Theorem 8413f.. : u9u22 (proof)
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Known d21a1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3∀ x5 : ο . x5)ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4
Known neq_5_0neq_5_0 : u5 = 0∀ x0 : ο . x0
Known neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0
Known neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0
Known neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0
Known neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0
Known 48efb.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0
Theorem 1f68f.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u5 = x5 (proof)
Known neq_6_0neq_6_0 : u6 = 0∀ x0 : ο . x0
Known neq_6_1neq_6_1 : u6 = u1∀ x0 : ο . x0
Known neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0
Known neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0
Known neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0
Known neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0
Theorem e1b97.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u6 = x6 (proof)
Known neq_7_0neq_7_0 : u7 = 0∀ x0 : ο . x0
Known neq_7_1neq_7_1 : u7 = u1∀ x0 : ο . x0
Known neq_7_2neq_7_2 : u7 = u2∀ x0 : ο . x0
Known neq_7_3neq_7_3 : u7 = u3∀ x0 : ο . x0
Known neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0
Known neq_7_5neq_7_5 : u7 = u5∀ x0 : ο . x0
Known neq_7_6neq_7_6 : u7 = u6∀ x0 : ο . x0
Theorem 9f38d.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u7 = x7 (proof)
Known neq_8_0neq_8_0 : u8 = 0∀ x0 : ο . x0
Known neq_8_1neq_8_1 : u8 = u1∀ x0 : ο . x0
Known neq_8_2neq_8_2 : u8 = u2∀ x0 : ο . x0
Known neq_8_3neq_8_3 : u8 = u3∀ x0 : ο . x0
Known neq_8_4neq_8_4 : u8 = u4∀ x0 : ο . x0
Known neq_8_5neq_8_5 : u8 = u5∀ x0 : ο . x0
Known neq_8_6neq_8_6 : u8 = u6∀ x0 : ο . x0
Known neq_8_7neq_8_7 : u8 = u7∀ x0 : ο . x0
Theorem 5f3eb.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u8 = x8 (proof)
Known neq_9_0neq_9_0 : u9 = 0∀ x0 : ο . x0
Known neq_9_1neq_9_1 : u9 = u1∀ x0 : ο . x0
Known neq_9_2neq_9_2 : u9 = u2∀ x0 : ο . x0
Known neq_9_3neq_9_3 : u9 = u3∀ x0 : ο . x0
Known neq_9_4neq_9_4 : u9 = u4∀ x0 : ο . x0
Known neq_9_5neq_9_5 : u9 = u5∀ x0 : ο . x0
Known neq_9_6neq_9_6 : u9 = u6∀ x0 : ο . x0
Known neq_9_7neq_9_7 : u9 = u7∀ x0 : ο . x0
Known neq_9_8neq_9_8 : u9 = u8∀ x0 : ο . x0
Theorem 6a2e0.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u9 = x9 (proof)
Definition 55574.. := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (lam 22 (λ x23 . If_i (x23 = 0) x1 (If_i (x23 = 1) x2 (If_i (x23 = 2) x3 (If_i (x23 = 3) x4 (If_i (x23 = 4) x5 (If_i (x23 = 5) x6 (If_i (x23 = 6) x7 (If_i (x23 = 7) x8 (If_i (x23 = 8) x9 (If_i (x23 = 9) x10 (If_i (x23 = 10) x11 (If_i (x23 = 11) x12 (If_i (x23 = 12) x13 (If_i (x23 = 13) x14 (If_i (x23 = 14) x15 (If_i (x23 = 15) x16 (If_i (x23 = 16) x17 (If_i (x23 = 17) x18 (If_i (x23 = 18) x19 (If_i (x23 = 19) x20 (If_i (x23 = 20) x21 x22)))))))))))))))))))))) x0
Theorem b535d.. : 55574.. u5 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x6 (proof)
Theorem 8ef56.. : 55574.. u6 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x7 (proof)
Theorem 151b0.. : 55574.. u7 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x8 (proof)
Theorem 9e99f.. : 55574.. u8 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x9 (proof)
Theorem 896c4.. : 55574.. u9 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x10 (proof)

previous assets