Search for blocks/addresses/...

Proofgold Asset

asset id
dbe54c52fe4ffc587c1d49345c6e9278a44292845fd14dc2a8ef012ac2dda915
asset hash
1509e420e3ed94f0cbbb4084d5dc2ba604f21e20f334ed1bff39205dfb2a1351
bday / block
4905
tx
70a36..
preasset
doc published by Pr6Pc..
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Known In_0_5In_0_5 : 05
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Theorem tuple_5_0_eqtuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0 (proof)
Known In_1_5In_1_5 : 15
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Theorem tuple_5_1_eqtuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1 (proof)
Known In_2_5In_2_5 : 25
Known neq_2_0neq_2_0 : 2 = 0∀ x0 : ο . x0
Known neq_2_1neq_2_1 : 2 = 1∀ x0 : ο . x0
Theorem tuple_5_2_eqtuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2 (proof)
Known In_3_5In_3_5 : 35
Known neq_3_0neq_3_0 : 3 = 0∀ x0 : ο . x0
Known neq_3_1neq_3_1 : 3 = 1∀ x0 : ο . x0
Known neq_3_2neq_3_2 : 3 = 2∀ x0 : ο . x0
Theorem tuple_5_3_eqtuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3 (proof)
Known In_4_5In_4_5 : 45
Known neq_4_0neq_4_0 : 4 = 0∀ x0 : ο . x0
Known neq_4_1neq_4_1 : 4 = 1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : 4 = 2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : 4 = 3∀ x0 : ο . x0
Theorem tuple_5_4_eqtuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4 (proof)
Known In_0_6In_0_6 : 06
Theorem tuple_6_0_eqtuple_6_0_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 0 = x0 (proof)
Known In_1_6In_1_6 : 16
Theorem tuple_6_1_eqtuple_6_1_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 1 = x1 (proof)
Known In_2_6In_2_6 : 26
Theorem tuple_6_2_eqtuple_6_2_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 2 = x2 (proof)
Known In_3_6In_3_6 : 36
Theorem tuple_6_3_eqtuple_6_3_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 3 = x3 (proof)
Known In_4_6In_4_6 : 46
Theorem tuple_6_4_eqtuple_6_4_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 4 = x4 (proof)
Known In_5_6In_5_6 : 56
Known neq_5_0neq_5_0 : 5 = 0∀ x0 : ο . x0
Known neq_5_1neq_5_1 : 5 = 1∀ x0 : ο . x0
Known neq_5_2neq_5_2 : 5 = 2∀ x0 : ο . x0
Known neq_5_3neq_5_3 : 5 = 3∀ x0 : ο . x0
Known neq_5_4neq_5_4 : 5 = 4∀ x0 : ο . x0
Theorem tuple_6_5_eqtuple_6_5_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 5 = x5 (proof)
Known In_0_7In_0_7 : 07
Theorem tuple_7_0_eqtuple_7_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 0 = x0 (proof)
Known In_1_7In_1_7 : 17
Theorem tuple_7_1_eqtuple_7_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 1 = x1 (proof)
Known In_2_7In_2_7 : 27
Theorem tuple_7_2_eqtuple_7_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 2 = x2 (proof)
Known In_3_7In_3_7 : 37
Theorem tuple_7_3_eqtuple_7_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 3 = x3 (proof)
Known In_4_7In_4_7 : 47
Theorem tuple_7_4_eqtuple_7_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 4 = x4 (proof)
Known In_5_7In_5_7 : 57
Theorem tuple_7_5_eqtuple_7_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 5 = x5 (proof)
Known In_6_7In_6_7 : 67
Known neq_6_0neq_6_0 : 6 = 0∀ x0 : ο . x0
Known neq_6_1neq_6_1 : 6 = 1∀ x0 : ο . x0
Known neq_6_2neq_6_2 : 6 = 2∀ x0 : ο . x0
Known neq_6_3neq_6_3 : 6 = 3∀ x0 : ο . x0
Known neq_6_4neq_6_4 : 6 = 4∀ x0 : ο . x0
Known neq_6_5neq_6_5 : 6 = 5∀ x0 : ο . x0
Theorem tuple_7_6_eqtuple_7_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 6 = x6 (proof)