Proofgold Address

Known df_lmat__df_cref__df_ldlf__df_pcmp__df_metid__df_pstm__df_hcmp__df_qqh__df_rrh__df_rrext__df_xrh__df_mntop__df_ind__df_esum__df_ofc__df_siga__df_sigagen__df_brsiga : ∀ x0 : ο . (wceq clmat (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . co c1 (cfv (cv x1) chash) cfz) (λ x2 x3 . co c1 (cfv (cfv cc0 (cv x1)) chash) cfz) (λ x2 x3 . cfv (co (cv x3) c1 cmin) (cfv (co (cv x2) c1 cmin) (cv x1))))) ⟶ (∀ x1 : ι → ο . wceq (ccref x1) (crab (λ x2 . wral (λ x3 . wceq (cuni (cv x2)) (cuni (cv x3)) ⟶ wrex (λ x4 . wbr (cv x4) (cv x3) cref) (λ x4 . cin (cpw (cv x2)) x1)) (λ x3 . cpw (cv x2))) (λ x2 . ctop))) ⟶ wceq cldlf (ccref (cab (λ x1 . wbr (cv x1) com cdom))) ⟶ wceq cpcmp (cab (λ x1 . wcel (cv x1) (ccref (cfv (cv x1) clocfin)))) ⟶ wceq cmetid (cmpt (λ x1 . cuni (crn cpsmet)) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cdm (cdm (cv x1)))) (wcel (cv x3) (cdm (cdm (cv x1))))) (wceq (co (cv x2) (cv x3) (cv x1)) cc0)))) ⟶ wceq cpstm (cmpt (λ x1 . cuni (crn cpsmet)) (λ x1 . cmpt2 (λ x2 x3 . cqs (cdm (cdm (cv x1))) (cfv (cv x1) cmetid)) (λ x2 x3 . cqs (cdm (cdm (cv x1))) (cfv (cv x1) cmetid)) (λ x2 x3 . cuni (cab (λ x4 . wrex (λ x5 . wrex (λ x6 . wceq (cv x4) (co (cv x5) (cv x6) (cv x1))) (λ x6 . cv x3)) (λ x5 . cv x2)))))) ⟶ wceq chcmp (copab (λ x1 x2 . w3a (wa (wcel (cv x1) (cuni (crn cust))) (wcel (cv x2) ccusp)) (wceq (co (cfv (cv x2) cuss) (cdm (cuni (cv x1))) crest) (cv x1)) (wceq (cfv (cdm (cuni (cv x1))) (cfv (cfv (cv x2) ctopn) ccl)) (cfv (cv x2) cbs)))) ⟶ wceq cqqh (cmpt (λ x1 . cvv) (λ x1 . crn (cmpt2 (λ x2 x3 . cz) (λ x2 x3 . cima (ccnv (cfv (cv x1) czrh)) (cfv (cv x1) cui)) (λ x2 x3 . cop (co (cv x2) (cv x3) cdiv) (co (cfv (cv x2) (cfv (cv x1) czrh)) (cfv (cv x3) (cfv (cv x1) czrh)) (cfv (cv x1) cdvr)))))) ⟶ wceq crrh (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cqqh) (co (cfv (crn cioo) ctg) (cfv (cv x1) ctopn) ccnext))) ⟶ wceq crrext (crab (λ x1 . wa (wa (wcel (cfv (cv x1) czlm) cnlm) (wceq (cfv (cv x1) cchr) cc0)) (wa (wcel (cv x1) ccusp) (wceq (cfv (cv x1) cuss) (cfv (cres (cfv (cv x1) cds) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) cmetu)))) (λ x1 . cin cnrg cdr)) ⟶ wceq cxrh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cxr) (λ x2 . cif (wcel (cv x2) cr) (cfv (cv x2) (cfv (cv x1) crrh)) (cif (wceq (cv x2) cpnf) (cfv (cima (cfv (cv x1) crrh) cr) (cfv (cv x1) club)) (cfv (cima (cfv (cv x1) crrh) cr) (cfv (cv x1) cglb)))))) ⟶ wceq cmntop (copab (λ x1 x2 . wa (wcel (cv x1) cn0) (w3a (wcel (cv x2) c2ndc) (wcel (cv x2) cha) (wcel (cv x2) (clly (cec (cfv (cfv (cv x1) cehl) ctopn) chmph)))))) ⟶ wceq cind (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cv x1)) (λ x2 . cmpt (λ x3 . cv x1) (λ x3 . cif (wcel (cv x3) (cv x2)) c1 cc0)))) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (cesum x1 x2) (cuni (co (co cxrs (co cc0 cpnf cicc) cress) (cmpt x1 x2) ctsu))) ⟶ (∀ x1 : ι → ο . wceq (cofc x1) (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . cmpt (λ x4 . cdm (cv x2)) (λ x4 . co (cfv (cv x4) (cv x2)) (cv x3) x1)))) ⟶ wceq csiga (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wss (cv x2) (cpw (cv x1))) (w3a (wcel (cv x1) (cv x2)) (wral (λ x3 . wcel (cdif (cv x1) (cv x3)) (cv x2)) (λ x3 . cv x2)) (wral (λ x3 . wbr (cv x3) com cdom ⟶ wcel (cuni (cv x3)) (cv x2)) (λ x3 . cpw (cv x2))))))) ⟶ wceq csigagen (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cuni (cv x1)) csiga)))) ⟶ wceq cbrsiga (cfv (cfv (crn cioo) ctg) csigagen) ⟶ x0) ⟶ x0
Theorem df_lmat : wceq clmat (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . co c1 (cfv (cv x0) chash) cfz) (λ x1 x2 . co c1 (cfv (cfv cc0 (cv x0)) chash) cfz) (λ x1 x2 . cfv (co (cv x2) c1 cmin) (cfv (co (cv x1) c1 cmin) (cv x0))))) (proof)
Theorem df_cref : ∀ x0 : ι → ο . wceq (ccref x0) (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2)) ⟶ wrex (λ x3 . wbr (cv x3) (cv x2) cref) (λ x3 . cin (cpw (cv x1)) x0)) (λ x2 . cpw (cv x1))) (λ x1 . ctop)) (proof)
Theorem df_ldlf : wceq cldlf (ccref (cab (λ x0 . wbr (cv x0) com cdom))) (proof)
Theorem df_pcmp : wceq cpcmp (cab (λ x0 . wcel (cv x0) (ccref (cfv (cv x0) clocfin)))) (proof)
Theorem df_metid : wceq cmetid (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cdm (cdm (cv x0)))) (wcel (cv x2) (cdm (cdm (cv x0))))) (wceq (co (cv x1) (cv x2) (cv x0)) cc0)))) (proof)
Theorem df_pstm : wceq cpstm (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . cmpt2 (λ x1 x2 . cqs (cdm (cdm (cv x0))) (cfv (cv x0) cmetid)) (λ x1 x2 . cqs (cdm (cdm (cv x0))) (cfv (cv x0) cmetid)) (λ x1 x2 . cuni (cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) (cv x0))) (λ x5 . cv x2)) (λ x4 . cv x1)))))) (proof)
Theorem df_hcmp : wceq chcmp (copab (λ x0 x1 . w3a (wa (wcel (cv x0) (cuni (crn cust))) (wcel (cv x1) ccusp)) (wceq (co (cfv (cv x1) cuss) (cdm (cuni (cv x0))) crest) (cv x0)) (wceq (cfv (cdm (cuni (cv x0))) (cfv (cfv (cv x1) ctopn) ccl)) (cfv (cv x1) cbs)))) (proof)
Theorem df_qqh : wceq cqqh (cmpt (λ x0 . cvv) (λ x0 . crn (cmpt2 (λ x1 x2 . cz) (λ x1 x2 . cima (ccnv (cfv (cv x0) czrh)) (cfv (cv x0) cui)) (λ x1 x2 . cop (co (cv x1) (cv x2) cdiv) (co (cfv (cv x1) (cfv (cv x0) czrh)) (cfv (cv x2) (cfv (cv x0) czrh)) (cfv (cv x0) cdvr)))))) (proof)
Theorem df_rrh : wceq crrh (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cqqh) (co (cfv (crn cioo) ctg) (cfv (cv x0) ctopn) ccnext))) (proof)
Theorem df_rrext : wceq crrext (crab (λ x0 . wa (wa (wcel (cfv (cv x0) czlm) cnlm) (wceq (cfv (cv x0) cchr) cc0)) (wa (wcel (cv x0) ccusp) (wceq (cfv (cv x0) cuss) (cfv (cres (cfv (cv x0) cds) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) cmetu)))) (λ x0 . cin cnrg cdr)) (proof)
Theorem df_xrh : wceq cxrh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cxr) (λ x1 . cif (wcel (cv x1) cr) (cfv (cv x1) (cfv (cv x0) crrh)) (cif (wceq (cv x1) cpnf) (cfv (cima (cfv (cv x0) crrh) cr) (cfv (cv x0) club)) (cfv (cima (cfv (cv x0) crrh) cr) (cfv (cv x0) cglb)))))) (proof)
Theorem df_mntop : wceq cmntop (copab (λ x0 x1 . wa (wcel (cv x0) cn0) (w3a (wcel (cv x1) c2ndc) (wcel (cv x1) cha) (wcel (cv x1) (clly (cec (cfv (cfv (cv x0) cehl) ctopn) chmph)))))) (proof)
Theorem df_ind : wceq cind (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cv x0)) (λ x1 . cmpt (λ x2 . cv x0) (λ x2 . cif (wcel (cv x2) (cv x1)) c1 cc0)))) (proof)
Theorem df_esum : ∀ x0 x1 : ι → ι → ο . wceq (cesum x0 x1) (cuni (co (co cxrs (co cc0 cpnf cicc) cress) (cmpt x0 x1) ctsu)) (proof)
Theorem df_ofc : ∀ x0 : ι → ο . wceq (cofc x0) (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cdm (cv x1)) (λ x3 . co (cfv (cv x3) (cv x1)) (cv x2) x0))) (proof)
Theorem df_siga : wceq csiga (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wss (cv x1) (cpw (cv x0))) (w3a (wcel (cv x0) (cv x1)) (wral (λ x2 . wcel (cdif (cv x0) (cv x2)) (cv x1)) (λ x2 . cv x1)) (wral (λ x2 . wbr (cv x2) com cdom ⟶ wcel (cuni (cv x2)) (cv x1)) (λ x2 . cpw (cv x1))))))) (proof)
Theorem df_sigagen : wceq csigagen (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wss (cv x0) (cv x1)) (λ x1 . cfv (cuni (cv x0)) csiga)))) (proof)
Theorem df_brsiga : wceq cbrsiga (cfv (cfv (crn cioo) ctg) csigagen) (proof)