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_8^In_0_8 : 0 ∈ 8
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem tuple_8_0_eq^tuple_8_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 0 = x0 (proof)
Known In_1_8^In_1_8 : 1 ∈ 8
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_8_1_eq^tuple_8_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 1 = x1 (proof)
Known In_2_8^In_2_8 : 2 ∈ 8
Known neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Theorem tuple_8_2_eq^tuple_8_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 2 = x2 (proof)
Known In_3_8^In_3_8 : 3 ∈ 8
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_8_3_eq^tuple_8_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 3 = x3 (proof)
Known In_4_8^In_4_8 : 4 ∈ 8
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_8_4_eq^tuple_8_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 4 = x4 (proof)
Known In_5_8^In_5_8 : 5 ∈ 8
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_8_5_eq^tuple_8_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 5 = x5 (proof)
Known In_6_8^In_6_8 : 6 ∈ 8
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_8_6_eq^tuple_8_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 6 = x6 (proof)
Known In_7_8^In_7_8 : 7 ∈ 8
Known neq_7_0^neq_7_0 : 7 = 0 ⟶ ∀ x0 : ο . x0
Known neq_7_1^neq_7_1 : 7 = 1 ⟶ ∀ x0 : ο . x0
Known neq_7_2^neq_7_2 : 7 = 2 ⟶ ∀ x0 : ο . x0
Known neq_7_3^neq_7_3 : 7 = 3 ⟶ ∀ x0 : ο . x0
Known neq_7_4^neq_7_4 : 7 = 4 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : 7 = 5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : 7 = 6 ⟶ ∀ x0 : ο . x0
Theorem tuple_8_7_eq^tuple_8_7_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 7 = x7 (proof)
Known In_0_9^In_0_9 : 0 ∈ 9
Theorem tuple_9_0_eq^tuple_9_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 0 = x0 (proof)
Known In_1_9^In_1_9 : 1 ∈ 9
Theorem tuple_9_1_eq^tuple_9_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 1 = x1 (proof)
Known In_2_9^In_2_9 : 2 ∈ 9
Theorem tuple_9_2_eq^tuple_9_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 2 = x2 (proof)
Known In_3_9^In_3_9 : 3 ∈ 9
Theorem tuple_9_3_eq^tuple_9_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 3 = x3 (proof)
Known In_4_9^In_4_9 : 4 ∈ 9
Theorem tuple_9_4_eq^tuple_9_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 4 = x4 (proof)
Known In_5_9^In_5_9 : 5 ∈ 9
Theorem tuple_9_5_eq^tuple_9_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 5 = x5 (proof)
Known In_6_9^In_6_9 : 6 ∈ 9
Theorem tuple_9_6_eq^tuple_9_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 6 = x6 (proof)
Known In_7_9^In_7_9 : 7 ∈ 9
Theorem tuple_9_7_eq^tuple_9_7_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 7 = x7 (proof)
Known In_8_9^In_8_9 : 8 ∈ 9
Known neq_8_0^neq_8_0 : 8 = 0 ⟶ ∀ x0 : ο . x0
Known neq_8_1^neq_8_1 : 8 = 1 ⟶ ∀ x0 : ο . x0
Known neq_8_2^neq_8_2 : 8 = 2 ⟶ ∀ x0 : ο . x0
Known neq_8_3^neq_8_3 : 8 = 3 ⟶ ∀ x0 : ο . x0
Known neq_8_4^neq_8_4 : 8 = 4 ⟶ ∀ x0 : ο . x0
Known neq_8_5^neq_8_5 : 8 = 5 ⟶ ∀ x0 : ο . x0
Known neq_8_6^neq_8_6 : 8 = 6 ⟶ ∀ x0 : ο . x0
Known neq_8_7^neq_8_7 : 8 = 7 ⟶ ∀ x0 : ο . x0
Theorem tuple_9_8_eq^tuple_9_8_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 8 = x8 (proof)