Proofgold Asset

Known df_gbow__df_gbo__ax_bgbltosilva__ax_tgoldbachgt__ax_hgprmladder__ax_bgbltosilvaOLD__ax_hgprmladderOLD__ax_tgoldbachgtOLD__df_upwlks__df_spr__df_mgmhm__df_submgm__df_cllaw__df_comlaw__df_asslaw__df_intop__df_clintop__df_assintop : ∀ x0 : ο . (wceq cgbow (crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x1) (co (co (cv x2) (cv x3) caddc) (cv x4) caddc)) (λ x4 . cprime)) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . codd)) ⟶ wceq cgbo (crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (w3a (wcel (cv x2) codd) (wcel (cv x3) codd) (wcel (cv x4) codd)) (wceq (cv x1) (co (co (cv x2) (cv x3) caddc) (cv x4) caddc))) (λ x4 . cprime)) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . codd)) ⟶ (∀ x1 : ι → ο . w3a (wcel x1 ceven) (wbr c4 x1 clt) (wbr x1 (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x1 cgbe) ⟶ (∀ x1 : ι → ι → ι → ι → ι → ι → ο . ∀ x2 : ι → ι → ο . (∀ x3 . wceq (x2 x3) (crab (λ x4 . wn (wbr c2 (cv x4) cdvds)) (λ x4 . cz))) ⟶ (∀ x3 x4 x5 x6 x7 . wceq (x1 x3 x4 x5 x6 x7) (crab (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . wa (w3a (wcel (cv x9) (x2 x4)) (wcel (cv x10) (x2 x4)) (wcel (cv x11) (x2 x4))) (wceq (cv x8) (co (co (cv x9) (cv x10) caddc) (cv x11) caddc))) (λ x11 . cprime)) (λ x10 . cprime)) (λ x9 . cprime)) (λ x8 . x2 x4))) ⟶ ∀ x3 x4 x5 x6 . wrex (λ x7 . wa (wbr (cv x7) (co (cdc c1 cc0) (cdc c2 c7) cexp) cle) (wral (λ x8 . wbr (cv x7) (cv x8) clt ⟶ wcel (cv x8) (x1 x3 x8 x4 x5 x6)) x2)) (λ x7 . cn)) ⟶ wrex (λ x1 . wrex (λ x2 . wa (w3a (wceq (cfv cc0 (cv x2)) c7) (wceq (cfv c1 (cv x2)) (cdc c1 c3)) (wceq (cfv (cv x1) (cv x2)) (co (cdc c8 c9) (co (cdc c1 cc0) (cdc c2 c9) cexp) cmul))) (wral (λ x3 . w3a (wcel (cfv (cv x3) (cv x2)) (cdif cprime (csn c2))) (wbr (co (cfv (co (cv x3) c1 caddc) (cv x2)) (cfv (cv x3) (cv x2)) cmin) (co (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) c4 cmin) clt) (wbr c4 (co (cfv (co (cv x3) c1 caddc) (cv x2)) (cfv (cv x3) (cv x2)) cmin) clt)) (λ x3 . co cc0 (cv x1) cfzo))) (λ x2 . cfv (cv x1) ciccp)) (λ x1 . cfv c3 cuz) ⟶ (∀ x1 : ι → ο . w3a (wcel x1 ceven) (wbr c4 x1 clt) (wbr x1 (co c4 (co c10 (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x1 cgbe) ⟶ wrex (λ x1 . wrex (λ x2 . wa (w3a (wceq (cfv cc0 (cv x2)) c7) (wceq (cfv c1 (cv x2)) (cdc c1 c3)) (wceq (cfv (cv x1) (cv x2)) (co (cdc c8 c9) (co c10 (cdc c2 c9) cexp) cmul))) (wral (λ x3 . w3a (wcel (cfv (cv x3) (cv x2)) (cdif cprime (csn c2))) (wbr (co (cfv (co (cv x3) c1 caddc) (cv x2)) (cfv (cv x3) (cv x2)) cmin) (co (co c4 (co c10 (cdc c1 c8) cexp) cmul) c4 cmin) clt) (wbr c4 (co (cfv (co (cv x3) c1 caddc) (cv x2)) (cfv (cv x3) (cv x2)) cmin) clt)) (λ x3 . co cc0 (cv x1) cfzo))) (λ x2 . cfv (cv x1) ciccp)) (λ x1 . cfv c3 cuz) ⟶ wrex (λ x1 . wa (wbr (cv x1) (co c10 (cdc c2 c7) cexp) cle) (wral (λ x2 . wbr (cv x1) (cv x2) clt ⟶ wcel (cv x2) cgbo) (λ x2 . codd))) (λ x1 . cn) ⟶ wceq cupwlks (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (cword (cdm (cfv (cv x1) ciedg)))) (wf (co cc0 (cfv (cv x2) chash) cfz) (cfv (cv x1) cvtx) (cv x3)) (wral (λ x4 . wceq (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) ciedg)) (cpr (cfv (cv x4) (cv x3)) (cfv (co (cv x4) c1 caddc) (cv x3)))) (λ x4 . co cc0 (cfv (cv x2) chash) cfzo))))) ⟶ wceq cspr (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (cpr (cv x3) (cv x4))) (λ x4 . cv x1)) (λ x3 . cv x1)))) ⟶ wceq cmgmhm (cmpt2 (λ x1 x2 . cmgm) (λ x1 x2 . cmgm) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cfv (cv x1) cplusg)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) cplusg))) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . co (cfv (cv x2) cbs) (cfv (cv x1) cbs) cmap))) ⟶ wceq csubmgm (cmpt (λ x1 . cmgm) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2)) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq ccllaw (copab (λ x1 x2 . wral (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) (cv x1)) (cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2))) ⟶ wceq ccomlaw (copab (λ x1 x2 . wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cv x1)) (co (cv x4) (cv x3) (cv x1))) (λ x4 . cv x2)) (λ x3 . cv x2))) ⟶ wceq casslaw (copab (λ x1 x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cv x3) (cv x4) (cv x1)) (cv x5) (cv x1)) (co (cv x3) (co (cv x4) (cv x5) (cv x1)) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2))) ⟶ wceq cintop (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cv x2) (cxp (cv x1) (cv x1)) cmap)) ⟶ wceq cclintop (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cv x1) cintop)) ⟶ wceq cassintop (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cv x1) casslaw) (λ x2 . cfv (cv x1) cclintop))) ⟶ x0) ⟶ x0
Theorem df_gbow : wceq cgbow (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wceq (cv x0) (co (co (cv x1) (cv x2) caddc) (cv x3) caddc)) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . cprime)) (λ x0 . codd)) (proof)
Theorem df_gbo : wceq cgbo (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (w3a (wcel (cv x1) codd) (wcel (cv x2) codd) (wcel (cv x3) codd)) (wceq (cv x0) (co (co (cv x1) (cv x2) caddc) (cv x3) caddc))) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . cprime)) (λ x0 . codd)) (proof)
Theorem ax_bgbltosilva : ∀ x0 : ι → ο . w3a (wcel x0 ceven) (wbr c4 x0 clt) (wbr x0 (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x0 cgbe (proof)
Theorem ax_tgoldbachgt : ∀ x0 : ι → ι → ι → ι → ι → ι → ο . ∀ x1 : ι → ι → ο . (∀ x2 . wceq (x1 x2) (crab (λ x3 . wn (wbr c2 (cv x3) cdvds)) (λ x3 . cz))) ⟶ (∀ x2 x3 x4 x5 x6 . wceq (x0 x2 x3 x4 x5 x6) (crab (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wa (w3a (wcel (cv x8) (x1 x3)) (wcel (cv x9) (x1 x3)) (wcel (cv x10) (x1 x3))) (wceq (cv x7) (co (co (cv x8) (cv x9) caddc) (cv x10) caddc))) (λ x10 . cprime)) (λ x9 . cprime)) (λ x8 . cprime)) (λ x7 . x1 x3))) ⟶ ∀ x2 x3 x4 x5 . wrex (λ x6 . wa (wbr (cv x6) (co (cdc c1 cc0) (cdc c2 c7) cexp) cle) (wral (λ x7 . wbr (cv x6) (cv x7) clt ⟶ wcel (cv x7) (x0 x2 x7 x3 x4 x5)) x1)) (λ x6 . cn) (proof)
Theorem ax_hgprmladder : wrex (λ x0 . wrex (λ x1 . wa (w3a (wceq (cfv cc0 (cv x1)) c7) (wceq (cfv c1 (cv x1)) (cdc c1 c3)) (wceq (cfv (cv x0) (cv x1)) (co (cdc c8 c9) (co (cdc c1 cc0) (cdc c2 c9) cexp) cmul))) (wral (λ x2 . w3a (wcel (cfv (cv x2) (cv x1)) (cdif cprime (csn c2))) (wbr (co (cfv (co (cv x2) c1 caddc) (cv x1)) (cfv (cv x2) (cv x1)) cmin) (co (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) c4 cmin) clt) (wbr c4 (co (cfv (co (cv x2) c1 caddc) (cv x1)) (cfv (cv x2) (cv x1)) cmin) clt)) (λ x2 . co cc0 (cv x0) cfzo))) (λ x1 . cfv (cv x0) ciccp)) (λ x0 . cfv c3 cuz) (proof)
Theorem ax_bgbltosilvaOLD : ∀ x0 : ι → ο . w3a (wcel x0 ceven) (wbr c4 x0 clt) (wbr x0 (co c4 (co c10 (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x0 cgbe (proof)
Theorem ax_hgprmladderOLD : wrex (λ x0 . wrex (λ x1 . wa (w3a (wceq (cfv cc0 (cv x1)) c7) (wceq (cfv c1 (cv x1)) (cdc c1 c3)) (wceq (cfv (cv x0) (cv x1)) (co (cdc c8 c9) (co c10 (cdc c2 c9) cexp) cmul))) (wral (λ x2 . w3a (wcel (cfv (cv x2) (cv x1)) (cdif cprime (csn c2))) (wbr (co (cfv (co (cv x2) c1 caddc) (cv x1)) (cfv (cv x2) (cv x1)) cmin) (co (co c4 (co c10 (cdc c1 c8) cexp) cmul) c4 cmin) clt) (wbr c4 (co (cfv (co (cv x2) c1 caddc) (cv x1)) (cfv (cv x2) (cv x1)) cmin) clt)) (λ x2 . co cc0 (cv x0) cfzo))) (λ x1 . cfv (cv x0) ciccp)) (λ x0 . cfv c3 cuz) (proof)
Theorem ax_tgoldbachgtOLD : wrex (λ x0 . wa (wbr (cv x0) (co c10 (cdc c2 c7) cexp) cle) (wral (λ x1 . wbr (cv x0) (cv x1) clt ⟶ wcel (cv x1) cgbo) (λ x1 . codd))) (λ x0 . cn) (proof)
Theorem df_upwlks : wceq cupwlks (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (cword (cdm (cfv (cv x0) ciedg)))) (wf (co cc0 (cfv (cv x1) chash) cfz) (cfv (cv x0) cvtx) (cv x2)) (wral (λ x3 . wceq (cfv (cfv (cv x3) (cv x1)) (cfv (cv x0) ciedg)) (cpr (cfv (cv x3) (cv x2)) (cfv (co (cv x3) c1 caddc) (cv x2)))) (λ x3 . co cc0 (cfv (cv x1) chash) cfzo))))) (proof)
Theorem df_spr : wceq cspr (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wrex (λ x2 . wrex (λ x3 . wceq (cv x1) (cpr (cv x2) (cv x3))) (λ x3 . cv x0)) (λ x2 . cv x0)))) (proof)
Theorem df_mgmhm : wceq cmgmhm (cmpt2 (λ x0 x1 . cmgm) (λ x0 x1 . cmgm) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cfv (co (cv x3) (cv x4) (cfv (cv x0) cplusg)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cplusg))) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . co (cfv (cv x1) cbs) (cfv (cv x0) cbs) cmap))) (proof)
Theorem df_submgm : wceq csubmgm (cmpt (λ x0 . cmgm) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wcel (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_cllaw : wceq ccllaw (copab (λ x0 x1 . wral (λ x2 . wral (λ x3 . wcel (co (cv x2) (cv x3) (cv x0)) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1))) (proof)
Theorem df_comlaw : wceq ccomlaw (copab (λ x0 x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cv x0)) (co (cv x3) (cv x2) (cv x0))) (λ x3 . cv x1)) (λ x2 . cv x1))) (proof)
Theorem df_asslaw : wceq casslaw (copab (λ x0 x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x0)) (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x0))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1))) (proof)
Theorem df_intop : wceq cintop (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cv x1) (cxp (cv x0) (cv x0)) cmap)) (proof)
Theorem df_clintop : wceq cclintop (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cv x0) cintop)) (proof)
Theorem df_assintop : wceq cassintop (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cv x0) casslaw) (λ x1 . cfv (cv x0) cclintop))) (proof)