Proofgold Address

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 ordsucc^ordsucc : ι → ι
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_6^cases_6 : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 x0
Theorem cases_6^cases_6 : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 x0 (proof)
Known In_0_6^In_0_6 : 0 ∈ u6
Theorem In_0_6^In_0_6 : 0 ∈ u6 (proof)
Known In_1_6^In_1_6 : u1 ∈ u6
Theorem In_1_6^In_1_6 : u1 ∈ u6 (proof)
Known In_2_6^In_2_6 : u2 ∈ u6
Theorem In_2_6^In_2_6 : u2 ∈ u6 (proof)
Known In_3_6^In_3_6 : u3 ∈ u6
Theorem In_3_6^In_3_6 : u3 ∈ u6 (proof)
Known In_4_6^In_4_6 : u4 ∈ u6
Theorem In_4_6^In_4_6 : u4 ∈ u6 (proof)
Known In_5_6^In_5_6 : u5 ∈ u6
Theorem In_5_6^In_5_6 : u5 ∈ u6 (proof)
Theorem 17ae2.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ x0 = Church6_to_u6 x2 ⟶ x1) ⟶ x1 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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_eq^tuple_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 x0 ⟶ Church6_to_u6 x0 ∈ u6 (proof)
Theorem 3b8c0.. : ∀ x0 . x0 ∈ u6 ⟶ Church6_p (nth_6_tuple x0) (proof)
Theorem 985a3.. : ∀ x0 . x0 ∈ u6 ⟶ Church6_to_u6 (nth_6_tuple x0) = x0 (proof)
Theorem 60d0e.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ nth_6_tuple x0 = nth_6_tuple x1 ⟶ x0 = x1 (proof)
Theorem 3ac64.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ nth_6_tuple (Church6_to_u6 x0) = x0 (proof)
Theorem b4e23.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ Church6_p x1 ⟶ Church6_to_u6 x0 = Church6_to_u6 x1 ⟶ x0 = 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 x2 ⟶ Church6_p x3 ⟶ x1 (λ x4 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x4 x2 x3)) ⟶ x1 x0
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Known tuple_2_setprod^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Theorem b4e0c.. : ∀ x0 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 884c6.. x0 ⟶ 8915b.. x0 ∈ setprod u6 u6 (proof)
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Theorem b410a.. : ∀ x0 . x0 ∈ setprod u6 u6 ⟶ 884c6.. (4aafd.. x0) (proof)
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Theorem f4bbb.. : ∀ x0 . x0 ∈ setprod u6 u6 ⟶ 8915b.. (4aafd.. x0) = x0 (proof)
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem b98f5.. : ∀ x0 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 884c6.. x0 ⟶ 4aafd.. (8915b.. x0) = x0 (proof)
Theorem 0b928.. : ∀ x0 . x0 ∈ setprod u6 u6 ⟶ ∀ x1 . x1 ∈ setprod u6 u6 ⟶ 4aafd.. x0 = 4aafd.. x1 ⟶ x0 = x1 (proof)
Theorem 7a51b.. : ∀ x0 x1 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 884c6.. x0 ⟶ 884c6.. x1 ⟶ 8915b.. x0 = 8915b.. x1 ⟶ x0 = x1 (proof)