Proofgold Signed Transaction

Known df_bigo__df_blen__df_dig__df_setrecs__df_pg__df_gte__df_gt__df_sinh__df_cosh__df_tanh__df_sec__df_csc__df_cot__df_logbALT__df_reflexive__df_irreflexive__df_alsi__df_alsc : ∀ x0 : ο . (wceq cbigo (cmpt (λ x1 . co cr cr cpm) (λ x1 . crab (λ x2 . wrex (λ x3 . wrex (λ x4 . wral (λ x5 . wbr (cfv (cv x5) (cv x2)) (co (cv x4) (cfv (cv x5) (cv x1)) cmul) cle) (λ x5 . cin (cdm (cv x2)) (co (cv x3) cpnf cico))) (λ x4 . cr)) (λ x3 . cr)) (λ x2 . co cr cr cpm))) ⟶ wceq cblen (cmpt (λ x1 . cvv) (λ x1 . cif (wceq (cv x1) cc0) c1 (co (cfv (co c2 (cfv (cv x1) cabs) clogb) cfl) c1 caddc))) ⟶ wceq cdig (cmpt (λ x1 . cn) (λ x1 . cmpt2 (λ x2 x3 . cz) (λ x2 x3 . co cc0 cpnf cico) (λ x2 x3 . co (cfv (co (co (cv x1) (cneg (cv x2)) cexp) (cv x3) cmul) cfl) (cv x1) cmo))) ⟶ (∀ x1 : ι → ο . wceq (csetrecs x1) (cuni (cab (λ x2 . ∀ x3 . (∀ x4 . wss (cv x4) (cv x2) ⟶ wss (cv x4) (cv x3) ⟶ wss (cfv (cv x4) x1) (cv x3)) ⟶ wss (cv x2) (cv x3))))) ⟶ wceq cpg (csetrecs (cmpt (λ x1 . cvv) (λ x1 . cxp (cpw (cv x1)) (cpw (cv x1))))) ⟶ wceq cge_real (ccnv cle) ⟶ wceq cgt (ccnv clt) ⟶ wceq csinh (cmpt (λ x1 . cc) (λ x1 . co (cfv (co ci (cv x1) cmul) csin) ci cdiv)) ⟶ wceq ccosh (cmpt (λ x1 . cc) (λ x1 . cfv (co ci (cv x1) cmul) ccos)) ⟶ wceq ctanh (cmpt (λ x1 . cima (ccnv ccosh) (cdif cc (csn cc0))) (λ x1 . co (cfv (co ci (cv x1) cmul) ctan) ci cdiv)) ⟶ wceq csec (cmpt (λ x1 . crab (λ x2 . wne (cfv (cv x2) ccos) cc0) (λ x2 . cc)) (λ x1 . co c1 (cfv (cv x1) ccos) cdiv)) ⟶ wceq ccsc (cmpt (λ x1 . crab (λ x2 . wne (cfv (cv x2) csin) cc0) (λ x2 . cc)) (λ x1 . co c1 (cfv (cv x1) csin) cdiv)) ⟶ wceq ccot (cmpt (λ x1 . crab (λ x2 . wne (cfv (cv x2) csin) cc0) (λ x2 . cc)) (λ x1 . co (cfv (cv x1) ccos) (cfv (cv x1) csin) cdiv)) ⟶ wceq clog_ (cmpt (λ x1 . cdif cc (cpr cc0 c1)) (λ x1 . cmpt (λ x2 . cdif cc (csn cc0)) (λ x2 . co (cfv (cv x2) clog) (cfv (cv x1) clog) cdiv))) ⟶ (∀ x1 x2 : ι → ο . wb (wreflexive x1 x2) (wa (wss x2 (cxp x1 x1)) (wral (λ x3 . wbr (cv x3) (cv x3) x2) (λ x3 . x1)))) ⟶ (∀ x1 x2 : ι → ο . wb (wirreflexive x1 x2) (wa (wss x2 (cxp x1 x1)) (wral (λ x3 . wn (wbr (cv x3) (cv x3) x2)) (λ x3 . x1)))) ⟶ (∀ x1 x2 : ι → ο . wb (walsi x1 x2) (wa (∀ x3 . x1 x3 ⟶ x2 x3) (wex x1))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (walsc x1 x2) (wa (wral x1 x2) (wex (λ x3 . wcel (cv x3) (x2 x3))))) ⟶ x0) ⟶ x0
Theorem df_bigo : wceq cbigo (cmpt (λ x0 . co cr cr cpm) (λ x0 . crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (cv x4) (cv x1)) (co (cv x3) (cfv (cv x4) (cv x0)) cmul) cle) (λ x4 . cin (cdm (cv x1)) (co (cv x2) cpnf cico))) (λ x3 . cr)) (λ x2 . cr)) (λ x1 . co cr cr cpm))) (proof)
Theorem df_blen : wceq cblen (cmpt (λ x0 . cvv) (λ x0 . cif (wceq (cv x0) cc0) c1 (co (cfv (co c2 (cfv (cv x0) cabs) clogb) cfl) c1 caddc))) (proof)
Theorem df_dig : wceq cdig (cmpt (λ x0 . cn) (λ x0 . cmpt2 (λ x1 x2 . cz) (λ x1 x2 . co cc0 cpnf cico) (λ x1 x2 . co (cfv (co (co (cv x0) (cneg (cv x1)) cexp) (cv x2) cmul) cfl) (cv x0) cmo))) (proof)
Theorem df_setrecs : ∀ x0 : ι → ο . wceq (csetrecs x0) (cuni (cab (λ x1 . ∀ x2 . (∀ x3 . wss (cv x3) (cv x1) ⟶ wss (cv x3) (cv x2) ⟶ wss (cfv (cv x3) x0) (cv x2)) ⟶ wss (cv x1) (cv x2)))) (proof)
Theorem df_pg : wceq cpg (csetrecs (cmpt (λ x0 . cvv) (λ x0 . cxp (cpw (cv x0)) (cpw (cv x0))))) (proof)
Theorem df_gte : wceq cge_real (ccnv cle) (proof)
Theorem df_gt : wceq cgt (ccnv clt) (proof)
Theorem df_sinh : wceq csinh (cmpt (λ x0 . cc) (λ x0 . co (cfv (co ci (cv x0) cmul) csin) ci cdiv)) (proof)
Theorem df_cosh : wceq ccosh (cmpt (λ x0 . cc) (λ x0 . cfv (co ci (cv x0) cmul) ccos)) (proof)
Theorem df_tanh : wceq ctanh (cmpt (λ x0 . cima (ccnv ccosh) (cdif cc (csn cc0))) (λ x0 . co (cfv (co ci (cv x0) cmul) ctan) ci cdiv)) (proof)
Theorem df_sec : wceq csec (cmpt (λ x0 . crab (λ x1 . wne (cfv (cv x1) ccos) cc0) (λ x1 . cc)) (λ x0 . co c1 (cfv (cv x0) ccos) cdiv)) (proof)
Theorem df_csc : wceq ccsc (cmpt (λ x0 . crab (λ x1 . wne (cfv (cv x1) csin) cc0) (λ x1 . cc)) (λ x0 . co c1 (cfv (cv x0) csin) cdiv)) (proof)
Theorem df_cot : wceq ccot (cmpt (λ x0 . crab (λ x1 . wne (cfv (cv x1) csin) cc0) (λ x1 . cc)) (λ x0 . co (cfv (cv x0) ccos) (cfv (cv x0) csin) cdiv)) (proof)
Theorem df_logbALT : wceq clog_ (cmpt (λ x0 . cdif cc (cpr cc0 c1)) (λ x0 . cmpt (λ x1 . cdif cc (csn cc0)) (λ x1 . co (cfv (cv x1) clog) (cfv (cv x0) clog) cdiv))) (proof)
Theorem df_reflexive : ∀ x0 x1 : ι → ο . wb (wreflexive x0 x1) (wa (wss x1 (cxp x0 x0)) (wral (λ x2 . wbr (cv x2) (cv x2) x1) (λ x2 . x0))) (proof)
Theorem df_irreflexive : ∀ x0 x1 : ι → ο . wb (wirreflexive x0 x1) (wa (wss x1 (cxp x0 x0)) (wral (λ x2 . wn (wbr (cv x2) (cv x2) x1)) (λ x2 . x0))) (proof)
Theorem df_alsi : ∀ x0 x1 : ι → ο . wb (walsi x0 x1) (wa (∀ x2 . x0 x2 ⟶ x1 x2) (wex x0)) (proof)
Theorem df_alsc : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (walsc x0 x1) (wa (wral x0 x1) (wex (λ x2 . wcel (cv x2) (x1 x2)))) (proof)