Proofgold Address

Known df_ch__df_oc__df_ch0__df_shs__df_span__df_chj__df_chsup__df_pjh__df_cm__df_hosum__df_homul__df_hodif__df_hfsum__df_hfmul__df_h0op__df_iop__df_nmop__df_cnop : ∀ x0 : ο . (wceq cch (crab (λ x1 . wss (cima chli (co (cv x1) cn cmap)) (cv x1)) (λ x1 . csh)) ⟶ wceq cort (cmpt (λ x1 . cpw chil) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) csp) cc0) (λ x3 . cv x1)) (λ x2 . chil))) ⟶ wceq c0h (csn c0v) ⟶ wceq cph (cmpt2 (λ x1 x2 . csh) (λ x1 x2 . csh) (λ x1 x2 . cima cva (cxp (cv x1) (cv x2)))) ⟶ wceq cspn (cmpt (λ x1 . cpw chil) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . csh)))) ⟶ wceq chj (cmpt2 (λ x1 x2 . cpw chil) (λ x1 x2 . cpw chil) (λ x1 x2 . cfv (cfv (cun (cv x1) (cv x2)) cort) cort)) ⟶ wceq chsup (cmpt (λ x1 . cpw (cpw chil)) (λ x1 . cfv (cfv (cuni (cv x1)) cort) cort)) ⟶ wceq cpjh (cmpt (λ x1 . cch) (λ x1 . cmpt (λ x2 . chil) (λ x2 . crio (λ x3 . wrex (λ x4 . wceq (cv x2) (co (cv x3) (cv x4) cva)) (λ x4 . cfv (cv x1) cort)) (λ x3 . cv x1)))) ⟶ wceq ccm (copab (λ x1 x2 . wa (wa (wcel (cv x1) cch) (wcel (cv x2) cch)) (wceq (cv x1) (co (cin (cv x1) (cv x2)) (cin (cv x1) (cfv (cv x2) cort)) chj)))) ⟶ wceq chos (cmpt2 (λ x1 x2 . co chil chil cmap) (λ x1 x2 . co chil chil cmap) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cva))) ⟶ wceq chot (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . co chil chil cmap) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (cv x1) (cfv (cv x3) (cv x2)) csm))) ⟶ wceq chod (cmpt2 (λ x1 x2 . co chil chil cmap) (λ x1 x2 . co chil chil cmap) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cmv))) ⟶ wceq chfs (cmpt2 (λ x1 x2 . co cc chil cmap) (λ x1 x2 . co cc chil cmap) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) caddc))) ⟶ wceq chft (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . co cc chil cmap) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (cv x1) (cfv (cv x3) (cv x2)) cmul))) ⟶ wceq ch0o (cfv c0h cpjh) ⟶ wceq chio (cfv chil cpjh) ⟶ wceq cnop (cmpt (λ x1 . co chil chil cmap) (λ x1 . csup (cab (λ x2 . wrex (λ x3 . wa (wbr (cfv (cv x3) cno) c1 cle) (wceq (cv x2) (cfv (cfv (cv x3) (cv x1)) cno))) (λ x3 . chil))) cxr clt)) ⟶ wceq ccop (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wral (λ x5 . wbr (cfv (co (cv x5) (cv x2) cmv) cno) (cv x4) clt ⟶ wbr (cfv (co (cfv (cv x5) (cv x1)) (cfv (cv x2) (cv x1)) cmv) cno) (cv x3) clt) (λ x5 . chil)) (λ x4 . crp)) (λ x3 . crp)) (λ x2 . chil)) (λ x1 . co chil chil cmap)) ⟶ x0) ⟶ x0
Theorem df_ch : wceq cch (crab (λ x0 . wss (cima chli (co (cv x0) cn cmap)) (cv x0)) (λ x0 . csh)) (proof)
Theorem df_oc : wceq cort (cmpt (λ x0 . cpw chil) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) csp) cc0) (λ x2 . cv x0)) (λ x1 . chil))) (proof)
Theorem df_ch0 : wceq c0h (csn c0v) (proof)
Theorem df_shs : wceq cph (cmpt2 (λ x0 x1 . csh) (λ x0 x1 . csh) (λ x0 x1 . cima cva (cxp (cv x0) (cv x1)))) (proof)
Theorem df_span : wceq cspn (cmpt (λ x0 . cpw chil) (λ x0 . cint (crab (λ x1 . wss (cv x0) (cv x1)) (λ x1 . csh)))) (proof)
Theorem df_chj : wceq chj (cmpt2 (λ x0 x1 . cpw chil) (λ x0 x1 . cpw chil) (λ x0 x1 . cfv (cfv (cun (cv x0) (cv x1)) cort) cort)) (proof)
Theorem df_chsup : wceq chsup (cmpt (λ x0 . cpw (cpw chil)) (λ x0 . cfv (cfv (cuni (cv x0)) cort) cort)) (proof)
Theorem df_pjh : wceq cpjh (cmpt (λ x0 . cch) (λ x0 . cmpt (λ x1 . chil) (λ x1 . crio (λ x2 . wrex (λ x3 . wceq (cv x1) (co (cv x2) (cv x3) cva)) (λ x3 . cfv (cv x0) cort)) (λ x2 . cv x0)))) (proof)
Theorem df_cm : wceq ccm (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wceq (cv x0) (co (cin (cv x0) (cv x1)) (cin (cv x0) (cfv (cv x1) cort)) chj)))) (proof)
Theorem df_hosum : wceq chos (cmpt2 (λ x0 x1 . co chil chil cmap) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cva))) (proof)
Theorem df_homul : wceq chot (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cv x0) (cfv (cv x2) (cv x1)) csm))) (proof)
Theorem df_hodif : wceq chod (cmpt2 (λ x0 x1 . co chil chil cmap) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cmv))) (proof)
Theorem df_hfsum : wceq chfs (cmpt2 (λ x0 x1 . co cc chil cmap) (λ x0 x1 . co cc chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) caddc))) (proof)
Theorem df_hfmul : wceq chft (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . co cc chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cv x0) (cfv (cv x2) (cv x1)) cmul))) (proof)
Theorem df_h0op : wceq ch0o (cfv c0h cpjh) (proof)
Theorem df_iop : wceq chio (cfv chil cpjh) (proof)
Theorem df_nmop : wceq cnop (cmpt (λ x0 . co chil chil cmap) (λ x0 . csup (cab (λ x1 . wrex (λ x2 . wa (wbr (cfv (cv x2) cno) c1 cle) (wceq (cv x1) (cfv (cfv (cv x2) (cv x0)) cno))) (λ x2 . chil))) cxr clt)) (proof)
Theorem df_cnop : wceq ccop (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (co (cv x4) (cv x1) cmv) cno) (cv x3) clt ⟶ wbr (cfv (co (cfv (cv x4) (cv x0)) (cfv (cv x1) (cv x0)) cmv) cno) (cv x2) clt) (λ x4 . chil)) (λ x3 . crp)) (λ x2 . crp)) (λ x1 . chil)) (λ x0 . co chil chil cmap)) (proof)