Search for blocks/addresses/...

Proofgold Asset

asset id
e214d11554772971586cae541ec82d9c3902a5fa65dea25de88e2d342242a5a0
asset hash
9b49b140457466ad3133c1661f2995e755ef0cdcbebd2047237a9d95ebf2f998
bday / block
19017
tx
cde34..
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
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 fe610.. : 516
Theorem 79c48.. : u5u17 (proof)
Known 6d5be.. : 616
Theorem b3205.. : u6u17 (proof)
Known 64265.. : 716
Theorem 51ef0.. : u7u17 (proof)
Known 98f71.. : 816
Theorem 6a4e9.. : u8u17 (proof)
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
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
Theorem 497c7.. : (∀ 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))))))))))))))))) 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 5af4c.. : (∀ 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))))))))))))))))) 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 63896.. : (∀ 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))))))))))))))))) 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 9c74a.. : (∀ 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))))))))))))))))) u8 = x8 (proof)