Proofgold Asset

Known df_sx__df_meas__df_dde__df_ae__df_fae__df_mbfm__df_oms__df_carsg__df_sitg__df_sitm__df_itgm__df_sseq__df_fib__df_prob__df_cndprob__df_rrv__df_orvc__df_repr : ∀ x0 : ο . (wceq csx (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cfv (crn (cmpt2 (λ x3 x4 . cv x1) (λ x3 x4 . cv x2) (λ x3 x4 . cxp (cv x3) (cv x4)))) csigagen)) ⟶ wceq cmeas (cmpt (λ x1 . cuni (crn csiga)) (λ x1 . cab (λ x2 . w3a (wf (cv x1) (co cc0 cpnf cicc) (cv x2)) (wceq (cfv c0 (cv x2)) cc0) (wral (λ x3 . wa (wbr (cv x3) com cdom) (wdisj (λ x4 . cv x3) cv) ⟶ wceq (cfv (cuni (cv x3)) (cv x2)) (cesum (λ x4 . cv x3) (λ x4 . cfv (cv x4) (cv x2)))) (λ x3 . cpw (cv x1)))))) ⟶ wceq cdde (cmpt (λ x1 . cpw cr) (λ x1 . cif (wcel cc0 (cv x1)) c1 cc0)) ⟶ wceq cae (copab (λ x1 x2 . wceq (cfv (cdif (cuni (cdm (cv x2))) (cv x1)) (cv x2)) cc0)) ⟶ wceq cfae (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cuni (crn cmeas)) (λ x1 x2 . copab (λ x3 x4 . wa (wa (wcel (cv x3) (co (cdm (cv x1)) (cuni (cdm (cv x2))) cmap)) (wcel (cv x4) (co (cdm (cv x1)) (cuni (cdm (cv x2))) cmap))) (wbr (crab (λ x5 . wbr (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)) (cv x1)) (λ x5 . cuni (cdm (cv x2)))) (cv x2) cae)))) ⟶ wceq cmbfm (cmpt2 (λ x1 x2 . cuni (crn csiga)) (λ x1 x2 . cuni (crn csiga)) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wcel (cima (ccnv (cv x3)) (cv x4)) (cv x1)) (λ x4 . cv x2)) (λ x3 . co (cuni (cv x2)) (cuni (cv x1)) cmap))) ⟶ wceq coms (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cuni (cdm (cv x1)))) (λ x2 . cinf (crn (cmpt (λ x3 . crab (λ x4 . wa (wss (cv x2) (cuni (cv x4))) (wbr (cv x4) com cdom)) (λ x4 . cpw (cdm (cv x1)))) (λ x3 . cesum (λ x4 . cv x3) (λ x4 . cfv (cv x4) (cv x1))))) (co cc0 cpnf cicc) clt))) ⟶ wceq ccarsg (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cfv (cin (cv x3) (cv x2)) (cv x1)) (cfv (cdif (cv x3) (cv x2)) (cv x1)) cxad) (cfv (cv x3) (cv x1))) (λ x3 . cpw (cuni (cdm (cv x1))))) (λ x2 . cpw (cuni (cdm (cv x1)))))) ⟶ wceq csitg (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cuni (crn cmeas)) (λ x1 x2 . cmpt (λ x3 . crab (λ x4 . wa (wcel (crn (cv x4)) cfn) (wral (λ x5 . wcel (cfv (cima (ccnv (cv x4)) (csn (cv x5))) (cv x2)) (co cc0 cpnf cico)) (λ x5 . cdif (crn (cv x4)) (csn (cfv (cv x1) c0g))))) (λ x4 . co (cdm (cv x2)) (cfv (cfv (cv x1) ctopn) csigagen) cmbfm)) (λ x3 . co (cv x1) (cmpt (λ x4 . cdif (crn (cv x3)) (csn (cfv (cv x1) c0g))) (λ x4 . co (cfv (cfv (cima (ccnv (cv x3)) (csn (cv x4))) (cv x2)) (cfv (cfv (cv x1) csca) crrh)) (cv x4) (cfv (cv x1) cvsca))) cgsu))) ⟶ wceq csitm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cuni (crn cmeas)) (λ x1 x2 . cmpt2 (λ x3 x4 . cdm (co (cv x1) (cv x2) csitg)) (λ x3 x4 . cdm (co (cv x1) (cv x2) csitg)) (λ x3 x4 . cfv (co (cv x3) (cv x4) (cof (cfv (cv x1) cds))) (co (co cxrs (co cc0 cpnf cicc) cress) (cv x2) csitg)))) ⟶ wceq citgm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cuni (crn cmeas)) (λ x1 x2 . cfv (co (cv x1) (cv x2) csitg) (co (cfv (co (cv x1) (cv x2) csitm) cmetu) (cfv (cv x1) cuss) ccnext))) ⟶ wceq csseq (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cun (cv x1) (ccom clsw (cseq (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . co (cv x3) (cs1 (cfv (cv x3) (cv x2))) cconcat)) (cxp cn0 (csn (co (cv x1) (cs1 (cfv (cv x1) (cv x2))) cconcat))) (cfv (cv x1) chash))))) ⟶ wceq cfib (co (cs2 cc0 c1) (cmpt (λ x1 . cin (cword cn0) (cima (ccnv chash) (cfv c2 cuz))) (λ x1 . co (cfv (co (cfv (cv x1) chash) c2 cmin) (cv x1)) (cfv (co (cfv (cv x1) chash) c1 cmin) (cv x1)) caddc)) csseq) ⟶ wceq cprb (crab (λ x1 . wceq (cfv (cuni (cdm (cv x1))) (cv x1)) c1) (λ x1 . cuni (crn cmeas))) ⟶ wceq ccprob (cmpt (λ x1 . cprb) (λ x1 . cmpt2 (λ x2 x3 . cdm (cv x1)) (λ x2 x3 . cdm (cv x1)) (λ x2 x3 . co (cfv (cin (cv x2) (cv x3)) (cv x1)) (cfv (cv x3) (cv x1)) cdiv))) ⟶ wceq crrv (cmpt (λ x1 . cprb) (λ x1 . co (cdm (cv x1)) cbrsiga cmbfm)) ⟶ (∀ x1 : ι → ο . wceq (corvc x1) (cmpt2 (λ x2 x3 . cab (λ x4 . wfun (cv x4))) (λ x2 x3 . cvv) (λ x2 x3 . cima (ccnv (cv x2)) (cab (λ x4 . wbr (cv x4) (cv x3) x1))))) ⟶ wceq crepr (cmpt (λ x1 . cn0) (λ x1 . cmpt2 (λ x2 x3 . cpw cn) (λ x2 x3 . cz) (λ x2 x3 . crab (λ x4 . wceq (csu (co cc0 (cv x1) cfzo) (λ x5 . cfv (cv x5) (cv x4))) (cv x3)) (λ x4 . co (cv x2) (co cc0 (cv x1) cfzo) cmap)))) ⟶ x0) ⟶ x0
Theorem df_sx : wceq csx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) csigagen)) (proof)
Theorem df_meas : wceq cmeas (cmpt (λ x0 . cuni (crn csiga)) (λ x0 . cab (λ x1 . w3a (wf (cv x0) (co cc0 cpnf cicc) (cv x1)) (wceq (cfv c0 (cv x1)) cc0) (wral (λ x2 . wa (wbr (cv x2) com cdom) (wdisj (λ x3 . cv x2) cv) ⟶ wceq (cfv (cuni (cv x2)) (cv x1)) (cesum (λ x3 . cv x2) (λ x3 . cfv (cv x3) (cv x1)))) (λ x2 . cpw (cv x0)))))) (proof)
Theorem df_dde : wceq cdde (cmpt (λ x0 . cpw cr) (λ x0 . cif (wcel cc0 (cv x0)) c1 cc0)) (proof)
Theorem df_ae : wceq cae (copab (λ x0 x1 . wceq (cfv (cdif (cuni (cdm (cv x1))) (cv x0)) (cv x1)) cc0)) (proof)
Theorem df_fae : wceq cfae (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap)) (wcel (cv x3) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap))) (wbr (crab (λ x4 . wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) (cv x0)) (λ x4 . cuni (cdm (cv x1)))) (cv x1) cae)))) (proof)
Theorem df_mbfm : wceq cmbfm (cmpt2 (λ x0 x1 . cuni (crn csiga)) (λ x0 x1 . cuni (crn csiga)) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (cv x3)) (cv x0)) (λ x3 . cv x1)) (λ x2 . co (cuni (cv x1)) (cuni (cv x0)) cmap))) (proof)
Theorem df_oms : wceq coms (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cuni (cdm (cv x0)))) (λ x1 . cinf (crn (cmpt (λ x2 . crab (λ x3 . wa (wss (cv x1) (cuni (cv x3))) (wbr (cv x3) com cdom)) (λ x3 . cpw (cdm (cv x0)))) (λ x2 . cesum (λ x3 . cv x2) (λ x3 . cfv (cv x3) (cv x0))))) (co cc0 cpnf cicc) clt))) (proof)
Theorem df_carsg : wceq ccarsg (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cfv (cin (cv x2) (cv x1)) (cv x0)) (cfv (cdif (cv x2) (cv x1)) (cv x0)) cxad) (cfv (cv x2) (cv x0))) (λ x2 . cpw (cuni (cdm (cv x0))))) (λ x1 . cpw (cuni (cdm (cv x0)))))) (proof)
Theorem df_sitg : wceq csitg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . cmpt (λ x2 . crab (λ x3 . wa (wcel (crn (cv x3)) cfn) (wral (λ x4 . wcel (cfv (cima (ccnv (cv x3)) (csn (cv x4))) (cv x1)) (co cc0 cpnf cico)) (λ x4 . cdif (crn (cv x3)) (csn (cfv (cv x0) c0g))))) (λ x3 . co (cdm (cv x1)) (cfv (cfv (cv x0) ctopn) csigagen) cmbfm)) (λ x2 . co (cv x0) (cmpt (λ x3 . cdif (crn (cv x2)) (csn (cfv (cv x0) c0g))) (λ x3 . co (cfv (cfv (cima (ccnv (cv x2)) (csn (cv x3))) (cv x1)) (cfv (cfv (cv x0) csca) crrh)) (cv x3) (cfv (cv x0) cvsca))) cgsu))) (proof)
Theorem df_sitm : wceq csitm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . cmpt2 (λ x2 x3 . cdm (co (cv x0) (cv x1) csitg)) (λ x2 x3 . cdm (co (cv x0) (cv x1) csitg)) (λ x2 x3 . cfv (co (cv x2) (cv x3) (cof (cfv (cv x0) cds))) (co (co cxrs (co cc0 cpnf cicc) cress) (cv x1) csitg)))) (proof)
Theorem df_itgm : wceq citgm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . cfv (co (cv x0) (cv x1) csitg) (co (cfv (co (cv x0) (cv x1) csitm) cmetu) (cfv (cv x0) cuss) ccnext))) (proof)
Theorem df_sseq : wceq csseq (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cun (cv x0) (ccom clsw (cseq (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . co (cv x2) (cs1 (cfv (cv x2) (cv x1))) cconcat)) (cxp cn0 (csn (co (cv x0) (cs1 (cfv (cv x0) (cv x1))) cconcat))) (cfv (cv x0) chash))))) (proof)
Theorem df_fib : wceq cfib (co (cs2 cc0 c1) (cmpt (λ x0 . cin (cword cn0) (cima (ccnv chash) (cfv c2 cuz))) (λ x0 . co (cfv (co (cfv (cv x0) chash) c2 cmin) (cv x0)) (cfv (co (cfv (cv x0) chash) c1 cmin) (cv x0)) caddc)) csseq) (proof)
Theorem df_prob : wceq cprb (crab (λ x0 . wceq (cfv (cuni (cdm (cv x0))) (cv x0)) c1) (λ x0 . cuni (crn cmeas))) (proof)
Theorem df_cndprob : wceq ccprob (cmpt (λ x0 . cprb) (λ x0 . cmpt2 (λ x1 x2 . cdm (cv x0)) (λ x1 x2 . cdm (cv x0)) (λ x1 x2 . co (cfv (cin (cv x1) (cv x2)) (cv x0)) (cfv (cv x2) (cv x0)) cdiv))) (proof)
Theorem df_rrv : wceq crrv (cmpt (λ x0 . cprb) (λ x0 . co (cdm (cv x0)) cbrsiga cmbfm)) (proof)
Theorem df_orvc : ∀ x0 : ι → ο . wceq (corvc x0) (cmpt2 (λ x1 x2 . cab (λ x3 . wfun (cv x3))) (λ x1 x2 . cvv) (λ x1 x2 . cima (ccnv (cv x1)) (cab (λ x3 . wbr (cv x3) (cv x2) x0)))) (proof)
Theorem df_repr : wceq crepr (cmpt (λ x0 . cn0) (λ x0 . cmpt2 (λ x1 x2 . cpw cn) (λ x1 x2 . cz) (λ x1 x2 . crab (λ x3 . wceq (csu (co cc0 (cv x0) cfzo) (λ x4 . cfv (cv x4) (cv x3))) (cv x2)) (λ x3 . co (cv x1) (co cc0 (cv x0) cfzo) cmap)))) (proof)