Search for blocks/addresses/...

Proofgold Address

address
PUMc8c6XCwpNw7K1mK12L1W72Jv2SiR5LbZ
total
0
mg
-
conjpub
-
current assets
41b30../9501c.. bday: 19014 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 SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known 2c104.. : 016
Theorem c5b55.. : 0u17 (proof)
Known 6ec80.. : 116
Theorem f6e42.. : u1u17 (proof)
Known b34ab.. : 216
Theorem 9502b.. : u2u17 (proof)
Known f312e.. : 316
Theorem 35c0a.. : u3u17 (proof)
Known add3d.. : 416
Theorem 793dd.. : u4u17 (proof)
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Theorem 192ab.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0)(∀ 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)∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) 0 = x0 (proof)
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Theorem 74e99.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0)(∀ 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)∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u1 = x1 (proof)
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Known neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0
Theorem c7cd7.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0)(∀ 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)∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u2 = x2 (proof)
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Known neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0
Known neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0
Theorem 2a0b0.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0)(∀ 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)∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u3 = x3 (proof)
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Known neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Theorem b09cb.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3x1ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0)(∀ 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)∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u4 = x4 (proof)

previous assets