Proofgold Signed Transaction

Param ordsucc^ordsucc : ι → ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known In_0_9^In_0_9 : 0 ∈ 9
Theorem d4e95.. : 0 ∈ 10 (proof)
Known In_1_9^In_1_9 : 1 ∈ 9
Theorem b7a5e.. : 1 ∈ 10 (proof)
Known In_2_9^In_2_9 : 2 ∈ 9
Theorem 3c603.. : 2 ∈ 10 (proof)
Known In_3_9^In_3_9 : 3 ∈ 9
Theorem 01826.. : 3 ∈ 10 (proof)
Known In_4_9^In_4_9 : 4 ∈ 9
Theorem 35ffd.. : 4 ∈ 10 (proof)
Known In_5_9^In_5_9 : 5 ∈ 9
Theorem a1b2a.. : 5 ∈ 10 (proof)
Known In_6_9^In_6_9 : 6 ∈ 9
Theorem 1beb5.. : 6 ∈ 10 (proof)
Known In_7_9^In_7_9 : 7 ∈ 9
Theorem 16542.. : 7 ∈ 10 (proof)
Known In_8_9^In_8_9 : 8 ∈ 9
Theorem 56b84.. : 8 ∈ 10 (proof)
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem fa1e6.. : 9 ∈ 10 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 3105e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 0 = x0 (proof)
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 f0027.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 1 = x1 (proof)
Known neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Theorem 71234.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 2 = x2 (proof)
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 cb998.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 3 = x3 (proof)
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 bd5cb.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 4 = x4 (proof)
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 11217.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 5 = x5 (proof)
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 bc2b8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 6 = x6 (proof)
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 c16dd.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 7 = x7 (proof)
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 0f630.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 8 = x8 (proof)
Known neq_9_0^neq_9_0 : 9 = 0 ⟶ ∀ x0 : ο . x0
Known neq_9_1^neq_9_1 : 9 = 1 ⟶ ∀ x0 : ο . x0
Known neq_9_2^neq_9_2 : 9 = 2 ⟶ ∀ x0 : ο . x0
Known neq_9_3^neq_9_3 : 9 = 3 ⟶ ∀ x0 : ο . x0
Known neq_9_4^neq_9_4 : 9 = 4 ⟶ ∀ x0 : ο . x0
Known neq_9_5^neq_9_5 : 9 = 5 ⟶ ∀ x0 : ο . x0
Known neq_9_6^neq_9_6 : 9 = 6 ⟶ ∀ x0 : ο . x0
Known neq_9_7^neq_9_7 : 9 = 7 ⟶ ∀ x0 : ο . x0
Known neq_9_8^neq_9_8 : 9 = 8 ⟶ ∀ x0 : ο . x0
Theorem 06839.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (lam 10 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 (If_i (x11 = 4) x4 (If_i (x11 = 5) x5 (If_i (x11 = 6) x6 (If_i (x11 = 7) x7 (If_i (x11 = 8) x8 x9)))))))))) 9 = x9 (proof)
Definition 4a740.. := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . lam 10 (λ 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 (If_i (x10 = 8) x8 x9)))))))))
Theorem 1d6af.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 0 = x0 (proof)
Theorem ada9b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 1 = x1 (proof)
Theorem 5b3bf.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 2 = x2 (proof)
Theorem 7684e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 3 = x3 (proof)
Theorem 601d3.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 4 = x4 (proof)
Theorem f536c.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 5 = x5 (proof)
Theorem 6a688.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 6 = x6 (proof)
Theorem 83113.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 7 = x7 (proof)
Theorem 1d841.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 8 = x8 (proof)
Theorem d7ed7.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (4a740.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) 9 = x9 (proof)