Known df_vts__ax_hgt749__ax_ros335__ax_ros336__df_trkg2d__df_afs__df_bnj17__df_bnj14__df_bnj13__df_bnj15__df_bnj18__df_bnj19__ax_7d__ax_8d__ax_9d1__ax_9d2__ax_10d__ax_11d : ∀ x0 : ο . (wceq cvts (cmpt2 (λ x1 x2 . co cc cn cmap) (λ x1 x2 . cn0) (λ x1 x2 . cmpt (λ x3 . cc) (λ x3 . csu (co c1 (cv x2) cfz) (λ x4 . co (cfv (cv x4) (cv x1)) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cv x4) (cv x3) cmul) cmul) ce) cmul)))) ⟶ wral (λ x1 . wbr (co (cdc c1 cc0) (cdc c2 c7) cexp) (cv x1) cle ⟶ wrex (λ x2 . wrex (λ x3 . w3a (wral (λ x4 . wbr (cfv (cv x4) (cv x3)) (co c1 (cdp2 cc0 (cdp2 c7 (cdp2 c9 (cdp2 c9 (cdp2 c5 c5))))) cdp) cle) (λ x4 . cn)) (wral (λ x4 . wbr (cfv (cv x4) (cv x2)) (co c1 (cdp2 c4 (cdp2 c1 c4)) cdp) cle) (λ x4 . cn)) (wbr (co (co cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 c4 (cdp2 c2 (cdp2 c2 (cdp2 c4 c8))))))) cdp) (co (cv x1) c2 cexp) cmul) (citg (λ x4 . co cc0 c1 cioo) (λ x4 . co (co (cfv (cv x4) (co (co cvma (cv x2) (cof cmul)) (cv x1) cvts)) (co (cfv (cv x4) (co (co cvma (cv x3) (cof cmul)) (cv x1) cvts)) c2 cexp) cmul) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cneg (cv x1)) (cv x4) cmul) cmul) ce) cmul)) cle)) (λ x3 . co (co cc0 cpnf cico) cn cmap)) (λ x2 . co (co cc0 cpnf cico) cn cmap)) (λ x1 . crab (λ x2 . wn (wbr c2 (cv x2) cdvds)) (λ x2 . cz)) ⟶ wral (λ x1 . wbr (cfv (cv x1) cchp) (co (co c1 (cdp2 cc0 (cdp2 c3 (cdp2 c8 (cdp2 c8 c3)))) cdp) (cv x1) cmul) clt) (λ x1 . crp) ⟶ wral (λ x1 . wbr (co (cfv (cv x1) cchp) (cfv (cv x1) ccht) cmin) (co (co c1 (cdp2 c4 (cdp2 c2 (cdp2 c6 c2))) cdp) (cfv (cv x1) csqrt) cmul) clt) (λ x1 . crp) ⟶ wceq cstrkg2d (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wn (w3o (wcel (cv x7) (co (cv x5) (cv x6) (cv x4))) (wcel (cv x5) (co (cv x7) (cv x6) (cv x4))) (wcel (cv x6) (co (cv x5) (cv x7) (cv x4))))) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wa (w3a (wceq (co (cv x5) (cv x8) (cv x3)) (co (cv x5) (cv x9) (cv x3))) (wceq (co (cv x6) (cv x8) (cv x3)) (co (cv x6) (cv x9) (cv x3))) (wceq (co (cv x7) (cv x8) (cv x3)) (co (cv x7) (cv x9) (cv x3)))) (wne (cv x8) (cv x9)) ⟶ w3o (wcel (cv x7) (co (cv x5) (cv x6) (cv x4))) (wcel (cv x5) (co (cv x7) (cv x6) (cv x4))) (wcel (cv x6) (co (cv x5) (cv x7) (cv x4)))) (λ x9 . cv x2)) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2))) (cfv (cv x1) citv)) (cfv (cv x1) cds)) (cfv (cv x1) cbs))) ⟶ wceq cafs (cmpt (λ x1 . cstrkg) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . wrex (λ x12 . wrex (λ x13 . wrex (λ x14 . w3a (wceq (cv x2) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (wceq (cv x3) (cop (cop (cv x11) (cv x12)) (cop (cv x13) (cv x14)))) (w3a (wa (wcel (cv x8) (co (cv x7) (cv x9) (cv x6))) (wcel (cv x12) (co (cv x11) (cv x13) (cv x6)))) (wa (wceq (co (cv x7) (cv x8) (cv x5)) (co (cv x11) (cv x12) (cv x5))) (wceq (co (cv x8) (cv x9) (cv x5)) (co (cv x12) (cv x13) (cv x5)))) (wa (wceq (co (cv x7) (cv x10) (cv x5)) (co (cv x11) (cv x14) (cv x5))) (wceq (co (cv x8) (cv x10) (cv x5)) (co (cv x12) (cv x14) (cv x5)))))) (λ x14 . cv x4)) (λ x13 . cv x4)) (λ x12 . cv x4)) (λ x11 . cv x4)) (λ x10 . cv x4)) (λ x9 . cv x4)) (λ x8 . cv x4)) (λ x7 . cv x4)) (cfv (cv x1) citv)) (cfv (cv x1) cds)) (cfv (cv x1) cbs)))) ⟶ (∀ x1 x2 x3 x4 : ο . wb (w_bnj17 x1 x2 x3 x4) (wa (w3a x1 x2 x3) x4)) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (c_bnj14 x1 x2 x3) (crab (λ x4 . wbr (cv x4) x3 x2) (λ x4 . x1))) ⟶ (∀ x1 x2 : ι → ο . wb (w_bnj13 x1 x2) (wral (λ x3 . wcel (c_bnj14 x1 x2 (cv x3)) cvv) (λ x3 . x1))) ⟶ (∀ x1 x2 : ι → ο . wb (w_bnj15 x1 x2) (wa (wfr x1 x2) (w_bnj13 x1 x2))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (c_bnj18 x1 x2 x3) (ciun (λ x4 . cab (λ x5 . wrex (λ x6 . w3a (wfn (cv x5) (cv x6)) (wceq (cfv c0 (cv x5)) (c_bnj14 x1 x2 x3)) (wral (λ x7 . wcel (csuc (cv x7)) (cv x6) ⟶ wceq (cfv (csuc (cv x7)) (cv x5)) (ciun (λ x8 . cfv (cv x7) (cv x5)) (λ x8 . c_bnj14 x1 x2 (cv x8)))) (λ x7 . com))) (λ x6 . cdif com (csn c0)))) (λ x4 . ciun (λ x5 . cdm (cv x4)) (λ x5 . cfv (cv x5) (cv x4))))) ⟶ (∀ x1 x2 x3 : ι → ο . wb (w_bnj19 x1 x2 x3) (wral (λ x4 . wss (c_bnj14 x1 x3 (cv x4)) x2) (λ x4 . x2))) ⟶ (∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3) ⟶ ∀ x2 x3 . x1 x3 x2) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x3) ⟶ wceq (cv x2) (cv x3)) ⟶ wn (∀ x1 . wn (wceq (cv x1) (cv x1))) ⟶ (∀ x1 . wn (∀ x2 . wn (wceq (cv x2) (cv x1)))) ⟶ (∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x2)) ⟶ ∀ x3 . wceq (cv x3) (cv x1)) ⟶ (∀ x1 : ι → ι → ο . ∀ x2 x3 . wceq (cv x2) (cv x3) ⟶ (∀ x4 . x1 x2 x4) ⟶ ∀ x4 . wceq (cv x4) (cv x3) ⟶ x1 x4 x3) ⟶ x0) ⟶ x0
Theorem df_vts : wceq cvts (cmpt2 (λ x0 x1 . co cc cn cmap) (λ x0 x1 . cn0) (λ x0 x1 . cmpt (λ x2 . cc) (λ x2 . csu (co c1 (cv x1) cfz) (λ x3 . co (cfv (cv x3) (cv x0)) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cv x3) (cv x2) cmul) cmul) ce) cmul)))) (proof)
Theorem ax_hgt749 : wral (λ x0 . wbr (co (cdc c1 cc0) (cdc c2 c7) cexp) (cv x0) cle ⟶ wrex (λ x1 . wrex (λ x2 . w3a (wral (λ x3 . wbr (cfv (cv x3) (cv x2)) (co c1 (cdp2 cc0 (cdp2 c7 (cdp2 c9 (cdp2 c9 (cdp2 c5 c5))))) cdp) cle) (λ x3 . cn)) (wral (λ x3 . wbr (cfv (cv x3) (cv x1)) (co c1 (cdp2 c4 (cdp2 c1 c4)) cdp) cle) (λ x3 . cn)) (wbr (co (co cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 c4 (cdp2 c2 (cdp2 c2 (cdp2 c4 c8))))))) cdp) (co (cv x0) c2 cexp) cmul) (citg (λ x3 . co cc0 c1 cioo) (λ x3 . co (co (cfv (cv x3) (co (co cvma (cv x1) (cof cmul)) (cv x0) cvts)) (co (cfv (cv x3) (co (co cvma (cv x2) (cof cmul)) (cv x0) cvts)) c2 cexp) cmul) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cneg (cv x0)) (cv x3) cmul) cmul) ce) cmul)) cle)) (λ x2 . co (co cc0 cpnf cico) cn cmap)) (λ x1 . co (co cc0 cpnf cico) cn cmap)) (λ x0 . crab (λ x1 . wn (wbr c2 (cv x1) cdvds)) (λ x1 . cz)) (proof)
Theorem ax_ros335 : wral (λ x0 . wbr (cfv (cv x0) cchp) (co (co c1 (cdp2 cc0 (cdp2 c3 (cdp2 c8 (cdp2 c8 c3)))) cdp) (cv x0) cmul) clt) (λ x0 . crp) (proof)
Theorem ax_ros336 : wral (λ x0 . wbr (co (cfv (cv x0) cchp) (cfv (cv x0) ccht) cmin) (co (co c1 (cdp2 c4 (cdp2 c2 (cdp2 c6 c2))) cdp) (cfv (cv x0) csqrt) cmul) clt) (λ x0 . crp) (proof)
Theorem df_trkg2d : wceq cstrkg2d (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wn (w3o (wcel (cv x6) (co (cv x4) (cv x5) (cv x3))) (wcel (cv x4) (co (cv x6) (cv x5) (cv x3))) (wcel (cv x5) (co (cv x4) (cv x6) (cv x3))))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wa (w3a (wceq (co (cv x4) (cv x7) (cv x2)) (co (cv x4) (cv x8) (cv x2))) (wceq (co (cv x5) (cv x7) (cv x2)) (co (cv x5) (cv x8) (cv x2))) (wceq (co (cv x6) (cv x7) (cv x2)) (co (cv x6) (cv x8) (cv x2)))) (wne (cv x7) (cv x8)) ⟶ w3o (wcel (cv x6) (co (cv x4) (cv x5) (cv x3))) (wcel (cv x4) (co (cv x6) (cv x5) (cv x3))) (wcel (cv x5) (co (cv x4) (cv x6) (cv x3)))) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1))) (cfv (cv x0) citv)) (cfv (cv x0) cds)) (cfv (cv x0) cbs))) (proof)
Theorem df_afs : wceq cafs (cmpt (λ x0 . cstrkg) (λ x0 . copab (λ x1 x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . wrex (λ x12 . wrex (λ x13 . w3a (wceq (cv x1) (cop (cop (cv x6) (cv x7)) (cop (cv x8) (cv x9)))) (wceq (cv x2) (cop (cop (cv x10) (cv x11)) (cop (cv x12) (cv x13)))) (w3a (wa (wcel (cv x7) (co (cv x6) (cv x8) (cv x5))) (wcel (cv x11) (co (cv x10) (cv x12) (cv x5)))) (wa (wceq (co (cv x6) (cv x7) (cv x4)) (co (cv x10) (cv x11) (cv x4))) (wceq (co (cv x7) (cv x8) (cv x4)) (co (cv x11) (cv x12) (cv x4)))) (wa (wceq (co (cv x6) (cv x9) (cv x4)) (co (cv x10) (cv x13) (cv x4))) (wceq (co (cv x7) (cv x9) (cv x4)) (co (cv x11) (cv x13) (cv x4)))))) (λ x13 . cv x3)) (λ x12 . cv x3)) (λ x11 . cv x3)) (λ x10 . cv x3)) (λ x9 . cv x3)) (λ x8 . cv x3)) (λ x7 . cv x3)) (λ x6 . cv x3)) (cfv (cv x0) citv)) (cfv (cv x0) cds)) (cfv (cv x0) cbs)))) (proof)
Theorem df_bnj17 : ∀ x0 x1 x2 x3 : ο . wb (w_bnj17 x0 x1 x2 x3) (wa (w3a x0 x1 x2) x3) (proof)
Theorem df_bnj14 : ∀ x0 x1 x2 : ι → ο . wceq (c_bnj14 x0 x1 x2) (crab (λ x3 . wbr (cv x3) x2 x1) (λ x3 . x0)) (proof)
Theorem df_bnj13 : ∀ x0 x1 : ι → ο . wb (w_bnj13 x0 x1) (wral (λ x2 . wcel (c_bnj14 x0 x1 (cv x2)) cvv) (λ x2 . x0)) (proof)
Theorem df_bnj15 : ∀ x0 x1 : ι → ο . wb (w_bnj15 x0 x1) (wa (wfr x0 x1) (w_bnj13 x0 x1)) (proof)
Theorem df_bnj18 : ∀ x0 x1 x2 : ι → ο . wceq (c_bnj18 x0 x1 x2) (ciun (λ x3 . cab (λ x4 . wrex (λ x5 . w3a (wfn (cv x4) (cv x5)) (wceq (cfv c0 (cv x4)) (c_bnj14 x0 x1 x2)) (wral (λ x6 . wcel (csuc (cv x6)) (cv x5) ⟶ wceq (cfv (csuc (cv x6)) (cv x4)) (ciun (λ x7 . cfv (cv x6) (cv x4)) (λ x7 . c_bnj14 x0 x1 (cv x7)))) (λ x6 . com))) (λ x5 . cdif com (csn c0)))) (λ x3 . ciun (λ x4 . cdm (cv x3)) (λ x4 . cfv (cv x4) (cv x3)))) (proof)
Theorem df_bnj19 : ∀ x0 x1 x2 : ι → ο . wb (w_bnj19 x0 x1 x2) (wral (λ x3 . wss (c_bnj14 x0 x2 (cv x3)) x1) (λ x3 . x1)) (proof)
Theorem ax_wl_11v : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2) ⟶ ∀ x1 x2 . x0 x2 x1 (proof)
Theorem ax_8d : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x2) ⟶ wceq (cv x1) (cv x2) (proof)
Theorem ax_9d1 : wn (∀ x0 . wn (wceq (cv x0) (cv x0))) (proof)
Theorem ax_9d2 : ∀ x0 . wn (∀ x1 . wn (wceq (cv x1) (cv x0))) (proof)
Theorem ax_c11n : ∀ x0 x1 . (∀ x2 . wceq (cv x2) (cv x1)) ⟶ ∀ x2 . wceq (cv x2) (cv x0) (proof)
Theorem ax_11d : ∀ x0 : ι → ι → ο . ∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ (∀ x3 . x0 x1 x3) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3 x2 (proof)

Proofgold Address