Proofgold Signed Transaction

Known df_ec__df_qs__df_map__df_pm__df_ixp__df_en__df_dom__df_sdom__df_fin__df_fsupp__df_fi__df_sup__df_inf__df_oi__df_har__df_wdom__ax_reg__ax_inf : ∀ x0 : ο . ((∀ x1 x2 : ι → ο . wceq (cec x1 x2) (cima x2 (csn x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (cqs x1 x2) (cab (λ x3 . wrex (λ x4 . wceq (cv x3) (cec (cv x4) x2)) (λ x4 . x1)))) ⟶ wceq cmap (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cab (λ x3 . wf (cv x2) (cv x1) (cv x3)))) ⟶ wceq cpm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wfun (cv x3)) (λ x3 . cpw (cxp (cv x2) (cv x1))))) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (cixp x1 x2) (cab (λ x3 . wa (wfn (cv x3) (cab (λ x4 . wcel (cv x4) (x1 x4)))) (wral (λ x4 . wcel (cfv (cv x4) (cv x3)) (x2 x4)) x1)))) ⟶ wceq cen (copab (λ x1 x2 . wex (λ x3 . wf1o (cv x1) (cv x2) (cv x3)))) ⟶ wceq cdom (copab (λ x1 x2 . wex (λ x3 . wf1 (cv x1) (cv x2) (cv x3)))) ⟶ wceq csdm (cdif cdom cen) ⟶ wceq cfn (cab (λ x1 . wrex (λ x2 . wbr (cv x1) (cv x2) cen) (λ x2 . com))) ⟶ wceq cfsupp (copab (λ x1 x2 . wa (wfun (cv x1)) (wcel (co (cv x1) (cv x2) csupp) cfn))) ⟶ wceq cfi (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wceq (cv x2) (cint (cv x3))) (λ x3 . cin (cpw (cv x1)) cfn)))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (csup x1 x2 x3) (cuni (crab (λ x4 . wa (wral (λ x5 . wn (wbr (cv x4) (cv x5) x3)) (λ x5 . x1)) (wral (λ x5 . wbr (cv x5) (cv x4) x3 ⟶ wrex (λ x6 . wbr (cv x5) (cv x6) x3) (λ x6 . x1)) (λ x5 . x2))) (λ x4 . x2)))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cinf x1 x2 x3) (csup x1 x2 (ccnv x3))) ⟶ (∀ x1 x2 : ι → ο . wceq (coi x1 x2) (cif (wa (wwe x1 x2) (wse x1 x2)) (cres (crecs (cmpt (λ x3 . cvv) (λ x3 . crio (λ x4 . wral (λ x5 . wn (wbr (cv x5) (cv x4) x2)) (λ x5 . crab (λ x6 . wral (λ x7 . wbr (cv x7) (cv x6) x2) (λ x7 . crn (cv x3))) (λ x6 . x1))) (λ x4 . crab (λ x5 . wral (λ x6 . wbr (cv x6) (cv x5) x2) (λ x6 . crn (cv x3))) (λ x5 . x1))))) (crab (λ x3 . wrex (λ x4 . wral (λ x5 . wbr (cv x5) (cv x4) x2) (λ x5 . cima (crecs (cmpt (λ x6 . cvv) (λ x6 . crio (λ x7 . wral (λ x8 . wn (wbr (cv x8) (cv x7) x2)) (λ x8 . crab (λ x9 . wral (λ x10 . wbr (cv x10) (cv x9) x2) (λ x10 . crn (cv x6))) (λ x9 . x1))) (λ x7 . crab (λ x8 . wral (λ x9 . wbr (cv x9) (cv x8) x2) (λ x9 . crn (cv x6))) (λ x8 . x1))))) (cv x3))) (λ x4 . x1)) (λ x3 . con0))) c0)) ⟶ wceq char (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cv x1) cdom) (λ x2 . con0))) ⟶ wceq cwdom (copab (λ x1 x2 . wo (wceq (cv x1) c0) (wex (λ x3 . wfo (cv x2) (cv x1) (cv x3))))) ⟶ (∀ x1 . wex (λ x2 . wcel (cv x2) (cv x1)) ⟶ wex (λ x2 . wa (wcel (cv x2) (cv x1)) (∀ x3 . wcel (cv x3) (cv x2) ⟶ wn (wcel (cv x3) (cv x1))))) ⟶ (∀ x1 . wex (λ x2 . wa (wcel (cv x1) (cv x2)) (∀ x3 . wcel (cv x3) (cv x2) ⟶ wex (λ x4 . wa (wcel (cv x3) (cv x4)) (wcel (cv x4) (cv x2)))))) ⟶ x0) ⟶ x0
Theorem df_ec : ∀ x0 x1 : ι → ο . wceq (cec x0 x1) (cima x1 (csn x0)) (proof)
Theorem df_qs : ∀ x0 x1 : ι → ο . wceq (cqs x0 x1) (cab (λ x2 . wrex (λ x3 . wceq (cv x2) (cec (cv x3) x1)) (λ x3 . x0))) (proof)
Theorem df_map : wceq cmap (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cab (λ x2 . wf (cv x1) (cv x0) (cv x2)))) (proof)
Theorem df_pm : wceq cpm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wfun (cv x2)) (λ x2 . cpw (cxp (cv x1) (cv x0))))) (proof)
Theorem df_ixp : ∀ x0 x1 : ι → ι → ο . wceq (cixp x0 x1) (cab (λ x2 . wa (wfn (cv x2) (cab (λ x3 . wcel (cv x3) (x0 x3)))) (wral (λ x3 . wcel (cfv (cv x3) (cv x2)) (x1 x3)) x0))) (proof)
Theorem df_en : wceq cen (copab (λ x0 x1 . wex (λ x2 . wf1o (cv x0) (cv x1) (cv x2)))) (proof)
Theorem df_dom : wceq cdom (copab (λ x0 x1 . wex (λ x2 . wf1 (cv x0) (cv x1) (cv x2)))) (proof)
Theorem df_sdom : wceq csdm (cdif cdom cen) (proof)
Theorem df_fin : wceq cfn (cab (λ x0 . wrex (λ x1 . wbr (cv x0) (cv x1) cen) (λ x1 . com))) (proof)
Theorem df_fsupp : wceq cfsupp (copab (λ x0 x1 . wa (wfun (cv x0)) (wcel (co (cv x0) (cv x1) csupp) cfn))) (proof)
Theorem df_fi : wceq cfi (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wrex (λ x2 . wceq (cv x1) (cint (cv x2))) (λ x2 . cin (cpw (cv x0)) cfn)))) (proof)
Theorem df_sup : ∀ x0 x1 x2 : ι → ο . wceq (csup x0 x1 x2) (cuni (crab (λ x3 . wa (wral (λ x4 . wn (wbr (cv x3) (cv x4) x2)) (λ x4 . x0)) (wral (λ x4 . wbr (cv x4) (cv x3) x2 ⟶ wrex (λ x5 . wbr (cv x4) (cv x5) x2) (λ x5 . x0)) (λ x4 . x1))) (λ x3 . x1))) (proof)
Theorem df_inf : ∀ x0 x1 x2 : ι → ο . wceq (cinf x0 x1 x2) (csup x0 x1 (ccnv x2)) (proof)
Theorem df_oi : ∀ x0 x1 : ι → ο . wceq (coi x0 x1) (cif (wa (wwe x0 x1) (wse x0 x1)) (cres (crecs (cmpt (λ x2 . cvv) (λ x2 . crio (λ x3 . wral (λ x4 . wn (wbr (cv x4) (cv x3) x1)) (λ x4 . crab (λ x5 . wral (λ x6 . wbr (cv x6) (cv x5) x1) (λ x6 . crn (cv x2))) (λ x5 . x0))) (λ x3 . crab (λ x4 . wral (λ x5 . wbr (cv x5) (cv x4) x1) (λ x5 . crn (cv x2))) (λ x4 . x0))))) (crab (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cv x4) (cv x3) x1) (λ x4 . cima (crecs (cmpt (λ x5 . cvv) (λ x5 . crio (λ x6 . wral (λ x7 . wn (wbr (cv x7) (cv x6) x1)) (λ x7 . crab (λ x8 . wral (λ x9 . wbr (cv x9) (cv x8) x1) (λ x9 . crn (cv x5))) (λ x8 . x0))) (λ x6 . crab (λ x7 . wral (λ x8 . wbr (cv x8) (cv x7) x1) (λ x8 . crn (cv x5))) (λ x7 . x0))))) (cv x2))) (λ x3 . x0)) (λ x2 . con0))) c0) (proof)
Theorem df_har : wceq char (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cv x0) cdom) (λ x1 . con0))) (proof)
Theorem df_wdom : wceq cwdom (copab (λ x0 x1 . wo (wceq (cv x0) c0) (wex (λ x2 . wfo (cv x1) (cv x0) (cv x2))))) (proof)
Theorem ax_reg : ∀ x0 . wex (λ x1 . wcel (cv x1) (cv x0)) ⟶ wex (λ x1 . wa (wcel (cv x1) (cv x0)) (∀ x2 . wcel (cv x2) (cv x1) ⟶ wn (wcel (cv x2) (cv x0)))) (proof)
Theorem ax_inf : ∀ x0 . wex (λ x1 . wa (wcel (cv x0) (cv x1)) (∀ x2 . wcel (cv x2) (cv x1) ⟶ wex (λ x3 . wa (wcel (cv x2) (cv x3)) (wcel (cv x3) (cv x1))))) (proof)