Proofgold Signed Transaction

Param c2e41.. : ι → ι → ο
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param e5b72.. : ι → ι
Param 1216a.. : ι → (ι → ο) → ι
Param f482f.. : ι → ι → ι
Param and : ο → ο → ο
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known c6ad4.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ c2e41.. x0 x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0)
Known 6e275.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ f482f.. x2 x4 = f482f.. x3 x4) ⟶ x2 = x3
Known 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known c8c18.. : 4a7ef.. = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Known d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)
Param 0fc90.. : ι → (ι → ι) → ι
Param If_i : ο → ι → ι → ι
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known 492ff.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ ∀ x3 : ο . (prim1 x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0
Theorem ba265.. : ∀ x0 . c2e41.. (b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0) (e5b72.. x0) (proof)