Proofgold Signed Transaction

Known df_fr__df_se__df_we__df_xp__df_rel__df_cnv__df_co__df_dm__df_rn__df_res__df_ima__df_pred__df_ord__df_on__df_lim__df_suc__df_iota__df_fun : ∀ x0 : ο . ((∀ x1 x2 : ι → ο . wb (wfr x1 x2) (∀ x3 . wa (wss (cv x3) x1) (wne (cv x3) c0) ⟶ wrex (λ x4 . wral (λ x5 . wn (wbr (cv x5) (cv x4) x2)) (λ x5 . cv x3)) (λ x4 . cv x3))) ⟶ (∀ x1 x2 : ι → ο . wb (wse x1 x2) (wral (λ x3 . wcel (crab (λ x4 . wbr (cv x4) (cv x3) x2) (λ x4 . x1)) cvv) (λ x3 . x1))) ⟶ (∀ x1 x2 : ι → ο . wb (wwe x1 x2) (wa (wfr x1 x2) (wor x1 x2))) ⟶ (∀ x1 x2 : ι → ο . wceq (cxp x1 x2) (copab (λ x3 x4 . wa (wcel (cv x3) x1) (wcel (cv x4) x2)))) ⟶ (∀ x1 : ι → ο . wb (wrel x1) (wss x1 (cxp cvv cvv))) ⟶ (∀ x1 : ι → ο . wceq (ccnv x1) (copab (λ x2 x3 . wbr (cv x3) (cv x2) x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (ccom x1 x2) (copab (λ x3 x4 . wex (λ x5 . wa (wbr (cv x3) (cv x5) x2) (wbr (cv x5) (cv x4) x1))))) ⟶ (∀ x1 : ι → ο . wceq (cdm x1) (cab (λ x2 . wex (λ x3 . wbr (cv x2) (cv x3) x1)))) ⟶ (∀ x1 : ι → ο . wceq (crn x1) (cdm (ccnv x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (cres x1 x2) (cin x1 (cxp x2 cvv))) ⟶ (∀ x1 x2 : ι → ο . wceq (cima x1 x2) (crn (cres x1 x2))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cpred x1 x2 x3) (cin x1 (cima (ccnv x2) (csn x3)))) ⟶ (∀ x1 : ι → ο . wb (word x1) (wa (wtr x1) (wwe x1 cep))) ⟶ wceq con0 (cab (λ x1 . word (cv x1))) ⟶ (∀ x1 : ι → ο . wb (wlim x1) (w3a (word x1) (wne x1 c0) (wceq x1 (cuni x1)))) ⟶ (∀ x1 : ι → ο . wceq (csuc x1) (cun x1 (csn x1))) ⟶ (∀ x1 : ι → ο . wceq (cio x1) (cuni (cab (λ x2 . wceq (cab x1) (csn (cv x2)))))) ⟶ (∀ x1 : ι → ο . wb (wfun x1) (wa (wrel x1) (wss (ccom x1 (ccnv x1)) cid))) ⟶ x0) ⟶ x0
Theorem df_fr : ∀ x0 x1 : ι → ο . wb (wfr x0 x1) (∀ x2 . wa (wss (cv x2) x0) (wne (cv x2) c0) ⟶ wrex (λ x3 . wral (λ x4 . wn (wbr (cv x4) (cv x3) x1)) (λ x4 . cv x2)) (λ x3 . cv x2)) (proof)
Theorem df_se : ∀ x0 x1 : ι → ο . wb (wse x0 x1) (wral (λ x2 . wcel (crab (λ x3 . wbr (cv x3) (cv x2) x1) (λ x3 . x0)) cvv) (λ x2 . x0)) (proof)
Theorem df_we : ∀ x0 x1 : ι → ο . wb (wwe x0 x1) (wa (wfr x0 x1) (wor x0 x1)) (proof)
Theorem df_xp : ∀ x0 x1 : ι → ο . wceq (cxp x0 x1) (copab (λ x2 x3 . wa (wcel (cv x2) x0) (wcel (cv x3) x1))) (proof)
Theorem df_rel : ∀ x0 : ι → ο . wb (wrel x0) (wss x0 (cxp cvv cvv)) (proof)
Theorem df_cnv : ∀ x0 : ι → ο . wceq (ccnv x0) (copab (λ x1 x2 . wbr (cv x2) (cv x1) x0)) (proof)
Theorem df_co : ∀ x0 x1 : ι → ο . wceq (ccom x0 x1) (copab (λ x2 x3 . wex (λ x4 . wa (wbr (cv x2) (cv x4) x1) (wbr (cv x4) (cv x3) x0)))) (proof)
Theorem df_dm : ∀ x0 : ι → ο . wceq (cdm x0) (cab (λ x1 . wex (λ x2 . wbr (cv x1) (cv x2) x0))) (proof)
Theorem df_rn : ∀ x0 : ι → ο . wceq (crn x0) (cdm (ccnv x0)) (proof)
Theorem df_res : ∀ x0 x1 : ι → ο . wceq (cres x0 x1) (cin x0 (cxp x1 cvv)) (proof)
Theorem df_ima : ∀ x0 x1 : ι → ο . wceq (cima x0 x1) (crn (cres x0 x1)) (proof)
Theorem df_pred : ∀ x0 x1 x2 : ι → ο . wceq (cpred x0 x1 x2) (cin x0 (cima (ccnv x1) (csn x2))) (proof)
Theorem df_ord : ∀ x0 : ι → ο . wb (word x0) (wa (wtr x0) (wwe x0 cep)) (proof)
Theorem df_on : wceq con0 (cab (λ x0 . word (cv x0))) (proof)
Theorem df_lim : ∀ x0 : ι → ο . wb (wlim x0) (w3a (word x0) (wne x0 c0) (wceq x0 (cuni x0))) (proof)
Theorem df_suc : ∀ x0 : ι → ο . wceq (csuc x0) (cun x0 (csn x0)) (proof)
Theorem df_iota : ∀ x0 : ι → ο . wceq (cio x0) (cuni (cab (λ x1 . wceq (cab x0) (csn (cv x1))))) (proof)
Theorem df_fun : ∀ x0 : ι → ο . wb (wfun x0) (wa (wrel x0) (wss (ccom x0 (ccnv x0)) cid)) (proof)