Search for blocks/addresses/...

Proofgold Asset

asset id
4b4765a960a5c327b412fb4288395d63a04f02223474e02b2766602cd13b7100
asset hash
de3662908a62d927ce3db7a75f1ae766ef49bc1100e53f168b32acdfe53df2e5
bday / block
19222
tx
ddf6a..
preasset
doc published by Pr4zB..
Definition Church6_p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2)x1 (λ x2 x3 x4 x5 x6 x7 . x3)x1 (λ x2 x3 x4 x5 x6 x7 . x4)x1 (λ x2 x3 x4 x5 x6 x7 . x5)x1 (λ x2 x3 x4 x5 x6 x7 . x6)x1 (λ x2 x3 x4 x5 x6 x7 . x7)x1 x0
Theorem 2d0c6.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x0) (proof)
Theorem bebec.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x1) (proof)
Theorem 8c295.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x2) (proof)
Theorem 3b22d.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x3) (proof)
Theorem 41e6a.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x4) (proof)
Theorem 28e18.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x5) (proof)
Param ordsuccordsucc : ιι
Definition u1 := 1
Param u2 : ι
Param u3 : ι
Param u4 : ι
Param u5 : ι
Definition Church6_to_u6 := λ x0 : ι → ι → ι → ι → ι → ι → ι . x0 0 u1 u2 u3 u4 u5
Param u6 : ι
Known cases_6cases_6 : ∀ x0 . x0u6∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 x0
Theorem cases_6cases_6 : ∀ x0 . x0u6∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 x0 (proof)
Known In_0_6In_0_6 : 0u6
Theorem In_0_6In_0_6 : 0u6 (proof)
Known In_1_6In_1_6 : u1u6
Theorem In_1_6In_1_6 : u1u6 (proof)
Known In_2_6In_2_6 : u2u6
Theorem In_2_6In_2_6 : u2u6 (proof)
Known In_3_6In_3_6 : u3u6
Theorem In_3_6In_3_6 : u3u6 (proof)
Known In_4_6In_4_6 : u4u6
Theorem In_4_6In_4_6 : u4u6 (proof)
Known In_5_6In_5_6 : u5u6
Theorem In_5_6In_5_6 : u5u6 (proof)
Theorem 17ae2.. : ∀ x0 . x0u6∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2x0 = Church6_to_u6 x2x1)x1 (proof)
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Definition nth_6_tuple := λ x0 x1 x2 x3 x4 x5 x6 . ap (lam 6 (λ x7 . If_i (x7 = 0) x1 (If_i (x7 = 1) x2 (If_i (x7 = 2) x3 (If_i (x7 = 3) x4 (If_i (x7 = 4) x5 x6)))))) x0
Theorem f957d.. : ∀ x0 . ∀ x1 : ι → ι → ι → ι → ι → ι → ι . (∀ x2 x3 x4 x5 x6 x7 . nth_6_tuple x0 x2 x3 x4 x5 x6 x7 = x1 x2 x3 x4 x5 x6 x7)nth_6_tuple x0 = x1 (proof)
Known 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)))))) u1 = x1
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)))))) u1 = x1 (proof)
Known 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)))))) u2 = x2
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)))))) u2 = x2 (proof)
Known 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)))))) u3 = x3
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)))))) u3 = x3 (proof)
Known 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)))))) u4 = x4
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)))))) u4 = x4 (proof)
Known 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)))))) u5 = x5
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)))))) u5 = x5 (proof)
Known 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
Theorem a1243.. : nth_6_tuple 0 = λ x1 x2 x3 x4 x5 x6 . x1 (proof)
Theorem a7cad.. : nth_6_tuple u1 = λ x1 x2 x3 x4 x5 x6 . x2 (proof)
Theorem a0d60.. : nth_6_tuple u2 = λ x1 x2 x3 x4 x5 x6 . x3 (proof)
Theorem 89684.. : nth_6_tuple u3 = λ x1 x2 x3 x4 x5 x6 . x4 (proof)
Theorem 33924.. : nth_6_tuple u4 = λ x1 x2 x3 x4 x5 x6 . x5 (proof)
Theorem fed6d.. : nth_6_tuple u5 = λ x1 x2 x3 x4 x5 x6 . x6 (proof)
Theorem 38ba0.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0Church6_to_u6 x0u6 (proof)
Theorem 3b8c0.. : ∀ x0 . x0u6Church6_p (nth_6_tuple x0) (proof)
Theorem 985a3.. : ∀ x0 . x0u6Church6_to_u6 (nth_6_tuple x0) = x0 (proof)
Theorem 60d0e.. : ∀ x0 . x0u6∀ x1 . x1u6nth_6_tuple x0 = nth_6_tuple x1x0 = x1 (proof)
Theorem 3ac64.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0nth_6_tuple (Church6_to_u6 x0) = x0 (proof)
Theorem b4e23.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0Church6_p x1Church6_to_u6 x0 = Church6_to_u6 x1x0 = x1 (proof)
Definition 8915b.. := λ x0 : ((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . lam 2 (λ x1 . If_i (x1 = 0) (Church6_to_u6 (x0 (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . x2))) (Church6_to_u6 (x0 (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . x3))))
Definition 4aafd.. := λ x0 . λ x1 : (ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . x1 (nth_6_tuple (ap x0 0)) (nth_6_tuple (ap x0 u1))
Definition 884c6.. := λ x0 : ((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι) → ο . (∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2Church6_p x3x1 (λ x4 : (ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . x4 x2 x3))x1 x0
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Theorem b4e0c.. : ∀ x0 : ((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . 884c6.. x08915b.. x0setprod u6 u6 (proof)
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Theorem b410a.. : ∀ x0 . x0setprod u6 u6884c6.. (4aafd.. x0) (proof)
Known tuple_Sigma_etatuple_Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Theorem f4bbb.. : ∀ x0 . x0setprod u6 u68915b.. (4aafd.. x0) = x0 (proof)
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem b98f5.. : ∀ x0 : ((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . 884c6.. x04aafd.. (8915b.. x0) = x0 (proof)
Theorem 0b928.. : ∀ x0 . x0setprod u6 u6∀ x1 . x1setprod u6 u64aafd.. x0 = 4aafd.. x1x0 = x1 (proof)
Theorem 7a51b.. : ∀ x0 x1 : ((ι → ι → ι → ι → ι → ι → ι)(ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι . 884c6.. x0884c6.. x18915b.. x0 = 8915b.. x1x0 = x1 (proof)