Proofgold Address

Known df_preset__df_drs__df_poset__df_plt__df_lub__df_glb__df_join__df_meet__df_toset__df_p0__df_p1__df_lat__df_clat__df_odu__df_ipo__df_dlat__df_ps__df_tsr : ∀ x0 : ο . (wceq cpreset (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wa (wbr (cv x4) (cv x4) (cv x3)) (wa (wbr (cv x4) (cv x5) (cv x3)) (wbr (cv x5) (cv x6) (cv x3)) ⟶ wbr (cv x4) (cv x6) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) cple)) (cfv (cv x1) cbs))) ⟶ wceq cdrs (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wne (cv x2) c0) (wral (λ x4 . wral (λ x5 . wrex (λ x6 . wa (wbr (cv x4) (cv x6) (cv x3)) (wbr (cv x5) (cv x6) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2))) (cfv (cv x1) cple)) (cfv (cv x1) cbs)) (λ x1 . cpreset)) ⟶ wceq cpo (cab (λ x1 . wex (λ x2 . wex (λ x3 . w3a (wceq (cv x2) (cfv (cv x1) cbs)) (wceq (cv x3) (cfv (cv x1) cple)) (wral (λ x4 . wral (λ x5 . wral (λ x6 . w3a (wbr (cv x4) (cv x4) (cv x3)) (wa (wbr (cv x4) (cv x5) (cv x3)) (wbr (cv x5) (cv x4) (cv x3)) ⟶ wceq (cv x4) (cv x5)) (wa (wbr (cv x4) (cv x5) (cv x3)) (wbr (cv x5) (cv x6) (cv x3)) ⟶ wbr (cv x4) (cv x6) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)))))) ⟶ wceq cplt (cmpt (λ x1 . cvv) (λ x1 . cdif (cfv (cv x1) cple) cid)) ⟶ wceq club (cmpt (λ x1 . cvv) (λ x1 . cres (cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . crio (λ x3 . wa (wral (λ x4 . wbr (cv x4) (cv x3) (cfv (cv x1) cple)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wbr (cv x5) (cv x4) (cfv (cv x1) cple)) (λ x5 . cv x2) ⟶ wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs))) (λ x3 . cfv (cv x1) cbs))) (cab (λ x2 . wreu (λ x3 . wa (wral (λ x4 . wbr (cv x4) (cv x3) (cfv (cv x1) cple)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wbr (cv x5) (cv x4) (cfv (cv x1) cple)) (λ x5 . cv x2) ⟶ wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs))) (λ x3 . cfv (cv x1) cbs))))) ⟶ wceq cglb (cmpt (λ x1 . cvv) (λ x1 . cres (cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . crio (λ x3 . wa (wral (λ x4 . wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wbr (cv x4) (cv x5) (cfv (cv x1) cple)) (λ x5 . cv x2) ⟶ wbr (cv x4) (cv x3) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs))) (λ x3 . cfv (cv x1) cbs))) (cab (λ x2 . wreu (λ x3 . wa (wral (λ x4 . wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wbr (cv x4) (cv x5) (cfv (cv x1) cple)) (λ x5 . cv x2) ⟶ wbr (cv x4) (cv x3) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs))) (λ x3 . cfv (cv x1) cbs))))) ⟶ wceq cjn (cmpt (λ x1 . cvv) (λ x1 . coprab (λ x2 x3 x4 . wbr (cpr (cv x2) (cv x3)) (cv x4) (cfv (cv x1) club)))) ⟶ wceq cmee (cmpt (λ x1 . cvv) (λ x1 . coprab (λ x2 x3 x4 . wbr (cpr (cv x2) (cv x3)) (cv x4) (cfv (cv x1) cglb)))) ⟶ wceq ctos (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wo (wbr (cv x4) (cv x5) (cv x3)) (wbr (cv x5) (cv x4) (cv x3))) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) cple)) (cfv (cv x1) cbs)) (λ x1 . cpo)) ⟶ wceq cp0 (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cbs) (cfv (cv x1) cglb))) ⟶ wceq cp1 (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cbs) (cfv (cv x1) club))) ⟶ wceq clat (crab (λ x1 . wa (wceq (cdm (cfv (cv x1) cjn)) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) (wceq (cdm (cfv (cv x1) cmee)) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)))) (λ x1 . cpo)) ⟶ wceq ccla (crab (λ x1 . wa (wceq (cdm (cfv (cv x1) club)) (cpw (cfv (cv x1) cbs))) (wceq (cdm (cfv (cv x1) cglb)) (cpw (cfv (cv x1) cbs)))) (λ x1 . cpo)) ⟶ wceq codu (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cop (cfv cnx cple) (ccnv (cfv (cv x1) cple))) csts)) ⟶ wceq cipo (cmpt (λ x1 . cvv) (λ x1 . csb (copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (cv x1)) (wss (cv x2) (cv x3)))) (λ x2 . cun (cpr (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cts) (cfv (cv x2) cordt))) (cpr (cop (cfv cnx cple) (cv x2)) (cop (cfv cnx coc) (cmpt (λ x3 . cv x1) (λ x3 . cuni (crab (λ x4 . wceq (cin (cv x4) (cv x3)) c0) (λ x4 . cv x1))))))))) ⟶ wceq cdlat (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wceq (co (cv x5) (co (cv x6) (cv x7) (cv x3)) (cv x4)) (co (co (cv x5) (cv x6) (cv x4)) (co (cv x5) (cv x7) (cv x4)) (cv x3))) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (cfv (cv x1) cmee)) (cfv (cv x1) cjn)) (cfv (cv x1) cbs)) (λ x1 . clat)) ⟶ wceq cps (cab (λ x1 . w3a (wrel (cv x1)) (wss (ccom (cv x1) (cv x1)) (cv x1)) (wceq (cin (cv x1) (ccnv (cv x1))) (cres cid (cuni (cuni (cv x1))))))) ⟶ wceq ctsr (crab (λ x1 . wss (cxp (cdm (cv x1)) (cdm (cv x1))) (cun (cv x1) (ccnv (cv x1)))) (λ x1 . cps)) ⟶ x0) ⟶ x0
Theorem df_preset : wceq cpreset (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wa (wbr (cv x3) (cv x3) (cv x2)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x5) (cv x2)) ⟶ wbr (cv x3) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cple)) (cfv (cv x0) cbs))) (proof)
Theorem df_drs : wceq cdrs (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wa (wne (cv x1) c0) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wa (wbr (cv x3) (cv x5) (cv x2)) (wbr (cv x4) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1))) (cfv (cv x0) cple)) (cfv (cv x0) cbs)) (λ x0 . cpreset)) (proof)
Theorem df_poset : wceq cpo (cab (λ x0 . wex (λ x1 . wex (λ x2 . w3a (wceq (cv x1) (cfv (cv x0) cbs)) (wceq (cv x2) (cfv (cv x0) cple)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . w3a (wbr (cv x3) (cv x3) (cv x2)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x3) (cv x2)) ⟶ wceq (cv x3) (cv x4)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x5) (cv x2)) ⟶ wbr (cv x3) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)))))) (proof)
Theorem df_plt : wceq cplt (cmpt (λ x0 . cvv) (λ x0 . cdif (cfv (cv x0) cple) cid)) (proof)
Theorem df_lub : wceq club (cmpt (λ x0 . cvv) (λ x0 . cres (cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crio (λ x2 . wa (wral (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x0) cple)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wbr (cv x4) (cv x3) (cfv (cv x0) cple)) (λ x4 . cv x1) ⟶ wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs))) (λ x2 . cfv (cv x0) cbs))) (cab (λ x1 . wreu (λ x2 . wa (wral (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x0) cple)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wbr (cv x4) (cv x3) (cfv (cv x0) cple)) (λ x4 . cv x1) ⟶ wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs))) (λ x2 . cfv (cv x0) cbs))))) (proof)
Theorem df_glb : wceq cglb (cmpt (λ x0 . cvv) (λ x0 . cres (cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crio (λ x2 . wa (wral (λ x3 . wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wbr (cv x3) (cv x4) (cfv (cv x0) cple)) (λ x4 . cv x1) ⟶ wbr (cv x3) (cv x2) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs))) (λ x2 . cfv (cv x0) cbs))) (cab (λ x1 . wreu (λ x2 . wa (wral (λ x3 . wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wbr (cv x3) (cv x4) (cfv (cv x0) cple)) (λ x4 . cv x1) ⟶ wbr (cv x3) (cv x2) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs))) (λ x2 . cfv (cv x0) cbs))))) (proof)
Theorem df_join : wceq cjn (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . wbr (cpr (cv x1) (cv x2)) (cv x3) (cfv (cv x0) club)))) (proof)
Theorem df_meet : wceq cmee (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . wbr (cpr (cv x1) (cv x2)) (cv x3) (cfv (cv x0) cglb)))) (proof)
Theorem df_toset : wceq ctos (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wo (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x3) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cple)) (cfv (cv x0) cbs)) (λ x0 . cpo)) (proof)
Theorem df_p0 : wceq cp0 (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) cglb))) (proof)
Theorem df_p1 : wceq cp1 (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) club))) (proof)
Theorem df_lat : wceq clat (crab (λ x0 . wa (wceq (cdm (cfv (cv x0) cjn)) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) (wceq (cdm (cfv (cv x0) cmee)) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)))) (λ x0 . cpo)) (proof)
Theorem df_clat : wceq ccla (crab (λ x0 . wa (wceq (cdm (cfv (cv x0) club)) (cpw (cfv (cv x0) cbs))) (wceq (cdm (cfv (cv x0) cglb)) (cpw (cfv (cv x0) cbs)))) (λ x0 . cpo)) (proof)
Theorem df_odu : wceq codu (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cop (cfv cnx cple) (ccnv (cfv (cv x0) cple))) csts)) (proof)
Theorem df_ipo : wceq cipo (cmpt (λ x0 . cvv) (λ x0 . csb (copab (λ x1 x2 . wa (wss (cpr (cv x1) (cv x2)) (cv x0)) (wss (cv x1) (cv x2)))) (λ x1 . cun (cpr (cop (cfv cnx cbs) (cv x0)) (cop (cfv cnx cts) (cfv (cv x1) cordt))) (cpr (cop (cfv cnx cple) (cv x1)) (cop (cfv cnx coc) (cmpt (λ x2 . cv x0) (λ x2 . cuni (crab (λ x3 . wceq (cin (cv x3) (cv x2)) c0) (λ x3 . cv x0))))))))) (proof)
Theorem df_dlat : wceq cdlat (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wceq (co (cv x4) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (co (co (cv x4) (cv x5) (cv x3)) (co (cv x4) (cv x6) (cv x3)) (cv x2))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (cfv (cv x0) cmee)) (cfv (cv x0) cjn)) (cfv (cv x0) cbs)) (λ x0 . clat)) (proof)
Theorem df_ps : wceq cps (cab (λ x0 . w3a (wrel (cv x0)) (wss (ccom (cv x0) (cv x0)) (cv x0)) (wceq (cin (cv x0) (ccnv (cv x0))) (cres cid (cuni (cuni (cv x0))))))) (proof)
Theorem df_tsr : wceq ctsr (crab (λ x0 . wss (cxp (cdm (cv x0)) (cdm (cv x0))) (cun (cv x0) (ccnv (cv x0)))) (λ x0 . cps)) (proof)