Proofgold Asset

Known df_ifs__df_cgr3__df_fs__df_segle__df_outsideof__df_line2__df_ray__df_lines2__df_fwddif__df_fwddifn__df_hf__df_fne__df_3nand__df_gcdOLD__ax_prv1__ax_prv2__ax_prv3__df_ssb : ∀ x0 : ο . (wceq cifs (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . w3a (wceq (cv x1) (cop (cop (cv x4) (cv x5)) (cop (cv x6) (cv x7)))) (wceq (cv x2) (cop (cop (cv x8) (cv x9)) (cop (cv x10) (cv x11)))) (w3a (wa (wbr (cv x5) (cop (cv x4) (cv x6)) cbtwn) (wbr (cv x9) (cop (cv x8) (cv x10)) cbtwn)) (wa (wbr (cop (cv x4) (cv x6)) (cop (cv x8) (cv x10)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x9) (cv x10)) ccgr)) (wa (wbr (cop (cv x4) (cv x7)) (cop (cv x8) (cv x11)) ccgr) (wbr (cop (cv x6) (cv x7)) (cop (cv x10) (cv x11)) ccgr)))) (λ x11 . cfv (cv x3) cee)) (λ x10 . cfv (cv x3) cee)) (λ x9 . cfv (cv x3) cee)) (λ x8 . cfv (cv x3) cee)) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq ccgr3 (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . w3a (wceq (cv x1) (cop (cv x4) (cop (cv x5) (cv x6)))) (wceq (cv x2) (cop (cv x7) (cop (cv x8) (cv x9)))) (w3a (wbr (cop (cv x4) (cv x5)) (cop (cv x7) (cv x8)) ccgr) (wbr (cop (cv x4) (cv x6)) (cop (cv x7) (cv x9)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x8) (cv x9)) ccgr))) (λ x9 . cfv (cv x3) cee)) (λ x8 . cfv (cv x3) cee)) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq cfs (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . w3a (wceq (cv x1) (cop (cop (cv x4) (cv x5)) (cop (cv x6) (cv x7)))) (wceq (cv x2) (cop (cop (cv x8) (cv x9)) (cop (cv x10) (cv x11)))) (w3a (wbr (cv x4) (cop (cv x5) (cv x6)) ccolin) (wbr (cop (cv x4) (cop (cv x5) (cv x6))) (cop (cv x8) (cop (cv x9) (cv x10))) ccgr3) (wa (wbr (cop (cv x4) (cv x7)) (cop (cv x8) (cv x11)) ccgr) (wbr (cop (cv x5) (cv x7)) (cop (cv x9) (cv x11)) ccgr)))) (λ x11 . cfv (cv x3) cee)) (λ x10 . cfv (cv x3) cee)) (λ x9 . cfv (cv x3) cee)) (λ x8 . cfv (cv x3) cee)) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq csegle (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . w3a (wceq (cv x1) (cop (cv x4) (cv x5))) (wceq (cv x2) (cop (cv x6) (cv x7))) (wrex (λ x8 . wa (wbr (cv x8) (cop (cv x6) (cv x7)) cbtwn) (wbr (cop (cv x4) (cv x5)) (cop (cv x6) (cv x8)) ccgr)) (λ x8 . cfv (cv x3) cee))) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq coutsideof (cdif ccolin cbtwn) ⟶ wceq cline2 (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee)) (wne (cv x1) (cv x2))) (wceq (cv x3) (cec (cop (cv x1) (cv x2)) (ccnv ccolin)))) (λ x4 . cn))) ⟶ wceq cray (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee)) (wne (cv x1) (cv x2))) (wceq (cv x3) (crab (λ x5 . wbr (cv x1) (cop (cv x2) (cv x5)) coutsideof) (λ x5 . cfv (cv x4) cee)))) (λ x4 . cn))) ⟶ wceq clines2 (crn cline2) ⟶ wceq cfwddif (cmpt (λ x1 . co cc cc cpm) (λ x1 . cmpt (λ x2 . crab (λ x3 . wcel (co (cv x3) c1 caddc) (cdm (cv x1))) (λ x3 . cdm (cv x1))) (λ x2 . co (cfv (co (cv x2) c1 caddc) (cv x1)) (cfv (cv x2) (cv x1)) cmin))) ⟶ wceq cfwddifn (cmpt2 (λ x1 x2 . cn0) (λ x1 x2 . co cc cc cpm) (λ x1 x2 . cmpt (λ x3 . crab (λ x4 . wral (λ x5 . wcel (co (cv x4) (cv x5) caddc) (cdm (cv x2))) (λ x5 . co cc0 (cv x1) cfz)) (λ x4 . cc)) (λ x3 . csu (co cc0 (cv x1) cfz) (λ x4 . co (co (cv x1) (cv x4) cbc) (co (co (cneg c1) (co (cv x1) (cv x4) cmin) cexp) (cfv (co (cv x3) (cv x4) caddc) (cv x2)) cmul) cmul)))) ⟶ wceq chf (cuni (cima cr1 com)) ⟶ wceq cfne (copab (λ x1 x2 . wa (wceq (cuni (cv x1)) (cuni (cv x2))) (wral (λ x3 . wss (cv x3) (cuni (cin (cv x2) (cpw (cv x3))))) (λ x3 . cv x1)))) ⟶ (∀ x1 x2 x3 : ο . wb (w3nand x1 x2 x3) (x1 ⟶ x2 ⟶ wn x3)) ⟶ (∀ x1 x2 : ι → ο . wceq (cgcdOLD x1 x2) (csup (crab (λ x3 . wa (wcel (co x1 (cv x3) cdiv) cn) (wcel (co x2 (cv x3) cdiv) cn)) (λ x3 . cn)) cn clt)) ⟶ (∀ x1 : ο . x1 ⟶ cprvb x1) ⟶ (∀ x1 x2 : ο . cprvb (x1 ⟶ x2) ⟶ cprvb x1 ⟶ cprvb x2) ⟶ (∀ x1 : ο . cprvb x1 ⟶ cprvb (cprvb x1)) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wssb x1 x2) (∀ x3 . wceq (cv x3) (cv x2) ⟶ ∀ x4 . wceq (cv x4) (cv x3) ⟶ x1 x4)) ⟶ x0) ⟶ x0
Theorem df_ifs : wceq cifs (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . w3a (wceq (cv x0) (cop (cop (cv x3) (cv x4)) (cop (cv x5) (cv x6)))) (wceq (cv x1) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (w3a (wa (wbr (cv x4) (cop (cv x3) (cv x5)) cbtwn) (wbr (cv x8) (cop (cv x7) (cv x9)) cbtwn)) (wa (wbr (cop (cv x3) (cv x5)) (cop (cv x7) (cv x9)) ccgr) (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr)) (wa (wbr (cop (cv x3) (cv x6)) (cop (cv x7) (cv x10)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x9) (cv x10)) ccgr)))) (λ x10 . cfv (cv x2) cee)) (λ x9 . cfv (cv x2) cee)) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_cgr3 : wceq ccgr3 (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . w3a (wceq (cv x0) (cop (cv x3) (cop (cv x4) (cv x5)))) (wceq (cv x1) (cop (cv x6) (cop (cv x7) (cv x8)))) (w3a (wbr (cop (cv x3) (cv x4)) (cop (cv x6) (cv x7)) ccgr) (wbr (cop (cv x3) (cv x5)) (cop (cv x6) (cv x8)) ccgr) (wbr (cop (cv x4) (cv x5)) (cop (cv x7) (cv x8)) ccgr))) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_fs : wceq cfs (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . w3a (wceq (cv x0) (cop (cop (cv x3) (cv x4)) (cop (cv x5) (cv x6)))) (wceq (cv x1) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (w3a (wbr (cv x3) (cop (cv x4) (cv x5)) ccolin) (wbr (cop (cv x3) (cop (cv x4) (cv x5))) (cop (cv x7) (cop (cv x8) (cv x9))) ccgr3) (wa (wbr (cop (cv x3) (cv x6)) (cop (cv x7) (cv x10)) ccgr) (wbr (cop (cv x4) (cv x6)) (cop (cv x8) (cv x10)) ccgr)))) (λ x10 . cfv (cv x2) cee)) (λ x9 . cfv (cv x2) cee)) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_segle : wceq csegle (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . w3a (wceq (cv x0) (cop (cv x3) (cv x4))) (wceq (cv x1) (cop (cv x5) (cv x6))) (wrex (λ x7 . wa (wbr (cv x7) (cop (cv x5) (cv x6)) cbtwn) (wbr (cop (cv x3) (cv x4)) (cop (cv x5) (cv x7)) ccgr)) (λ x7 . cfv (cv x2) cee))) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_outsideof : wceq coutsideof (cdif ccolin cbtwn) (proof)
Theorem df_line2 : wceq cline2 (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee)) (wne (cv x0) (cv x1))) (wceq (cv x2) (cec (cop (cv x0) (cv x1)) (ccnv ccolin)))) (λ x3 . cn))) (proof)
Theorem df_ray : wceq cray (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee)) (wne (cv x0) (cv x1))) (wceq (cv x2) (crab (λ x4 . wbr (cv x0) (cop (cv x1) (cv x4)) coutsideof) (λ x4 . cfv (cv x3) cee)))) (λ x3 . cn))) (proof)
Theorem df_lines2 : wceq clines2 (crn cline2) (proof)
Theorem df_fwddif : wceq cfwddif (cmpt (λ x0 . co cc cc cpm) (λ x0 . cmpt (λ x1 . crab (λ x2 . wcel (co (cv x2) c1 caddc) (cdm (cv x0))) (λ x2 . cdm (cv x0))) (λ x1 . co (cfv (co (cv x1) c1 caddc) (cv x0)) (cfv (cv x1) (cv x0)) cmin))) (proof)
Theorem df_fwddifn : wceq cfwddifn (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . co cc cc cpm) (λ x0 x1 . cmpt (λ x2 . crab (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) caddc) (cdm (cv x1))) (λ x4 . co cc0 (cv x0) cfz)) (λ x3 . cc)) (λ x2 . csu (co cc0 (cv x0) cfz) (λ x3 . co (co (cv x0) (cv x3) cbc) (co (co (cneg c1) (co (cv x0) (cv x3) cmin) cexp) (cfv (co (cv x2) (cv x3) caddc) (cv x1)) cmul) cmul)))) (proof)
Theorem df_hf : wceq chf (cuni (cima cr1 com)) (proof)
Theorem df_fne : wceq cfne (copab (λ x0 x1 . wa (wceq (cuni (cv x0)) (cuni (cv x1))) (wral (λ x2 . wss (cv x2) (cuni (cin (cv x1) (cpw (cv x2))))) (λ x2 . cv x0)))) (proof)
Theorem df_3nand : ∀ x0 x1 x2 : ο . wb (w3nand x0 x1 x2) (x0 ⟶ x1 ⟶ wn x2) (proof)
Theorem df_gcdOLD : ∀ x0 x1 : ι → ο . wceq (cgcdOLD x0 x1) (csup (crab (λ x2 . wa (wcel (co x0 (cv x2) cdiv) cn) (wcel (co x1 (cv x2) cdiv) cn)) (λ x2 . cn)) cn clt) (proof)
Theorem ax_prv1 : ∀ x0 : ο . x0 ⟶ cprvb x0 (proof)
Theorem ax_prv2 : ∀ x0 x1 : ο . cprvb (x0 ⟶ x1) ⟶ cprvb x0 ⟶ cprvb x1 (proof)
Theorem ax_prv3 : ∀ x0 : ο . cprvb x0 ⟶ cprvb (cprvb x0) (proof)
Theorem df_ssb_b : ∀ x0 : ι → ο . ∀ x1 . wb (wssb x0 x1) (∀ x2 . wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3) (proof)