Proofgold Signed Transaction

Known df_coels__df_rels__df_ssr__df_refs__df_refrels__df_refrel__df_cnvrefs__df_cnvrefrels__df_cnvrefrel__df_syms__df_symrels__df_symrel__df_prt__ax_c5__ax_c4__ax_c7__ax_c10__ax_c10_b : ∀ x0 : ο . ((∀ x1 : ι → ο . wceq (ccoels x1) (ccoss (cres (ccnv cep) x1))) ⟶ wceq crels (cpw (cxp cvv cvv)) ⟶ wceq cssr (copab (λ x1 x2 . wss (cv x1) (cv x2))) ⟶ wceq crefs (cab (λ x1 . wbr (cin cid (cxp (cdm (cv x1)) (crn (cv x1)))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) cssr)) ⟶ wceq crefrels (cin crefs crels) ⟶ (∀ x1 : ι → ο . wb (wrefrel x1) (wa (wss (cin cid (cxp (cdm x1) (crn x1))) (cin x1 (cxp (cdm x1) (crn x1)))) (wrel x1))) ⟶ wceq ccnvrefs (cab (λ x1 . wbr (cin cid (cxp (cdm (cv x1)) (crn (cv x1)))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) (ccnv cssr))) ⟶ wceq ccnvrefrels (cin ccnvrefs crels) ⟶ (∀ x1 : ι → ο . wb (wcnvrefrel x1) (wa (wss (cin x1 (cxp (cdm x1) (crn x1))) (cin cid (cxp (cdm x1) (crn x1)))) (wrel x1))) ⟶ wceq csyms (cab (λ x1 . wbr (ccnv (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1))))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) cssr)) ⟶ wceq csymrels (cin csyms crels) ⟶ (∀ x1 : ι → ο . wb (wsymrel x1) (wa (wss (ccnv (cin x1 (cxp (cdm x1) (crn x1)))) (cin x1 (cxp (cdm x1) (crn x1)))) (wrel x1))) ⟶ (∀ x1 : ι → ο . wb (wprt x1) (wral (λ x2 . wral (λ x3 . wo (wceq (cv x2) (cv x3)) (wceq (cin (cv x2) (cv x3)) c0)) (λ x3 . x1)) (λ x2 . x1))) ⟶ (∀ x1 : ι → ο . ∀ x2 . (∀ x3 . x1 x3) ⟶ x1 x2) ⟶ (∀ x1 x2 : ι → ο . (∀ x3 . (∀ x4 . x1 x4) ⟶ x2 x3) ⟶ (∀ x3 . x1 x3) ⟶ ∀ x3 . x2 x3) ⟶ (∀ x1 : ι → ο . ∀ x2 . wn (∀ x3 . wn (∀ x4 . x1 x4)) ⟶ x1 x2) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . (∀ x4 . wceq (cv x4) (cv x2) ⟶ ∀ x5 . x1 x5) ⟶ x1 x3) ⟶ (∀ x1 : ι → ο . ∀ x2 . (∀ x3 . wceq (cv x3) (cv x3) ⟶ ∀ x4 . x1 x4) ⟶ x1 x2) ⟶ x0) ⟶ x0
Theorem df_coels : ∀ x0 : ι → ο . wceq (ccoels x0) (ccoss (cres (ccnv cep) x0)) (proof)
Theorem df_rels : wceq crels (cpw (cxp cvv cvv)) (proof)
Theorem df_ssr : wceq cssr (copab (λ x0 x1 . wss (cv x0) (cv x1))) (proof)
Theorem df_refs : wceq crefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)) (proof)
Theorem df_refrels : wceq crefrels (cin crefs crels) (proof)
Theorem df_refrel : ∀ x0 : ι → ο . wb (wrefrel x0) (wa (wss (cin cid (cxp (cdm x0) (crn x0))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_cnvrefs : wceq ccnvrefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) (ccnv cssr))) (proof)
Theorem df_cnvrefrels : wceq ccnvrefrels (cin ccnvrefs crels) (proof)
Theorem df_cnvrefrel : ∀ x0 : ι → ο . wb (wcnvrefrel x0) (wa (wss (cin x0 (cxp (cdm x0) (crn x0))) (cin cid (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_syms : wceq csyms (cab (λ x0 . wbr (ccnv (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0))))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)) (proof)
Theorem df_symrels : wceq csymrels (cin csyms crels) (proof)
Theorem df_symrel : ∀ x0 : ι → ο . wb (wsymrel x0) (wa (wss (ccnv (cin x0 (cxp (cdm x0) (crn x0)))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_prt : ∀ x0 : ι → ο . wb (wprt x0) (wral (λ x1 . wral (λ x2 . wo (wceq (cv x1) (cv x2)) (wceq (cin (cv x1) (cv x2)) c0)) (λ x2 . x0)) (λ x1 . x0)) (proof)
Theorem ax_c5 : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ x0 x1 (proof)
Theorem ax_c4 : ∀ x0 x1 : ι → ο . (∀ x2 . (∀ x3 . x0 x3) ⟶ x1 x2) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . x1 x2 (proof)
Theorem ax_c7 : ∀ x0 : ι → ο . ∀ x1 . wn (∀ x2 . wn (∀ x3 . x0 x3)) ⟶ x0 x1 (proof)
Theorem ax_c10 : ∀ x0 : ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x1) ⟶ ∀ x4 . x0 x4) ⟶ x0 x2 (proof)
Theorem ax_c10_b : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . wceq (cv x2) (cv x2) ⟶ ∀ x3 . x0 x3) ⟶ x0 x1 (proof)