Proofgold Asset

Known df_cnp__df_lm__df_t0__df_t1__df_haus__df_reg__df_nrm__df_cnrm__df_pnrm__df_cmp__df_conn__df_1stc__df_2ndc__df_lly__df_nlly__df_ref__df_ptfin__df_locfin : ∀ x0 : ο . (wceq ccnp (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . cmpt (λ x3 . cuni (cv x1)) (λ x3 . crab (λ x4 . wral (λ x5 . wcel (cfv (cv x3) (cv x4)) (cv x5) ⟶ wrex (λ x6 . wa (wcel (cv x3) (cv x6)) (wss (cima (cv x4) (cv x6)) (cv x5))) (λ x6 . cv x1)) (λ x5 . cv x2)) (λ x4 . co (cuni (cv x2)) (cuni (cv x1)) cmap)))) ⟶ wceq clm (cmpt (λ x1 . ctop) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (co (cuni (cv x1)) cc cpm)) (wcel (cv x3) (cuni (cv x1))) (wral (λ x4 . wcel (cv x3) (cv x4) ⟶ wrex (λ x5 . wf (cv x5) (cv x4) (cres (cv x2) (cv x5))) (λ x5 . crn cuz)) (λ x4 . cv x1))))) ⟶ wceq ct0 (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wb (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4))) (λ x4 . cv x1) ⟶ wceq (cv x2) (cv x3)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq ct1 (crab (λ x1 . wral (λ x2 . wcel (csn (cv x2)) (cfv (cv x1) ccld)) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq cha (crab (λ x1 . wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3) ⟶ wrex (λ x4 . wrex (λ x5 . w3a (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x5)) (wceq (cin (cv x4) (cv x5)) c0)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq creg (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wss (cfv (cv x4) (cfv (cv x1) ccl)) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)) ⟶ wceq cnrm (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wss (cv x3) (cv x4)) (wss (cfv (cv x4) (cfv (cv x1) ccl)) (cv x2))) (λ x4 . cv x1)) (λ x3 . cin (cfv (cv x1) ccld) (cpw (cv x2)))) (λ x2 . cv x1)) (λ x1 . ctop)) ⟶ wceq ccnrm (crab (λ x1 . wral (λ x2 . wcel (co (cv x1) (cv x2) crest) cnrm) (λ x2 . cpw (cuni (cv x1)))) (λ x1 . ctop)) ⟶ wceq cpnrm (crab (λ x1 . wss (cfv (cv x1) ccld) (crn (cmpt (λ x2 . co (cv x1) cn cmap) (λ x2 . cint (crn (cv x2)))))) (λ x1 . cnrm)) ⟶ wceq ccmp (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2)) ⟶ wrex (λ x3 . wceq (cuni (cv x1)) (cuni (cv x3))) (λ x3 . cin (cpw (cv x2)) cfn)) (λ x2 . cpw (cv x1))) (λ x1 . ctop)) ⟶ wceq cconn (crab (λ x1 . wceq (cin (cv x1) (cfv (cv x1) ccld)) (cpr c0 (cuni (cv x1)))) (λ x1 . ctop)) ⟶ wceq c1stc (crab (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wbr (cv x3) com cdom) (wral (λ x4 . wcel (cv x2) (cv x4) ⟶ wcel (cv x2) (cuni (cin (cv x3) (cpw (cv x4))))) (λ x4 . cv x1))) (λ x3 . cpw (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq c2ndc (cab (λ x1 . wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cfv (cv x2) ctg) (cv x1))) (λ x2 . ctb))) ⟶ (∀ x1 : ι → ο . wceq (clly x1) (crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wa (wcel (cv x4) (cv x5)) (wcel (co (cv x2) (cv x5) crest) x1)) (λ x5 . cin (cv x2) (cpw (cv x3)))) (λ x4 . cv x3)) (λ x3 . cv x2)) (λ x2 . ctop))) ⟶ (∀ x1 : ι → ο . wceq (cnlly x1) (crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wcel (co (cv x2) (cv x5) crest) x1) (λ x5 . cin (cfv (csn (cv x4)) (cfv (cv x2) cnei)) (cpw (cv x3)))) (λ x4 . cv x3)) (λ x3 . cv x2)) (λ x2 . ctop))) ⟶ wceq cref (copab (λ x1 x2 . wa (wceq (cuni (cv x2)) (cuni (cv x1))) (wral (λ x3 . wrex (λ x4 . wss (cv x3) (cv x4)) (λ x4 . cv x2)) (λ x3 . cv x1)))) ⟶ wceq cptfin (cab (λ x1 . wral (λ x2 . wcel (crab (λ x3 . wcel (cv x2) (cv x3)) (λ x3 . cv x1)) cfn) (λ x2 . cuni (cv x1)))) ⟶ wceq clocfin (cmpt (λ x1 . ctop) (λ x1 . cab (λ x2 . wa (wceq (cuni (cv x1)) (cuni (cv x2))) (wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wcel (crab (λ x5 . wne (cin (cv x5) (cv x4)) c0) (λ x5 . cv x2)) cfn)) (λ x4 . cv x1)) (λ x3 . cuni (cv x1)))))) ⟶ x0) ⟶ x0
Theorem df_cnp : wceq ccnp (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cmpt (λ x2 . cuni (cv x0)) (λ x2 . crab (λ x3 . wral (λ x4 . wcel (cfv (cv x2) (cv x3)) (cv x4) ⟶ wrex (λ x5 . wa (wcel (cv x2) (cv x5)) (wss (cima (cv x3) (cv x5)) (cv x4))) (λ x5 . cv x0)) (λ x4 . cv x1)) (λ x3 . co (cuni (cv x1)) (cuni (cv x0)) cmap)))) (proof)
Theorem df_lm : wceq clm (cmpt (λ x0 . ctop) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (co (cuni (cv x0)) cc cpm)) (wcel (cv x2) (cuni (cv x0))) (wral (λ x3 . wcel (cv x2) (cv x3) ⟶ wrex (λ x4 . wf (cv x4) (cv x3) (cres (cv x1) (cv x4))) (λ x4 . crn cuz)) (λ x3 . cv x0))))) (proof)
Theorem df_t0 : wceq ct0 (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wb (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0) ⟶ wceq (cv x1) (cv x2)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_t1 : wceq ct1 (crab (λ x0 . wral (λ x1 . wcel (csn (cv x1)) (cfv (cv x0) ccld)) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_haus : wceq cha (crab (λ x0 . wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wrex (λ x3 . wrex (λ x4 . w3a (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x4)) (wceq (cin (cv x3) (cv x4)) c0)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_reg : wceq creg (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wcel (cv x2) (cv x3)) (wss (cfv (cv x3) (cfv (cv x0) ccl)) (cv x1))) (λ x3 . cv x0)) (λ x2 . cv x1)) (λ x1 . cv x0)) (λ x0 . ctop)) (proof)
Theorem df_nrm : wceq cnrm (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wss (cv x2) (cv x3)) (wss (cfv (cv x3) (cfv (cv x0) ccl)) (cv x1))) (λ x3 . cv x0)) (λ x2 . cin (cfv (cv x0) ccld) (cpw (cv x1)))) (λ x1 . cv x0)) (λ x0 . ctop)) (proof)
Theorem df_cnrm : wceq ccnrm (crab (λ x0 . wral (λ x1 . wcel (co (cv x0) (cv x1) crest) cnrm) (λ x1 . cpw (cuni (cv x0)))) (λ x0 . ctop)) (proof)
Theorem df_pnrm : wceq cpnrm (crab (λ x0 . wss (cfv (cv x0) ccld) (crn (cmpt (λ x1 . co (cv x0) cn cmap) (λ x1 . cint (crn (cv x1)))))) (λ x0 . cnrm)) (proof)
Theorem df_cmp : wceq ccmp (crab (λ x0 . wral (λ x1 . wceq (cuni (cv x0)) (cuni (cv x1)) ⟶ wrex (λ x2 . wceq (cuni (cv x0)) (cuni (cv x2))) (λ x2 . cin (cpw (cv x1)) cfn)) (λ x1 . cpw (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_conn : wceq cconn (crab (λ x0 . wceq (cin (cv x0) (cfv (cv x0) ccld)) (cpr c0 (cuni (cv x0)))) (λ x0 . ctop)) (proof)
Theorem df_1stc : wceq c1stc (crab (λ x0 . wral (λ x1 . wrex (λ x2 . wa (wbr (cv x2) com cdom) (wral (λ x3 . wcel (cv x1) (cv x3) ⟶ wcel (cv x1) (cuni (cin (cv x2) (cpw (cv x3))))) (λ x3 . cv x0))) (λ x2 . cpw (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_2ndc : wceq c2ndc (cab (λ x0 . wrex (λ x1 . wa (wbr (cv x1) com cdom) (wceq (cfv (cv x1) ctg) (cv x0))) (λ x1 . ctb))) (proof)
Theorem df_lly : ∀ x0 : ι → ο . wceq (clly x0) (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wcel (co (cv x1) (cv x4) crest) x0)) (λ x4 . cin (cv x1) (cpw (cv x2)))) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)) (proof)
Theorem df_nlly : ∀ x0 : ι → ο . wceq (cnlly x0) (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wcel (co (cv x1) (cv x4) crest) x0) (λ x4 . cin (cfv (csn (cv x3)) (cfv (cv x1) cnei)) (cpw (cv x2)))) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)) (proof)
Theorem df_ref : wceq cref (copab (λ x0 x1 . wa (wceq (cuni (cv x1)) (cuni (cv x0))) (wral (λ x2 . wrex (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cv x1)) (λ x2 . cv x0)))) (proof)
Theorem df_ptfin : wceq cptfin (cab (λ x0 . wral (λ x1 . wcel (crab (λ x2 . wcel (cv x1) (cv x2)) (λ x2 . cv x0)) cfn) (λ x1 . cuni (cv x0)))) (proof)
Theorem df_locfin : wceq clocfin (cmpt (λ x0 . ctop) (λ x0 . cab (λ x1 . wa (wceq (cuni (cv x0)) (cuni (cv x1))) (wral (λ x2 . wrex (λ x3 . wa (wcel (cv x2) (cv x3)) (wcel (crab (λ x4 . wne (cin (cv x4) (cv x3)) c0) (λ x4 . cv x1)) cfn)) (λ x3 . cv x0)) (λ x2 . cuni (cv x0)))))) (proof)