Proofgold Signed Transaction

Known df_sslt__df_scut__df_made__df_old__df_new__df_left__df_right__df_txp__df_pprod__df_sset__df_trans__df_bigcup__df_fix__df_limits__df_funs__df_singleton__df_singles__df_image : ∀ x0 : ο . (wceq csslt (copab (λ x1 x2 . w3a (wss (cv x1) csur) (wss (cv x2) csur) (wral (λ x3 . wral (λ x4 . wbr (cv x3) (cv x4) cslt) (λ x4 . cv x2)) (λ x3 . cv x1)))) ⟶ wceq cscut (cmpt2 (λ x1 x2 . cpw csur) (λ x1 x2 . cima csslt (csn (cv x1))) (λ x1 x2 . crio (λ x3 . wceq (cfv (cv x3) cbday) (cint (cima cbday (crab (λ x4 . wa (wbr (cv x1) (csn (cv x4)) csslt) (wbr (csn (cv x4)) (cv x2) csslt)) (λ x4 . csur))))) (λ x3 . crab (λ x4 . wa (wbr (cv x1) (csn (cv x4)) csslt) (wbr (csn (cv x4)) (cv x2) csslt)) (λ x4 . csur)))) ⟶ wceq cmade (crecs (cmpt (λ x1 . cvv) (λ x1 . cima cscut (cxp (cpw (cuni (crn (cv x1)))) (cpw (cuni (crn (cv x1)))))))) ⟶ wceq cold (cmpt (λ x1 . con0) (λ x1 . cuni (cima cmade (cv x1)))) ⟶ wceq cnew (cmpt (λ x1 . con0) (λ x1 . cdif (cfv (cv x1) cold) (cfv (cv x1) cmade))) ⟶ wceq cleft (cmpt (λ x1 . csur) (λ x1 . crab (λ x2 . wral (λ x3 . wa (wbr (cv x2) (cv x3) cslt) (wbr (cv x3) (cv x1) cslt) ⟶ wcel (cfv (cv x2) cbday) (cfv (cv x3) cbday)) (λ x3 . csur)) (λ x2 . cfv (cfv (cv x1) cbday) cold))) ⟶ wceq cright (cmpt (λ x1 . csur) (λ x1 . crab (λ x2 . wral (λ x3 . wa (wbr (cv x1) (cv x3) cslt) (wbr (cv x3) (cv x2) cslt) ⟶ wcel (cfv (cv x2) cbday) (cfv (cv x3) cbday)) (λ x3 . csur)) (λ x2 . cfv (cfv (cv x1) cbday) cold))) ⟶ (∀ x1 x2 : ι → ο . wceq (ctxp x1 x2) (cin (ccom (ccnv (cres c1st (cxp cvv cvv))) x1) (ccom (ccnv (cres c2nd (cxp cvv cvv))) x2))) ⟶ (∀ x1 x2 : ι → ο . wceq (cpprod x1 x2) (ctxp (ccom x1 (cres c1st (cxp cvv cvv))) (ccom x2 (cres c2nd (cxp cvv cvv))))) ⟶ wceq csset (cdif (cxp cvv cvv) (crn (ctxp cep (cdif cvv cep)))) ⟶ wceq ctrans (cdif cvv (crn (cdif (ccom cep cep) cep))) ⟶ wceq cbigcup (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (ccom cep cep) cvv)))) ⟶ (∀ x1 : ι → ο . wceq (cfix x1) (cdm (cin x1 cid))) ⟶ wceq climits (cdif (cin con0 (cfix cbigcup)) (csn c0)) ⟶ wceq cfuns (cdif (cpw (cxp cvv cvv)) (cfix (ccom cep (ccom (ctxp c1st (ccom (cdif cvv cid) c2nd)) (ccnv cep))))) ⟶ wceq csingle (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp cid cvv)))) ⟶ wceq csingles (crn csingle) ⟶ (∀ x1 : ι → ο . wceq (cimage x1) (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (ccom cep (ccnv x1)) cvv))))) ⟶ x0) ⟶ x0
Theorem df_sslt : wceq csslt (copab (λ x0 x1 . w3a (wss (cv x0) csur) (wss (cv x1) csur) (wral (λ x2 . wral (λ x3 . wbr (cv x2) (cv x3) cslt) (λ x3 . cv x1)) (λ x2 . cv x0)))) (proof)
Theorem df_scut : wceq cscut (cmpt2 (λ x0 x1 . cpw csur) (λ x0 x1 . cima csslt (csn (cv x0))) (λ x0 x1 . crio (λ x2 . wceq (cfv (cv x2) cbday) (cint (cima cbday (crab (λ x3 . wa (wbr (cv x0) (csn (cv x3)) csslt) (wbr (csn (cv x3)) (cv x1) csslt)) (λ x3 . csur))))) (λ x2 . crab (λ x3 . wa (wbr (cv x0) (csn (cv x3)) csslt) (wbr (csn (cv x3)) (cv x1) csslt)) (λ x3 . csur)))) (proof)
Theorem df_made : wceq cmade (crecs (cmpt (λ x0 . cvv) (λ x0 . cima cscut (cxp (cpw (cuni (crn (cv x0)))) (cpw (cuni (crn (cv x0)))))))) (proof)
Theorem df_old : wceq cold (cmpt (λ x0 . con0) (λ x0 . cuni (cima cmade (cv x0)))) (proof)
Theorem df_new : wceq cnew (cmpt (λ x0 . con0) (λ x0 . cdif (cfv (cv x0) cold) (cfv (cv x0) cmade))) (proof)
Theorem df_left : wceq cleft (cmpt (λ x0 . csur) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wbr (cv x1) (cv x2) cslt) (wbr (cv x2) (cv x0) cslt) ⟶ wcel (cfv (cv x1) cbday) (cfv (cv x2) cbday)) (λ x2 . csur)) (λ x1 . cfv (cfv (cv x0) cbday) cold))) (proof)
Theorem df_right : wceq cright (cmpt (λ x0 . csur) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wbr (cv x0) (cv x2) cslt) (wbr (cv x2) (cv x1) cslt) ⟶ wcel (cfv (cv x1) cbday) (cfv (cv x2) cbday)) (λ x2 . csur)) (λ x1 . cfv (cfv (cv x0) cbday) cold))) (proof)
Theorem df_txp : ∀ x0 x1 : ι → ο . wceq (ctxp x0 x1) (cin (ccom (ccnv (cres c1st (cxp cvv cvv))) x0) (ccom (ccnv (cres c2nd (cxp cvv cvv))) x1)) (proof)
Theorem df_pprod : ∀ x0 x1 : ι → ο . wceq (cpprod x0 x1) (ctxp (ccom x0 (cres c1st (cxp cvv cvv))) (ccom x1 (cres c2nd (cxp cvv cvv)))) (proof)
Theorem df_sset : wceq csset (cdif (cxp cvv cvv) (crn (ctxp cep (cdif cvv cep)))) (proof)
Theorem df_trans : wceq ctrans (cdif cvv (crn (cdif (ccom cep cep) cep))) (proof)
Theorem df_bigcup : wceq cbigcup (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (ccom cep cep) cvv)))) (proof)
Theorem df_fix : ∀ x0 : ι → ο . wceq (cfix x0) (cdm (cin x0 cid)) (proof)
Theorem df_limits : wceq climits (cdif (cin con0 (cfix cbigcup)) (csn c0)) (proof)
Theorem df_funs : wceq cfuns (cdif (cpw (cxp cvv cvv)) (cfix (ccom cep (ccom (ctxp c1st (ccom (cdif cvv cid) c2nd)) (ccnv cep))))) (proof)
Theorem df_singleton : wceq csingle (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp cid cvv)))) (proof)
Theorem df_singles : wceq csingles (crn csingle) (proof)
Theorem df_image : ∀ x0 : ι → ο . wceq (cimage x0) (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (ccom cep (ccnv x0)) cvv)))) (proof)