Proofgold Signed Transaction

Known Eps_i_ex^Eps_i_R2 : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (Eps_i x0)
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known 7f305..^EmptyAx : not (∀ x0 : ο . (∀ x1 . In x1 0 ⟶ x0) ⟶ x0)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known 06486.. : ∀ x0 x1 : ο . or x0 x1 ⟶ not x0 ⟶ x1
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known fcbcf..^{not_all_ex_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1
Known 35ec9.. : ∀ x0 x1 : ο . not (and x0 x1) ⟶ or (not x0) (not x1)
Known 5f823..^{not_ex_all_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1)
Known 0ff1b.. : ∀ x0 x1 : ο . not (x0 ⟶ x1) ⟶ and x0 (not x1)
Known 91bfe..^dnegI : ∀ x0 : ο . x0 ⟶ not (not x0)
Known bc5df.. : ∀ x0 x1 : ο . (not x0 ⟶ not x1) ⟶ x1 ⟶ x0
Known 0b2fd.. : ∀ x0 x1 : ο . (not x0 ⟶ x1) ⟶ not x1 ⟶ x0
Theorem 50f98.. : ∀ x0 : ο . (∀ x1 . and (∀ x2 . In x2 (binrep (Power (Power (Power (Power 0)))) 0) ⟶ ∀ x3 . In x3 x1 ⟶ ∀ x4 . Subq x4 x3 ⟶ ∀ x5 . ordinal (SNoLev x4)) (∀ x2 . and (∀ x3 : ο . (∀ x4 . and (∀ x5 : ο . (∀ x6 . and (Subq x6 x2) (∀ x7 . Subq x7 x6 ⟶ not (nat_p x4)) ⟶ x5) ⟶ x5) (not (exactly5 x2)) ⟶ x3) ⟶ x3) (exactly5 x2) ⟶ ∀ x3 . In x3 (binrep (Power (Power (Power (Power 0)))) (Power (Power 0))) ⟶ ∀ x4 : ο . (∀ x5 . and (Subq x5 x1) (∀ x6 : ο . (∀ x7 . and (Subq x7 x5) (exactly5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x0) ⟶ x0 (proof)