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 c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Known 7f305..^EmptyAx : not (∀ x0 : ο . (∀ x1 . In x1 0 ⟶ x0) ⟶ x0)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known e7295.. : ∀ x0 x1 : ο . x0 = x1 ⟶ and (x0 ⟶ x1) (x1 ⟶ x0)
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 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 5232a.. : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ not x1 ⟶ not x0
Theorem 5f006.. : ∀ x0 . Subq x0 (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) ⟶ ∀ x1 : ο . (∀ x2 . ((∀ x3 : ο . (∀ x4 . and (∀ x5 . SNo_ x0 (binrep (Power (Power (Power (Power 0)))) 0) ⟶ ∀ x6 . not (atleast4 x5)) (∀ x5 . Subq x5 x2 ⟶ ∀ x6 : ο . (∀ x7 . and (In x7 (Inj0 (binrep (Power (Power (Power 0))) 0))) (and ((atleast6 x5 ⟶ not (set_of_pairs x7)) ⟶ and (atleast6 x7) (not (exactly4 x5))) (and (not (exactly2 x7)) (not (Subq 0 x4)))) ⟶ x6) ⟶ x6) ⟶ x3) ⟶ x3) ⟶ ∀ x3 : ο . (∀ x4 . and (Subq x4 (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0)) (ordinal 0) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)