Proofgold Signed Transaction

Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known In_0_5^In_0_5 : 0 ∈ 5
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem tuple_5_0_eq^tuple_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_5^In_1_5 : 1 ∈ 5
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0
Theorem tuple_5_1_eq^tuple_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_5^In_2_5 : 2 ∈ 5
Known neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Theorem tuple_5_2_eq^tuple_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_5^In_3_5 : 3 ∈ 5
Known neq_3_0^neq_3_0 : 3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : 3 = 1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : 3 = 2 ⟶ ∀ x0 : ο . x0
Theorem tuple_5_3_eq^tuple_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_5^In_4_5 : 4 ∈ 5
Known neq_4_0^neq_4_0 : 4 = 0 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : 4 = 1 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : 4 = 2 ⟶ ∀ x0 : ο . x0
Known neq_4_3^neq_4_3 : 4 = 3 ⟶ ∀ x0 : ο . x0
Theorem tuple_5_4_eq^tuple_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_6^In_0_6 : 0 ∈ 6
Theorem 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 (proof)
Known In_1_6^In_1_6 : 1 ∈ 6
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)))))) 1 = x1 (proof)
Known In_2_6^In_2_6 : 2 ∈ 6
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)))))) 2 = x2 (proof)
Known In_3_6^In_3_6 : 3 ∈ 6
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)))))) 3 = x3 (proof)
Known In_4_6^In_4_6 : 4 ∈ 6
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)))))) 4 = x4 (proof)
Known In_5_6^In_5_6 : 5 ∈ 6
Known neq_5_0^neq_5_0 : 5 = 0 ⟶ ∀ x0 : ο . x0
Known neq_5_1^neq_5_1 : 5 = 1 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : 5 = 2 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : 5 = 3 ⟶ ∀ x0 : ο . x0
Known neq_5_4^neq_5_4 : 5 = 4 ⟶ ∀ x0 : ο . x0
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)))))) 5 = x5 (proof)
Known In_0_7^In_0_7 : 0 ∈ 7
Theorem tuple_7_0_eq^tuple_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_7^In_1_7 : 1 ∈ 7
Theorem tuple_7_1_eq^tuple_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_7^In_2_7 : 2 ∈ 7
Theorem tuple_7_2_eq^tuple_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_7^In_3_7 : 3 ∈ 7
Theorem tuple_7_3_eq^tuple_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_7^In_4_7 : 4 ∈ 7
Theorem tuple_7_4_eq^tuple_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_7^In_5_7 : 5 ∈ 7
Theorem tuple_7_5_eq^tuple_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_7^In_6_7 : 6 ∈ 7
Known neq_6_0^neq_6_0 : 6 = 0 ⟶ ∀ x0 : ο . x0
Known neq_6_1^neq_6_1 : 6 = 1 ⟶ ∀ x0 : ο . x0
Known neq_6_2^neq_6_2 : 6 = 2 ⟶ ∀ x0 : ο . x0
Known neq_6_3^neq_6_3 : 6 = 3 ⟶ ∀ x0 : ο . x0
Known neq_6_4^neq_6_4 : 6 = 4 ⟶ ∀ x0 : ο . x0
Known neq_6_5^neq_6_5 : 6 = 5 ⟶ ∀ x0 : ο . x0
Theorem tuple_7_6_eq^tuple_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)