Proofgold Address

Known df_mpq__df_ltpq__df_enq__df_nq__df_erq__df_plq__df_mq__df_1nq__df_rq__df_ltnq__df_np__df_1p__df_plp__df_mp__df_ltp__df_enr__df_nr__df_plr : ∀ x0 : ο . (wceq cmpq (cmpt2 (λ x1 x2 . cxp cnpi cnpi) (λ x1 x2 . cxp cnpi cnpi) (λ x1 x2 . cop (co (cfv (cv x1) c1st) (cfv (cv x2) c1st) cmi) (co (cfv (cv x1) c2nd) (cfv (cv x2) c2nd) cmi))) ⟶ wceq cltpq (copab (λ x1 x2 . wa (wa (wcel (cv x1) (cxp cnpi cnpi)) (wcel (cv x2) (cxp cnpi cnpi))) (wbr (co (cfv (cv x1) c1st) (cfv (cv x2) c2nd) cmi) (co (cfv (cv x2) c1st) (cfv (cv x1) c2nd) cmi) clti))) ⟶ wceq ceq (copab (λ x1 x2 . wa (wa (wcel (cv x1) (cxp cnpi cnpi)) (wcel (cv x2) (cxp cnpi cnpi))) (wex (λ x3 . wex (λ x4 . wex (λ x5 . wex (λ x6 . wa (wa (wceq (cv x1) (cop (cv x3) (cv x4))) (wceq (cv x2) (cop (cv x5) (cv x6)))) (wceq (co (cv x3) (cv x6) cmi) (co (cv x4) (cv x5) cmi))))))))) ⟶ wceq cnq (crab (λ x1 . wral (λ x2 . wbr (cv x1) (cv x2) ceq ⟶ wn (wbr (cfv (cv x2) c2nd) (cfv (cv x1) c2nd) clti)) (λ x2 . cxp cnpi cnpi)) (λ x1 . cxp cnpi cnpi)) ⟶ wceq cerq (cin ceq (cxp (cxp cnpi cnpi) cnq)) ⟶ wceq cplq (cres (ccom cerq cplpq) (cxp cnq cnq)) ⟶ wceq cmq (cres (ccom cerq cmpq) (cxp cnq cnq)) ⟶ wceq c1q (cop c1o c1o) ⟶ wceq crq (cima (ccnv cmq) (csn c1q)) ⟶ wceq cltq (cin cltpq (cxp cnq cnq)) ⟶ wceq cnp (cab (λ x1 . wa (wa (wpss c0 (cv x1)) (wpss (cv x1) cnq)) (wral (λ x2 . wa (∀ x3 . wbr (cv x3) (cv x2) cltq ⟶ wcel (cv x3) (cv x1)) (wrex (λ x3 . wbr (cv x2) (cv x3) cltq) (λ x3 . cv x1))) (λ x2 . cv x1)))) ⟶ wceq c1p (cab (λ x1 . wbr (cv x1) c1q cltq)) ⟶ wceq cpp (cmpt2 (λ x1 x2 . cnp) (λ x1 x2 . cnp) (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) cplq)) (λ x5 . cv x2)) (λ x4 . cv x1)))) ⟶ wceq cmp (cmpt2 (λ x1 x2 . cnp) (λ x1 x2 . cnp) (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) cmq)) (λ x5 . cv x2)) (λ x4 . cv x1)))) ⟶ wceq cltp (copab (λ x1 x2 . wa (wa (wcel (cv x1) cnp) (wcel (cv x2) cnp)) (wpss (cv x1) (cv x2)))) ⟶ wceq cer (copab (λ x1 x2 . wa (wa (wcel (cv x1) (cxp cnp cnp)) (wcel (cv x2) (cxp cnp cnp))) (wex (λ x3 . wex (λ x4 . wex (λ x5 . wex (λ x6 . wa (wa (wceq (cv x1) (cop (cv x3) (cv x4))) (wceq (cv x2) (cop (cv x5) (cv x6)))) (wceq (co (cv x3) (cv x6) cpp) (co (cv x4) (cv x5) cpp))))))))) ⟶ wceq cnr (cqs (cxp cnp cnp) cer) ⟶ wceq cplr (coprab (λ x1 x2 x3 . wa (wa (wcel (cv x1) cnr) (wcel (cv x2) cnr)) (wex (λ x4 . wex (λ x5 . wex (λ x6 . wex (λ x7 . wa (wa (wceq (cv x1) (cec (cop (cv x4) (cv x5)) cer)) (wceq (cv x2) (cec (cop (cv x6) (cv x7)) cer))) (wceq (cv x3) (cec (cop (co (cv x4) (cv x6) cpp) (co (cv x5) (cv x7) cpp)) cer))))))))) ⟶ x0) ⟶ x0
Theorem df_mpq : wceq cmpq (cmpt2 (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cop (co (cfv (cv x0) c1st) (cfv (cv x1) c1st) cmi) (co (cfv (cv x0) c2nd) (cfv (cv x1) c2nd) cmi))) (proof)
Theorem df_ltpq : wceq cltpq (copab (λ x0 x1 . wa (wa (wcel (cv x0) (cxp cnpi cnpi)) (wcel (cv x1) (cxp cnpi cnpi))) (wbr (co (cfv (cv x0) c1st) (cfv (cv x1) c2nd) cmi) (co (cfv (cv x1) c1st) (cfv (cv x0) c2nd) cmi) clti))) (proof)
Theorem df_enq : wceq ceq (copab (λ x0 x1 . wa (wa (wcel (cv x0) (cxp cnpi cnpi)) (wcel (cv x1) (cxp cnpi cnpi))) (wex (λ x2 . wex (λ x3 . wex (λ x4 . wex (λ x5 . wa (wa (wceq (cv x0) (cop (cv x2) (cv x3))) (wceq (cv x1) (cop (cv x4) (cv x5)))) (wceq (co (cv x2) (cv x5) cmi) (co (cv x3) (cv x4) cmi))))))))) (proof)
Theorem df_nq : wceq cnq (crab (λ x0 . wral (λ x1 . wbr (cv x0) (cv x1) ceq ⟶ wn (wbr (cfv (cv x1) c2nd) (cfv (cv x0) c2nd) clti)) (λ x1 . cxp cnpi cnpi)) (λ x0 . cxp cnpi cnpi)) (proof)
Theorem df_erq : wceq cerq (cin ceq (cxp (cxp cnpi cnpi) cnq)) (proof)
Theorem df_plq : wceq cplq (cres (ccom cerq cplpq) (cxp cnq cnq)) (proof)
Theorem df_mq : wceq cmq (cres (ccom cerq cmpq) (cxp cnq cnq)) (proof)
Theorem df_1nq : wceq c1q (cop c1o c1o) (proof)
Theorem df_rq : wceq crq (cima (ccnv cmq) (csn c1q)) (proof)
Theorem df_ltnq : wceq cltq (cin cltpq (cxp cnq cnq)) (proof)
Theorem df_np : wceq cnp (cab (λ x0 . wa (wa (wpss c0 (cv x0)) (wpss (cv x0) cnq)) (wral (λ x1 . wa (∀ x2 . wbr (cv x2) (cv x1) cltq ⟶ wcel (cv x2) (cv x0)) (wrex (λ x2 . wbr (cv x1) (cv x2) cltq) (λ x2 . cv x0))) (λ x1 . cv x0)))) (proof)
Theorem df_1p : wceq c1p (cab (λ x0 . wbr (cv x0) c1q cltq)) (proof)
Theorem df_plp : wceq cpp (cmpt2 (λ x0 x1 . cnp) (λ x0 x1 . cnp) (λ x0 x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (co (cv x3) (cv x4) cplq)) (λ x4 . cv x1)) (λ x3 . cv x0)))) (proof)
Theorem df_mp : wceq cmp (cmpt2 (λ x0 x1 . cnp) (λ x0 x1 . cnp) (λ x0 x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (co (cv x3) (cv x4) cmq)) (λ x4 . cv x1)) (λ x3 . cv x0)))) (proof)
Theorem df_ltp : wceq cltp (copab (λ x0 x1 . wa (wa (wcel (cv x0) cnp) (wcel (cv x1) cnp)) (wpss (cv x0) (cv x1)))) (proof)
Theorem df_enr : wceq cer (copab (λ x0 x1 . wa (wa (wcel (cv x0) (cxp cnp cnp)) (wcel (cv x1) (cxp cnp cnp))) (wex (λ x2 . wex (λ x3 . wex (λ x4 . wex (λ x5 . wa (wa (wceq (cv x0) (cop (cv x2) (cv x3))) (wceq (cv x1) (cop (cv x4) (cv x5)))) (wceq (co (cv x2) (cv x5) cpp) (co (cv x3) (cv x4) cpp))))))))) (proof)
Theorem df_nr : wceq cnr (cqs (cxp cnp cnp) cer) (proof)
Theorem df_plr : wceq cplr (coprab (λ x0 x1 x2 . wa (wa (wcel (cv x0) cnr) (wcel (cv x1) cnr)) (wex (λ x3 . wex (λ x4 . wex (λ x5 . wex (λ x6 . wa (wa (wceq (cv x0) (cec (cop (cv x3) (cv x4)) cer)) (wceq (cv x1) (cec (cop (cv x5) (cv x6)) cer))) (wceq (cv x2) (cec (cop (co (cv x3) (cv x5) cpp) (co (cv x4) (cv x6) cpp)) cer))))))))) (proof)