Proofgold Address

Known df_sca__df_vsca__df_ip__df_tset__df_ple__df_ocomp__df_ds__df_unif__df_hom__df_cco__df_rest__df_topn__df_0g__df_gsum__df_topgen__df_pt__df_prds__df_pws : ∀ x0 : ο . (wceq csca (cslot c5) ⟶ wceq cvsca (cslot c6) ⟶ wceq cip (cslot c8) ⟶ wceq cts (cslot c9) ⟶ wceq cple (cslot (cdc c1 cc0)) ⟶ wceq coc (cslot (cdc c1 c1)) ⟶ wceq cds (cslot (cdc c1 c2)) ⟶ wceq cunif (cslot (cdc c1 c3)) ⟶ wceq chom (cslot (cdc c1 c4)) ⟶ wceq cco (cslot (cdc c1 c5)) ⟶ wceq crest (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crn (cmpt (λ x3 . cv x1) (λ x3 . cin (cv x3) (cv x2))))) ⟶ wceq ctopn (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cts) (cfv (cv x1) cbs) crest)) ⟶ wceq c0g (cmpt (λ x1 . cvv) (λ x1 . cio (λ x2 . wa (wcel (cv x2) (cfv (cv x1) cbs)) (wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cfv (cv x1) cplusg)) (cv x3)) (wceq (co (cv x3) (cv x2) (cfv (cv x1) cplusg)) (cv x3))) (λ x3 . cfv (cv x1) cbs))))) ⟶ wceq cgsu (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (crab (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x4)) (wceq (co (cv x4) (cv x3) (cfv (cv x1) cplusg)) (cv x4))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs)) (λ x3 . cif (wss (crn (cv x2)) (cv x3)) (cfv (cv x1) c0g) (cif (wcel (cdm (cv x2)) (crn cfz)) (cio (λ x4 . wex (λ x5 . wrex (λ x6 . wa (wceq (cdm (cv x2)) (co (cv x5) (cv x6) cfz)) (wceq (cv x4) (cfv (cv x6) (cseq (cfv (cv x1) cplusg) (cv x2) (cv x5))))) (λ x6 . cfv (cv x5) cuz)))) (cio (λ x4 . wex (λ x5 . wsbc (λ x6 . wa (wf1o (co c1 (cfv (cv x6) chash) cfz) (cv x6) (cv x5)) (wceq (cv x4) (cfv (cfv (cv x6) chash) (cseq (cfv (cv x1) cplusg) (ccom (cv x2) (cv x5)) c1)))) (cima (ccnv (cv x2)) (cdif cvv (cv x3)))))))))) ⟶ wceq ctg (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wss (cv x2) (cuni (cin (cv x1) (cpw (cv x2))))))) ⟶ wceq cpt (cmpt (λ x1 . cvv) (λ x1 . cfv (cab (λ x2 . wex (λ x3 . wa (w3a (wfn (cv x3) (cdm (cv x1))) (wral (λ x4 . wcel (cfv (cv x4) (cv x3)) (cfv (cv x4) (cv x1))) (λ x4 . cdm (cv x1))) (wrex (λ x4 . wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (cuni (cfv (cv x5) (cv x1)))) (λ x5 . cdif (cdm (cv x1)) (cv x4))) (λ x4 . cfn))) (wceq (cv x2) (cixp (λ x4 . cdm (cv x1)) (λ x4 . cfv (cv x4) (cv x3))))))) ctg)) ⟶ wceq cprds (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cixp (λ x3 . cdm (cv x2)) (λ x3 . cfv (cfv (cv x3) (cv x2)) cbs)) (λ x3 . csb (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cixp (λ x6 . cdm (cv x2)) (λ x6 . co (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x2)) chom)))) (λ x4 . cun (cun (ctp (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx cplusg) (cmpt2 (λ x5 x6 . cv x3) (λ x5 x6 . cv x3) (λ x5 x6 . cmpt (λ x7 . cdm (cv x2)) (λ x7 . co (cfv (cv x7) (cv x5)) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x5 x6 . cv x3) (λ x5 x6 . cv x3) (λ x5 x6 . cmpt (λ x7 . cdm (cv x2)) (λ x7 . co (cfv (cv x7) (cv x5)) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cmulr)))))) (ctp (cop (cfv cnx csca) (cv x1)) (cop (cfv cnx cvsca) (cmpt2 (λ x5 x6 . cfv (cv x1) cbs) (λ x5 x6 . cv x3) (λ x5 x6 . cmpt (λ x7 . cdm (cv x2)) (λ x7 . co (cv x5) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cvsca))))) (cop (cfv cnx cip) (cmpt2 (λ x5 x6 . cv x3) (λ x5 x6 . cv x3) (λ x5 x6 . co (cv x1) (cmpt (λ x7 . cdm (cv x2)) (λ x7 . co (cfv (cv x7) (cv x5)) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cip))) cgsu))))) (cun (ctp (cop (cfv cnx cts) (cfv (ccom ctopn (cv x2)) cpt)) (cop (cfv cnx cple) (copab (λ x5 x6 . wa (wss (cpr (cv x5) (cv x6)) (cv x3)) (wral (λ x7 . wbr (cfv (cv x7) (cv x5)) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cple)) (λ x7 . cdm (cv x2)))))) (cop (cfv cnx cds) (cmpt2 (λ x5 x6 . cv x3) (λ x5 x6 . cv x3) (λ x5 x6 . csup (cun (crn (cmpt (λ x7 . cdm (cv x2)) (λ x7 . co (cfv (cv x7) (cv x5)) (cfv (cv x7) (cv x6)) (cfv (cfv (cv x7) (cv x2)) cds)))) (csn cc0)) cxr clt)))) (cpr (cop (cfv cnx chom) (cv x4)) (cop (cfv cnx cco) (cmpt2 (λ x5 x6 . cxp (cv x3) (cv x3)) (λ x5 x6 . cv x3) (λ x5 x6 . cmpt2 (λ x7 x8 . co (cv x6) (cfv (cv x5) c2nd) (cv x4)) (λ x7 x8 . cfv (cv x5) (cv x4)) (λ x7 x8 . cmpt (λ x9 . cdm (cv x2)) (λ x9 . co (cfv (cv x9) (cv x7)) (cfv (cv x9) (cv x8)) (co (cop (cfv (cv x9) (cfv (cv x5) c1st)) (cfv (cv x9) (cfv (cv x5) c2nd))) (cfv (cv x9) (cv x6)) (cfv (cfv (cv x9) (cv x2)) cco))))))))))))) ⟶ wceq cpws (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cfv (cv x1) csca) (cxp (cv x2) (csn (cv x1))) cprds)) ⟶ x0) ⟶ x0
Theorem df_sca : wceq csca (cslot c5) (proof)
Theorem df_vsca : wceq cvsca (cslot c6) (proof)
Theorem df_ip : wceq cip (cslot c8) (proof)
Theorem df_tset : wceq cts (cslot c9) (proof)
Theorem df_ple : wceq cple (cslot (cdc c1 cc0)) (proof)
Theorem df_ocomp : wceq coc (cslot (cdc c1 c1)) (proof)
Theorem df_ds : wceq cds (cslot (cdc c1 c2)) (proof)
Theorem df_unif : wceq cunif (cslot (cdc c1 c3)) (proof)
Theorem df_hom : wceq chom (cslot (cdc c1 c4)) (proof)
Theorem df_cco : wceq cco (cslot (cdc c1 c5)) (proof)
Theorem df_rest : wceq crest (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crn (cmpt (λ x2 . cv x0) (λ x2 . cin (cv x2) (cv x1))))) (proof)
Theorem df_topn : wceq ctopn (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cts) (cfv (cv x0) cbs) crest)) (proof)
Theorem df_0g : wceq c0g (cmpt (λ x0 . cvv) (λ x0 . cio (λ x1 . wa (wcel (cv x1) (cfv (cv x0) cbs)) (wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cfv (cv x0) cplusg)) (cv x2)) (wceq (co (cv x2) (cv x1) (cfv (cv x0) cplusg)) (cv x2))) (λ x2 . cfv (cv x0) cbs))))) (proof)
Theorem df_gsum : wceq cgsu (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (crab (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x3)) (wceq (co (cv x3) (cv x2) (cfv (cv x0) cplusg)) (cv x3))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs)) (λ x2 . cif (wss (crn (cv x1)) (cv x2)) (cfv (cv x0) c0g) (cif (wcel (cdm (cv x1)) (crn cfz)) (cio (λ x3 . wex (λ x4 . wrex (λ x5 . wa (wceq (cdm (cv x1)) (co (cv x4) (cv x5) cfz)) (wceq (cv x3) (cfv (cv x5) (cseq (cfv (cv x0) cplusg) (cv x1) (cv x4))))) (λ x5 . cfv (cv x4) cuz)))) (cio (λ x3 . wex (λ x4 . wsbc (λ x5 . wa (wf1o (co c1 (cfv (cv x5) chash) cfz) (cv x5) (cv x4)) (wceq (cv x3) (cfv (cfv (cv x5) chash) (cseq (cfv (cv x0) cplusg) (ccom (cv x1) (cv x4)) c1)))) (cima (ccnv (cv x1)) (cdif cvv (cv x2)))))))))) (proof)
Theorem df_topgen : wceq ctg (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wss (cv x1) (cuni (cin (cv x0) (cpw (cv x1))))))) (proof)
Theorem df_pt : wceq cpt (cmpt (λ x0 . cvv) (λ x0 . cfv (cab (λ x1 . wex (λ x2 . wa (w3a (wfn (cv x2) (cdm (cv x0))) (wral (λ x3 . wcel (cfv (cv x3) (cv x2)) (cfv (cv x3) (cv x0))) (λ x3 . cdm (cv x0))) (wrex (λ x3 . wral (λ x4 . wceq (cfv (cv x4) (cv x2)) (cuni (cfv (cv x4) (cv x0)))) (λ x4 . cdif (cdm (cv x0)) (cv x3))) (λ x3 . cfn))) (wceq (cv x1) (cixp (λ x3 . cdm (cv x0)) (λ x3 . cfv (cv x3) (cv x2))))))) ctg)) (proof)
Theorem df_prds : wceq cprds (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cixp (λ x2 . cdm (cv x1)) (λ x2 . cfv (cfv (cv x2) (cv x1)) cbs)) (λ x2 . csb (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cixp (λ x5 . cdm (cv x1)) (λ x5 . co (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)) (cfv (cfv (cv x5) (cv x1)) chom)))) (λ x3 . cun (cun (ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . cmpt (λ x6 . cdm (cv x1)) (λ x6 . co (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . cmpt (λ x6 . cdm (cv x1)) (λ x6 . co (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cmulr)))))) (ctp (cop (cfv cnx csca) (cv x0)) (cop (cfv cnx cvsca) (cmpt2 (λ x4 x5 . cfv (cv x0) cbs) (λ x4 x5 . cv x2) (λ x4 x5 . cmpt (λ x6 . cdm (cv x1)) (λ x6 . co (cv x4) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cvsca))))) (cop (cfv cnx cip) (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . co (cv x0) (cmpt (λ x6 . cdm (cv x1)) (λ x6 . co (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cip))) cgsu))))) (cun (ctp (cop (cfv cnx cts) (cfv (ccom ctopn (cv x1)) cpt)) (cop (cfv cnx cple) (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cv x2)) (wral (λ x6 . wbr (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cple)) (λ x6 . cdm (cv x1)))))) (cop (cfv cnx cds) (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . csup (cun (crn (cmpt (λ x6 . cdm (cv x1)) (λ x6 . co (cfv (cv x6) (cv x4)) (cfv (cv x6) (cv x5)) (cfv (cfv (cv x6) (cv x1)) cds)))) (csn cc0)) cxr clt)))) (cpr (cop (cfv cnx chom) (cv x3)) (cop (cfv cnx cco) (cmpt2 (λ x4 x5 . cxp (cv x2) (cv x2)) (λ x4 x5 . cv x2) (λ x4 x5 . cmpt2 (λ x6 x7 . co (cv x5) (cfv (cv x4) c2nd) (cv x3)) (λ x6 x7 . cfv (cv x4) (cv x3)) (λ x6 x7 . cmpt (λ x8 . cdm (cv x1)) (λ x8 . co (cfv (cv x8) (cv x6)) (cfv (cv x8) (cv x7)) (co (cop (cfv (cv x8) (cfv (cv x4) c1st)) (cfv (cv x8) (cfv (cv x4) c2nd))) (cfv (cv x8) (cv x5)) (cfv (cfv (cv x8) (cv x1)) cco))))))))))))) (proof)
Theorem df_pws : wceq cpws (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cfv (cv x0) csca) (cxp (cv x1) (csn (cv x0))) cprds)) (proof)