Proofgold Address

Known df_lnop__df_bdop__df_unop__df_hmop__df_nmfn__df_nlfn__df_cnfn__df_lnfn__df_adjh__df_bra__df_kb__df_leop__df_eigvec__df_eigval__df_spec__df_st__df_hst__df_cv : ∀ x0 : ο . (wceq clo (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cfv (co (co (cv x2) (cv x3) csm) (cv x4) cva) (cv x1)) (co (co (cv x2) (cfv (cv x3) (cv x1)) csm) (cfv (cv x4) (cv x1)) cva)) (λ x4 . chil)) (λ x3 . chil)) (λ x2 . cc)) (λ x1 . co chil chil cmap)) ⟶ wceq cbo (crab (λ x1 . wbr (cfv (cv x1) cnop) cpnf clt) (λ x1 . clo)) ⟶ wceq cuo (cab (λ x1 . wa (wfo chil chil (cv x1)) (wral (λ x2 . wral (λ x3 . wceq (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) csp) (co (cv x2) (cv x3) csp)) (λ x3 . chil)) (λ x2 . chil)))) ⟶ wceq cho (crab (λ x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cfv (cv x3) (cv x1)) csp) (co (cfv (cv x2) (cv x1)) (cv x3) csp)) (λ x3 . chil)) (λ x2 . chil)) (λ x1 . co chil chil cmap)) ⟶ wceq cnmf (cmpt (λ x1 . co cc 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)) cabs))) (λ x3 . chil))) cxr clt)) ⟶ wceq cnl (cmpt (λ x1 . co cc chil cmap) (λ x1 . cima (ccnv (cv x1)) (csn cc0))) ⟶ wceq ccnfn (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)) cmin) cabs) (cv x3) clt) (λ x5 . chil)) (λ x4 . crp)) (λ x3 . crp)) (λ x2 . chil)) (λ x1 . co cc chil cmap)) ⟶ wceq clf (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cfv (co (co (cv x2) (cv x3) csm) (cv x4) cva) (cv x1)) (co (co (cv x2) (cfv (cv x3) (cv x1)) cmul) (cfv (cv x4) (cv x1)) caddc)) (λ x4 . chil)) (λ x3 . chil)) (λ x2 . cc)) (λ x1 . co cc chil cmap)) ⟶ wceq cado (copab (λ x1 x2 . w3a (wf chil chil (cv x1)) (wf chil chil (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x1)) (cv x4) csp) (co (cv x3) (cfv (cv x4) (cv x2)) csp)) (λ x4 . chil)) (λ x3 . chil)))) ⟶ wceq cbr (cmpt (λ x1 . chil) (λ x1 . cmpt (λ x2 . chil) (λ x2 . co (cv x2) (cv x1) csp))) ⟶ wceq ck (cmpt2 (λ x1 x2 . chil) (λ x1 x2 . chil) (λ x1 x2 . cmpt (λ x3 . chil) (λ x3 . co (co (cv x3) (cv x2) csp) (cv x1) csm))) ⟶ wceq cleo (copab (λ x1 x2 . wa (wcel (co (cv x2) (cv x1) chod) cho) (wral (λ x3 . wbr cc0 (co (cfv (cv x3) (co (cv x2) (cv x1) chod)) (cv x3) csp) cle) (λ x3 . chil)))) ⟶ wceq cei (cmpt (λ x1 . co chil chil cmap) (λ x1 . crab (λ x2 . wrex (λ x3 . wceq (cfv (cv x2) (cv x1)) (co (cv x3) (cv x2) csm)) (λ x3 . cc)) (λ x2 . cdif chil c0h))) ⟶ wceq cel (cmpt (λ x1 . co chil chil cmap) (λ x1 . cmpt (λ x2 . cfv (cv x1) cei) (λ x2 . co (co (cfv (cv x2) (cv x1)) (cv x2) csp) (co (cfv (cv x2) cno) c2 cexp) cdiv))) ⟶ wceq cspc (cmpt (λ x1 . co chil chil cmap) (λ x1 . crab (λ x2 . wn (wf1 chil chil (co (cv x1) (co (cv x2) (cres cid chil) chot) chod))) (λ x2 . cc))) ⟶ wceq cst (crab (λ x1 . wa (wceq (cfv chil (cv x1)) c1) (wral (λ x2 . wral (λ x3 . wss (cv x2) (cfv (cv x3) cort) ⟶ wceq (cfv (co (cv x2) (cv x3) chj) (cv x1)) (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) caddc)) (λ x3 . cch)) (λ x2 . cch))) (λ x1 . co (co cc0 c1 cicc) cch cmap)) ⟶ wceq chst (crab (λ x1 . wa (wceq (cfv (cfv chil (cv x1)) cno) c1) (wral (λ x2 . wral (λ x3 . wss (cv x2) (cfv (cv x3) cort) ⟶ wa (wceq (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) csp) cc0) (wceq (cfv (co (cv x2) (cv x3) chj) (cv x1)) (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) cva))) (λ x3 . cch)) (λ x2 . cch))) (λ x1 . co chil cch cmap)) ⟶ wceq ccv (copab (λ x1 x2 . wa (wa (wcel (cv x1) cch) (wcel (cv x2) cch)) (wa (wpss (cv x1) (cv x2)) (wn (wrex (λ x3 . wa (wpss (cv x1) (cv x3)) (wpss (cv x3) (cv x2))) (λ x3 . cch)))))) ⟶ x0) ⟶ x0
Theorem df_lnop : wceq clo (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wceq (cfv (co (co (cv x1) (cv x2) csm) (cv x3) cva) (cv x0)) (co (co (cv x1) (cfv (cv x2) (cv x0)) csm) (cfv (cv x3) (cv x0)) cva)) (λ x3 . chil)) (λ x2 . chil)) (λ x1 . cc)) (λ x0 . co chil chil cmap)) (proof)
Theorem df_bdop : wceq cbo (crab (λ x0 . wbr (cfv (cv x0) cnop) cpnf clt) (λ x0 . clo)) (proof)
Theorem df_unop : wceq cuo (cab (λ x0 . wa (wfo chil chil (cv x0)) (wral (λ x1 . wral (λ x2 . wceq (co (cfv (cv x1) (cv x0)) (cfv (cv x2) (cv x0)) csp) (co (cv x1) (cv x2) csp)) (λ x2 . chil)) (λ x1 . chil)))) (proof)
Theorem df_hmop : wceq cho (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cfv (cv x2) (cv x0)) csp) (co (cfv (cv x1) (cv x0)) (cv x2) csp)) (λ x2 . chil)) (λ x1 . chil)) (λ x0 . co chil chil cmap)) (proof)
Theorem df_nmfn : wceq cnmf (cmpt (λ x0 . co cc 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)) cabs))) (λ x2 . chil))) cxr clt)) (proof)
Theorem df_nlfn : wceq cnl (cmpt (λ x0 . co cc chil cmap) (λ x0 . cima (ccnv (cv x0)) (csn cc0))) (proof)
Theorem df_cnfn : wceq ccnfn (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)) cmin) cabs) (cv x2) clt) (λ x4 . chil)) (λ x3 . crp)) (λ x2 . crp)) (λ x1 . chil)) (λ x0 . co cc chil cmap)) (proof)
Theorem df_lnfn : wceq clf (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wceq (cfv (co (co (cv x1) (cv x2) csm) (cv x3) cva) (cv x0)) (co (co (cv x1) (cfv (cv x2) (cv x0)) cmul) (cfv (cv x3) (cv x0)) caddc)) (λ x3 . chil)) (λ x2 . chil)) (λ x1 . cc)) (λ x0 . co cc chil cmap)) (proof)
Theorem df_adjh : wceq cado (copab (λ x0 x1 . w3a (wf chil chil (cv x0)) (wf chil chil (cv x1)) (wral (λ x2 . wral (λ x3 . wceq (co (cfv (cv x2) (cv x0)) (cv x3) csp) (co (cv x2) (cfv (cv x3) (cv x1)) csp)) (λ x3 . chil)) (λ x2 . chil)))) (proof)
Theorem df_bra : wceq cbr (cmpt (λ x0 . chil) (λ x0 . cmpt (λ x1 . chil) (λ x1 . co (cv x1) (cv x0) csp))) (proof)
Theorem df_kb : wceq ck (cmpt2 (λ x0 x1 . chil) (λ x0 x1 . chil) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (co (cv x2) (cv x1) csp) (cv x0) csm))) (proof)
Theorem df_leop : wceq cleo (copab (λ x0 x1 . wa (wcel (co (cv x1) (cv x0) chod) cho) (wral (λ x2 . wbr cc0 (co (cfv (cv x2) (co (cv x1) (cv x0) chod)) (cv x2) csp) cle) (λ x2 . chil)))) (proof)
Theorem df_eigvec : wceq cei (cmpt (λ x0 . co chil chil cmap) (λ x0 . crab (λ x1 . wrex (λ x2 . wceq (cfv (cv x1) (cv x0)) (co (cv x2) (cv x1) csm)) (λ x2 . cc)) (λ x1 . cdif chil c0h))) (proof)
Theorem df_eigval : wceq cel (cmpt (λ x0 . co chil chil cmap) (λ x0 . cmpt (λ x1 . cfv (cv x0) cei) (λ x1 . co (co (cfv (cv x1) (cv x0)) (cv x1) csp) (co (cfv (cv x1) cno) c2 cexp) cdiv))) (proof)
Theorem df_spec : wceq cspc (cmpt (λ x0 . co chil chil cmap) (λ x0 . crab (λ x1 . wn (wf1 chil chil (co (cv x0) (co (cv x1) (cres cid chil) chot) chod))) (λ x1 . cc))) (proof)
Theorem df_st : wceq cst (crab (λ x0 . wa (wceq (cfv chil (cv x0)) c1) (wral (λ x1 . wral (λ x2 . wss (cv x1) (cfv (cv x2) cort) ⟶ wceq (cfv (co (cv x1) (cv x2) chj) (cv x0)) (co (cfv (cv x1) (cv x0)) (cfv (cv x2) (cv x0)) caddc)) (λ x2 . cch)) (λ x1 . cch))) (λ x0 . co (co cc0 c1 cicc) cch cmap)) (proof)
Theorem df_hst : wceq chst (crab (λ x0 . wa (wceq (cfv (cfv chil (cv x0)) cno) c1) (wral (λ x1 . wral (λ x2 . wss (cv x1) (cfv (cv x2) cort) ⟶ wa (wceq (co (cfv (cv x1) (cv x0)) (cfv (cv x2) (cv x0)) csp) cc0) (wceq (cfv (co (cv x1) (cv x2) chj) (cv x0)) (co (cfv (cv x1) (cv x0)) (cfv (cv x2) (cv x0)) cva))) (λ x2 . cch)) (λ x1 . cch))) (λ x0 . co chil cch cmap)) (proof)
Theorem df_cv : wceq ccv (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wa (wpss (cv x0) (cv x1)) (wn (wrex (λ x2 . wa (wpss (cv x0) (cv x2)) (wpss (cv x2) (cv x1))) (λ x2 . cch)))))) (proof)