Proofgold Address

Known df_odz__df_phi__df_pc__df_gz__df_vdwap__df_vdwmc__df_vdwpc__df_ram__df_prmo__df_struct__df_ndx__df_slot__df_base__df_sets__df_ress__df_plusg__df_mulr__df_starv : ∀ x0 : ο . (wceq codz (cmpt (λ x1 . cn) (λ x1 . cmpt (λ x2 . crab (λ x3 . wceq (co (cv x3) (cv x1) cgcd) c1) (λ x3 . cz)) (λ x2 . cinf (crab (λ x3 . wbr (cv x1) (co (co (cv x2) (cv x3) cexp) c1 cmin) cdvds) (λ x3 . cn)) cr clt))) ⟶ wceq cphi (cmpt (λ x1 . cn) (λ x1 . cfv (crab (λ x2 . wceq (co (cv x2) (cv x1) cgcd) c1) (λ x2 . co c1 (cv x1) cfz)) chash)) ⟶ wceq cpc (cmpt2 (λ x1 x2 . cprime) (λ x1 x2 . cq) (λ x1 x2 . cif (wceq (cv x2) cc0) cpnf (cio (λ x3 . wrex (λ x4 . wrex (λ x5 . wa (wceq (cv x2) (co (cv x4) (cv x5) cdiv)) (wceq (cv x3) (co (csup (crab (λ x6 . wbr (co (cv x1) (cv x6) cexp) (cv x4) cdvds) (λ x6 . cn0)) cr clt) (csup (crab (λ x6 . wbr (co (cv x1) (cv x6) cexp) (cv x5) cdvds) (λ x6 . cn0)) cr clt) cmin))) (λ x5 . cn)) (λ x4 . cz))))) ⟶ wceq cgz (crab (λ x1 . wa (wcel (cfv (cv x1) cre) cz) (wcel (cfv (cv x1) cim) cz)) (λ x1 . cc)) ⟶ wceq cvdwa (cmpt (λ x1 . cn0) (λ x1 . cmpt2 (λ x2 x3 . cn) (λ x2 x3 . cn) (λ x2 x3 . crn (cmpt (λ x4 . co cc0 (co (cv x1) c1 cmin) cfz) (λ x4 . co (cv x2) (co (cv x4) (cv x3) cmul) caddc))))) ⟶ wceq cvdwm (copab (λ x1 x2 . wex (λ x3 . wne (cin (crn (cfv (cv x1) cvdwa)) (cpw (cima (ccnv (cv x2)) (csn (cv x3))))) c0))) ⟶ wceq cvdwp (coprab (λ x1 x2 x3 . wrex (λ x4 . wrex (λ x5 . wa (wral (λ x6 . wss (co (co (cv x4) (cfv (cv x6) (cv x5)) caddc) (cfv (cv x6) (cv x5)) (cfv (cv x2) cvdwa)) (cima (ccnv (cv x3)) (csn (cfv (co (cv x4) (cfv (cv x6) (cv x5)) caddc) (cv x3))))) (λ x6 . co c1 (cv x1) cfz)) (wceq (cfv (crn (cmpt (λ x6 . co c1 (cv x1) cfz) (λ x6 . cfv (co (cv x4) (cfv (cv x6) (cv x5)) caddc) (cv x3)))) chash) (cv x1))) (λ x5 . co cn (co c1 (cv x1) cfz) cmap)) (λ x4 . cn))) ⟶ wceq cram (cmpt2 (λ x1 x2 . cn0) (λ x1 x2 . cvv) (λ x1 x2 . cinf (crab (λ x3 . ∀ x4 . wbr (cv x3) (cfv (cv x4) chash) cle ⟶ wral (λ x5 . wrex (λ x6 . wrex (λ x7 . wa (wbr (cfv (cv x6) (cv x2)) (cfv (cv x7) chash) cle) (wral (λ x8 . wceq (cfv (cv x8) chash) (cv x1) ⟶ wceq (cfv (cv x8) (cv x5)) (cv x6)) (λ x8 . cpw (cv x7)))) (λ x7 . cpw (cv x4))) (λ x6 . cdm (cv x2))) (λ x5 . co (cdm (cv x2)) (crab (λ x6 . wceq (cfv (cv x6) chash) (cv x1)) (λ x6 . cpw (cv x4))) cmap)) (λ x3 . cn0)) cxr clt)) ⟶ wceq cprmo (cmpt (λ x1 . cn0) (λ x1 . cprod (λ x2 . co c1 (cv x1) cfz) (λ x2 . cif (wcel (cv x2) cprime) (cv x2) c1))) ⟶ wceq cstr (copab (λ x1 x2 . w3a (wcel (cv x2) (cin cle (cxp cn cn))) (wfun (cdif (cv x1) (csn c0))) (wss (cdm (cv x1)) (cfv (cv x2) cfz)))) ⟶ wceq cnx (cres cid cn) ⟶ (∀ x1 : ι → ο . wceq (cslot x1) (cmpt (λ x2 . cvv) (λ x2 . cfv x1 (cv x2)))) ⟶ wceq cbs (cslot c1) ⟶ wceq csts (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cun (cres (cv x1) (cdif cvv (cdm (csn (cv x2))))) (csn (cv x2)))) ⟶ wceq cress (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cif (wss (cfv (cv x1) cbs) (cv x2)) (cv x1) (co (cv x1) (cop (cfv cnx cbs) (cin (cv x2) (cfv (cv x1) cbs))) csts))) ⟶ wceq cplusg (cslot c2) ⟶ wceq cmulr (cslot c3) ⟶ wceq cstv (cslot c4) ⟶ x0) ⟶ x0
Theorem df_odz : wceq codz (cmpt (λ x0 . cn) (λ x0 . cmpt (λ x1 . crab (λ x2 . wceq (co (cv x2) (cv x0) cgcd) c1) (λ x2 . cz)) (λ x1 . cinf (crab (λ x2 . wbr (cv x0) (co (co (cv x1) (cv x2) cexp) c1 cmin) cdvds) (λ x2 . cn)) cr clt)))
Theorem df_phi : wceq cphi (cmpt (λ x0 . cn) (λ x0 . cfv (crab (λ x1 . wceq (co (cv x1) (cv x0) cgcd) c1) (λ x1 . co c1 (cv x0) cfz)) chash))
Theorem df_pc : wceq cpc (cmpt2 (λ x0 x1 . cprime) (λ x0 x1 . cq) (λ x0 x1 . cif (wceq (cv x1) cc0) cpnf (cio (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wceq (cv x1) (co (cv x3) (cv x4) cdiv)) (wceq (cv x2) (co (csup (crab (λ x5 . wbr (co (cv x0) (cv x5) cexp) (cv x3) cdvds) (λ x5 . cn0)) cr clt) (csup (crab (λ x5 . wbr (co (cv x0) (cv x5) cexp) (cv x4) cdvds) (λ x5 . cn0)) cr clt) cmin))) (λ x4 . cn)) (λ x3 . cz)))))
Theorem df_gz : wceq cgz (crab (λ x0 . wa (wcel (cfv (cv x0) cre) cz) (wcel (cfv (cv x0) cim) cz)) (λ x0 . cc))
Theorem df_vdwap : wceq cvdwa (cmpt (λ x0 . cn0) (λ x0 . cmpt2 (λ x1 x2 . cn) (λ x1 x2 . cn) (λ x1 x2 . crn (cmpt (λ x3 . co cc0 (co (cv x0) c1 cmin) cfz) (λ x3 . co (cv x1) (co (cv x3) (cv x2) cmul) caddc)))))
Theorem df_vdwmc : wceq cvdwm (copab (λ x0 x1 . wex (λ x2 . wne (cin (crn (cfv (cv x0) cvdwa)) (cpw (cima (ccnv (cv x1)) (csn (cv x2))))) c0)))
Theorem df_vdwpc : wceq cvdwp (coprab (λ x0 x1 x2 . wrex (λ x3 . wrex (λ x4 . wa (wral (λ x5 . wss (co (co (cv x3) (cfv (cv x5) (cv x4)) caddc) (cfv (cv x5) (cv x4)) (cfv (cv x1) cvdwa)) (cima (ccnv (cv x2)) (csn (cfv (co (cv x3) (cfv (cv x5) (cv x4)) caddc) (cv x2))))) (λ x5 . co c1 (cv x0) cfz)) (wceq (cfv (crn (cmpt (λ x5 . co c1 (cv x0) cfz) (λ x5 . cfv (co (cv x3) (cfv (cv x5) (cv x4)) caddc) (cv x2)))) chash) (cv x0))) (λ x4 . co cn (co c1 (cv x0) cfz) cmap)) (λ x3 . cn)))
Theorem df_ram : wceq cram (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cvv) (λ x0 x1 . cinf (crab (λ x2 . ∀ x3 . wbr (cv x2) (cfv (cv x3) chash) cle ⟶ wral (λ x4 . wrex (λ x5 . wrex (λ x6 . wa (wbr (cfv (cv x5) (cv x1)) (cfv (cv x6) chash) cle) (wral (λ x7 . wceq (cfv (cv x7) chash) (cv x0) ⟶ wceq (cfv (cv x7) (cv x4)) (cv x5)) (λ x7 . cpw (cv x6)))) (λ x6 . cpw (cv x3))) (λ x5 . cdm (cv x1))) (λ x4 . co (cdm (cv x1)) (crab (λ x5 . wceq (cfv (cv x5) chash) (cv x0)) (λ x5 . cpw (cv x3))) cmap)) (λ x2 . cn0)) cxr clt))
Theorem df_prmo : wceq cprmo (cmpt (λ x0 . cn0) (λ x0 . cprod (λ x1 . co c1 (cv x0) cfz) (λ x1 . cif (wcel (cv x1) cprime) (cv x1) c1)))
Theorem df_struct : wceq cstr (copab (λ x0 x1 . w3a (wcel (cv x1) (cin cle (cxp cn cn))) (wfun (cdif (cv x0) (csn c0))) (wss (cdm (cv x0)) (cfv (cv x1) cfz))))
Theorem df_ndx : wceq cnx (cres cid cn)
Theorem df_slot : ∀ x0 : ι → ο . wceq (cslot x0) (cmpt (λ x1 . cvv) (λ x1 . cfv x0 (cv x1)))
Theorem df_base : wceq cbs (cslot c1)
Theorem df_sets : wceq csts (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cun (cres (cv x0) (cdif cvv (cdm (csn (cv x1))))) (csn (cv x1))))
Theorem df_ress : wceq cress (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cif (wss (cfv (cv x0) cbs) (cv x1)) (cv x0) (co (cv x0) (cop (cfv cnx cbs) (cin (cv x1) (cfv (cv x0) cbs))) csts)))
Theorem df_plusg : wceq cplusg (cslot c2)
Theorem df_mulr : wceq cmulr (cslot c3)
Theorem df_starv : wceq cstv (cslot c4)