Proofgold Address

Known df_mpl__df_ltbag__df_opsr__df_evls__df_evl__df_mhp__df_psd__df_selv__df_algind__df_psr1__df_vr1__df_ply1__df_coe1__df_toply1__df_evls1__df_evl1__df_psmet__df_xmet : ∀ x0 : ο . (wceq cmpl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (co (cv x1) (cv x2) cmps) (λ x3 . co (cv x3) (crab (λ x4 . wbr (cv x4) (cfv (cv x2) c0g) cfsupp) (λ x4 . cfv (cv x3) cbs)) cress))) ⟶ wceq cltb (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x2) cmap))) (wrex (λ x5 . wa (wbr (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)) clt) (wral (λ x6 . wbr (cv x5) (cv x6) (cv x1) ⟶ wceq (cfv (cv x6) (cv x3)) (cfv (cv x6) (cv x4))) (λ x6 . cv x2))) (λ x5 . cv x2))))) ⟶ wceq copws (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cpw (cxp (cv x1) (cv x1))) (λ x3 . csb (co (cv x1) (cv x2) cmps) (λ x4 . co (cv x4) (cop (cfv cnx cple) (copab (λ x5 x6 . wa (wss (cpr (cv x5) (cv x6)) (cfv (cv x4) cbs)) (wo (wsbc (λ x7 . wrex (λ x8 . wa (wbr (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6)) (cfv (cv x2) cplt)) (wral (λ x9 . wbr (cv x9) (cv x8) (co (cv x3) (cv x1) cltb) ⟶ wceq (cfv (cv x9) (cv x5)) (cfv (cv x9) (cv x6))) (λ x9 . cv x7))) (λ x8 . cv x7)) (crab (λ x7 . wcel (cima (ccnv (cv x7)) cn) cfn) (λ x7 . co cn0 (cv x1) cmap))) (wceq (cv x5) (cv x6)))))) csts)))) ⟶ wceq ces (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . ccrg) (λ x1 x2 . csb (cfv (cv x2) cbs) (λ x3 . cmpt (λ x4 . cfv (cv x2) csubrg) (λ x4 . csb (co (cv x1) (co (cv x2) (cv x4) cress) cmpl) (λ x5 . crio (λ x6 . wa (wceq (ccom (cv x6) (cfv (cv x5) cascl)) (cmpt (λ x7 . cv x4) (λ x7 . cxp (co (cv x3) (cv x1) cmap) (csn (cv x7))))) (wceq (ccom (cv x6) (co (cv x1) (co (cv x2) (cv x4) cress) cmvr)) (cmpt (λ x7 . cv x1) (λ x7 . cmpt (λ x8 . co (cv x3) (cv x1) cmap) (λ x8 . cfv (cv x7) (cv x8)))))) (λ x6 . co (cv x5) (co (cv x2) (co (cv x3) (cv x1) cmap) cpws) crh)))))) ⟶ wceq cevl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cfv (cfv (cv x2) cbs) (co (cv x1) (cv x2) ces))) ⟶ wceq cmhp (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cn0) (λ x3 . crab (λ x4 . wss (co (cv x4) (cfv (cv x2) c0g) csupp) (crab (λ x5 . wceq (csu cn0 (λ x6 . cfv (cv x6) (cv x5))) (cv x3)) (λ x5 . crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x1) cmap)))) (λ x4 . cfv (co (cv x1) (cv x2) cmpl) cbs)))) ⟶ wceq cpsd (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cv x1) (λ x3 . cmpt (λ x4 . cfv (co (cv x1) (cv x2) cmps) cbs) (λ x4 . cmpt (λ x5 . crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x1) cmap)) (λ x5 . co (co (cfv (cv x3) (cv x5)) c1 caddc) (cfv (co (cv x5) (cmpt (λ x6 . cv x1) (λ x6 . cif (wceq (cv x6) (cv x3)) c1 cc0)) (cof caddc)) (cv x4)) (cfv (cv x2) cmg)))))) ⟶ wceq cslv (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cpw (cv x1)) (λ x3 . cmpt (λ x4 . co (cv x1) (cv x2) cmpl) (λ x4 . csb (co (cdif (cv x1) (cv x3)) (cv x2) cmpl) (λ x5 . csb (cmpt (λ x6 . cfv (cv x5) csca) (λ x6 . co (cv x6) (cfv (cv x5) cur) (cfv (cv x5) cvsca))) (λ x6 . cfv (cmpt (λ x7 . cv x1) (λ x7 . cif (wcel (cv x7) (cv x3)) (cfv (cv x7) (co (cv x3) (co (cdif (cv x1) (cv x3)) (cv x2) cmpl) cmvr)) (ccom (cv x6) (cfv (cv x7) (co (cdif (cv x1) (cv x3)) (cv x2) cmvr))))) (cfv (ccom (cv x6) (cv x4)) (cfv (co (cv x6) (cv x2) cimas) (co (cv x1) (cv x5) ces))))))))) ⟶ wceq cai (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cpw (cfv (cv x1) cbs)) (λ x1 x2 . crab (λ x3 . wfun (ccnv (cmpt (λ x4 . cfv (co (cv x3) (co (cv x1) (cv x2) cress) cmpl) cbs) (λ x4 . cfv (cres cid (cv x3)) (cfv (cv x4) (cfv (cv x2) (co (cv x3) (cv x1) ces))))))) (λ x3 . cpw (cfv (cv x1) cbs)))) ⟶ wceq cps1 (cmpt (λ x1 . cvv) (λ x1 . cfv c0 (co c1o (cv x1) copws))) ⟶ wceq cv1 (cmpt (λ x1 . cvv) (λ x1 . cfv c0 (co c1o (cv x1) cmvr))) ⟶ wceq cpl1 (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cps1) (cfv (co c1o (cv x1) cmpl) cbs) cress)) ⟶ wceq cco1 (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cn0) (λ x2 . cfv (cxp c1o (csn (cv x2))) (cv x1)))) ⟶ wceq ctp1 (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . co cn0 c1o cmap) (λ x2 . cfv (cfv c0 (cv x2)) (cv x1)))) ⟶ wceq ces1 (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cpw (cfv (cv x1) cbs)) (λ x1 x2 . csb (cfv (cv x1) cbs) (λ x3 . ccom (cmpt (λ x4 . co (cv x3) (co (cv x3) c1o cmap) cmap) (λ x4 . ccom (cv x4) (cmpt (λ x5 . cv x3) (λ x5 . cxp c1o (csn (cv x5)))))) (cfv (cv x2) (co c1o (cv x1) ces))))) ⟶ wceq ce1 (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . ccom (cmpt (λ x3 . co (cv x2) (co (cv x2) c1o cmap) cmap) (λ x3 . ccom (cv x3) (cmpt (λ x4 . cv x2) (λ x4 . cxp c1o (csn (cv x4)))))) (co c1o (cv x1) cevl)))) ⟶ wceq cpsmet (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wa (wceq (co (cv x3) (cv x3) (cv x2)) cc0) (wral (λ x4 . wral (λ x5 . wbr (co (cv x3) (cv x4) (cv x2)) (co (co (cv x5) (cv x3) (cv x2)) (co (cv x5) (cv x4) (cv x2)) cxad) cle) (λ x5 . cv x1)) (λ x4 . cv x1))) (λ x3 . cv x1)) (λ x2 . co cxr (cxp (cv x1) (cv x1)) cmap))) ⟶ wceq cxmt (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wa (wb (wceq (co (cv x3) (cv x4) (cv x2)) cc0) (wceq (cv x3) (cv x4))) (wral (λ x5 . wbr (co (cv x3) (cv x4) (cv x2)) (co (co (cv x5) (cv x3) (cv x2)) (co (cv x5) (cv x4) (cv x2)) cxad) cle) (λ x5 . cv x1))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . co cxr (cxp (cv x1) (cv x1)) cmap))) ⟶ x0) ⟶ x0
Theorem df_mpl : wceq cmpl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmps) (λ x2 . co (cv x2) (crab (λ x3 . wbr (cv x3) (cfv (cv x1) c0g) cfsupp) (λ x3 . cfv (cv x2) cbs)) cress))) (proof)
Theorem df_ltbag : wceq cltb (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (crab (λ x4 . wcel (cima (ccnv (cv x4)) cn) cfn) (λ x4 . co cn0 (cv x1) cmap))) (wrex (λ x4 . wa (wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) clt) (wral (λ x5 . wbr (cv x4) (cv x5) (cv x0) ⟶ wceq (cfv (cv x5) (cv x2)) (cfv (cv x5) (cv x3))) (λ x5 . cv x1))) (λ x4 . cv x1))))) (proof)
Theorem df_opsr : wceq copws (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cpw (cxp (cv x0) (cv x0))) (λ x2 . csb (co (cv x0) (cv x1) cmps) (λ x3 . co (cv x3) (cop (cfv cnx cple) (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cfv (cv x3) cbs)) (wo (wsbc (λ x6 . wrex (λ x7 . wa (wbr (cfv (cv x7) (cv x4)) (cfv (cv x7) (cv x5)) (cfv (cv x1) cplt)) (wral (λ x8 . wbr (cv x8) (cv x7) (co (cv x2) (cv x0) cltb) ⟶ wceq (cfv (cv x8) (cv x4)) (cfv (cv x8) (cv x5))) (λ x8 . cv x6))) (λ x7 . cv x6)) (crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x0) cmap))) (wceq (cv x4) (cv x5)))))) csts)))) (proof)
Theorem df_evls : wceq ces (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . ccrg) (λ x0 x1 . csb (cfv (cv x1) cbs) (λ x2 . cmpt (λ x3 . cfv (cv x1) csubrg) (λ x3 . csb (co (cv x0) (co (cv x1) (cv x3) cress) cmpl) (λ x4 . crio (λ x5 . wa (wceq (ccom (cv x5) (cfv (cv x4) cascl)) (cmpt (λ x6 . cv x3) (λ x6 . cxp (co (cv x2) (cv x0) cmap) (csn (cv x6))))) (wceq (ccom (cv x5) (co (cv x0) (co (cv x1) (cv x3) cress) cmvr)) (cmpt (λ x6 . cv x0) (λ x6 . cmpt (λ x7 . co (cv x2) (cv x0) cmap) (λ x7 . cfv (cv x6) (cv x7)))))) (λ x5 . co (cv x4) (co (cv x1) (co (cv x2) (cv x0) cmap) cpws) crh)))))) (proof)
Theorem df_evl : wceq cevl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (cfv (cv x1) cbs) (co (cv x0) (cv x1) ces))) (proof)
Theorem df_mhp : wceq cmhp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cn0) (λ x2 . crab (λ x3 . wss (co (cv x3) (cfv (cv x1) c0g) csupp) (crab (λ x4 . wceq (csu cn0 (λ x5 . cfv (cv x5) (cv x4))) (cv x2)) (λ x4 . crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x0) cmap)))) (λ x3 . cfv (co (cv x0) (cv x1) cmpl) cbs)))) (proof)
Theorem df_psd : wceq cpsd (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x0) (λ x2 . cmpt (λ x3 . cfv (co (cv x0) (cv x1) cmps) cbs) (λ x3 . cmpt (λ x4 . crab (λ x5 . wcel (cima (ccnv (cv x5)) cn) cfn) (λ x5 . co cn0 (cv x0) cmap)) (λ x4 . co (co (cfv (cv x2) (cv x4)) c1 caddc) (cfv (co (cv x4) (cmpt (λ x5 . cv x0) (λ x5 . cif (wceq (cv x5) (cv x2)) c1 cc0)) (cof caddc)) (cv x3)) (cfv (cv x1) cmg)))))) (proof)
Theorem df_selv : wceq cslv (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cpw (cv x0)) (λ x2 . cmpt (λ x3 . co (cv x0) (cv x1) cmpl) (λ x3 . csb (co (cdif (cv x0) (cv x2)) (cv x1) cmpl) (λ x4 . csb (cmpt (λ x5 . cfv (cv x4) csca) (λ x5 . co (cv x5) (cfv (cv x4) cur) (cfv (cv x4) cvsca))) (λ x5 . cfv (cmpt (λ x6 . cv x0) (λ x6 . cif (wcel (cv x6) (cv x2)) (cfv (cv x6) (co (cv x2) (co (cdif (cv x0) (cv x2)) (cv x1) cmpl) cmvr)) (ccom (cv x5) (cfv (cv x6) (co (cdif (cv x0) (cv x2)) (cv x1) cmvr))))) (cfv (ccom (cv x5) (cv x3)) (cfv (co (cv x5) (cv x1) cimas) (co (cv x0) (cv x4) ces))))))))) (proof)
Theorem df_algind : wceq cai (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . crab (λ x2 . wfun (ccnv (cmpt (λ x3 . cfv (co (cv x2) (co (cv x0) (cv x1) cress) cmpl) cbs) (λ x3 . cfv (cres cid (cv x2)) (cfv (cv x3) (cfv (cv x1) (co (cv x2) (cv x0) ces))))))) (λ x2 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_psr1 : wceq cps1 (cmpt (λ x0 . cvv) (λ x0 . cfv c0 (co c1o (cv x0) copws))) (proof)
Theorem df_vr1 : wceq cv1 (cmpt (λ x0 . cvv) (λ x0 . cfv c0 (co c1o (cv x0) cmvr))) (proof)
Theorem df_ply1 : wceq cpl1 (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cps1) (cfv (co c1o (cv x0) cmpl) cbs) cress)) (proof)
Theorem df_coe1 : wceq cco1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cn0) (λ x1 . cfv (cxp c1o (csn (cv x1))) (cv x0)))) (proof)
Theorem df_toply1 : wceq ctp1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co cn0 c1o cmap) (λ x1 . cfv (cfv c0 (cv x1)) (cv x0)))) (proof)
Theorem df_evls1 : wceq ces1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . ccom (cmpt (λ x3 . co (cv x2) (co (cv x2) c1o cmap) cmap) (λ x3 . ccom (cv x3) (cmpt (λ x4 . cv x2) (λ x4 . cxp c1o (csn (cv x4)))))) (cfv (cv x1) (co c1o (cv x0) ces))))) (proof)
Theorem df_evl1 : wceq ce1 (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . ccom (cmpt (λ x2 . co (cv x1) (co (cv x1) c1o cmap) cmap) (λ x2 . ccom (cv x2) (cmpt (λ x3 . cv x1) (λ x3 . cxp c1o (csn (cv x3)))))) (co c1o (cv x0) cevl)))) (proof)
Theorem df_psmet : wceq cpsmet (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wceq (co (cv x2) (cv x2) (cv x1)) cc0) (wral (λ x3 . wral (λ x4 . wbr (co (cv x2) (cv x3) (cv x1)) (co (co (cv x4) (cv x2) (cv x1)) (co (cv x4) (cv x3) (cv x1)) cxad) cle) (λ x4 . cv x0)) (λ x3 . cv x0))) (λ x2 . cv x0)) (λ x1 . co cxr (cxp (cv x0) (cv x0)) cmap))) (proof)
Theorem df_xmet : wceq cxmt (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wa (wb (wceq (co (cv x2) (cv x3) (cv x1)) cc0) (wceq (cv x2) (cv x3))) (wral (λ x4 . wbr (co (cv x2) (cv x3) (cv x1)) (co (co (cv x4) (cv x2) (cv x1)) (co (cv x4) (cv x3) (cv x1)) cxad) cle) (λ x4 . cv x0))) (λ x3 . cv x0)) (λ x2 . cv x0)) (λ x1 . co cxr (cxp (cv x0) (cv x0)) cmap))) (proof)