Proofgold Address

Known ax_c11__ax_c11_b__ax_c11n__ax_c15__ax_c9__ax_c9_b__ax_c9_b1__ax_c9_b2__ax_c9_b3__ax_c14__ax_c16__ax_riotaBAD__df_lsatoms__df_lshyp__df_lcv__df_lfl__df_lkr__df_ldual : ∀ x0 : ο . ((∀ x1 : ι → ι → ο . ∀ x2 x3 . (∀ x4 . wceq (cv x4) (cv x3)) ⟶ (∀ x4 . x1 x4 x3) ⟶ ∀ x4 . x1 x2 x4) ⟶ (∀ x1 : ι → ο . (∀ x2 . wceq (cv x2) (cv x2)) ⟶ (∀ x2 . x1 x2) ⟶ ∀ x2 . x1 x2) ⟶ (∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x2)) ⟶ ∀ x3 . wceq (cv x3) (cv x1)) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . wn (∀ x4 . wceq (cv x4) (cv x2)) ⟶ wceq (cv x3) (cv x2) ⟶ x1 x3 ⟶ ∀ x4 . wceq (cv x4) (cv x2) ⟶ x1 x4) ⟶ (∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wn (∀ x3 . wceq (cv x3) (cv x2)) ⟶ wceq (cv x1) (cv x2) ⟶ ∀ x3 . wceq (cv x1) (cv x2)) ⟶ (∀ x1 . wn (∀ x2 . wceq (cv x2) (cv x2)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x2)) ⟶ wceq (cv x1) (cv x1) ⟶ ∀ x2 . wceq (cv x2) (cv x2)) ⟶ (∀ x1 . wn (∀ x2 . wceq (cv x2) (cv x1)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x1)) ⟶ wceq (cv x1) (cv x1) ⟶ ∀ x2 . wceq (cv x1) (cv x1)) ⟶ (∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x3)) ⟶ wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x1)) ⟶ (∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wn (∀ x3 . wceq (cv x3) (cv x3)) ⟶ wceq (cv x1) (cv x2) ⟶ ∀ x3 . wceq (cv x1) (cv x3)) ⟶ (∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wn (∀ x3 . wceq (cv x3) (cv x2)) ⟶ wcel (cv x1) (cv x2) ⟶ ∀ x3 . wcel (cv x1) (cv x2)) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . (∀ x4 . wceq (cv x4) (cv x2)) ⟶ x1 x3 ⟶ ∀ x4 . x1 x4) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wceq (crio x1 x2) (cif (wreu x1 x2) (cio (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3))) (cfv (cab (λ x3 . wcel (cv x3) (x2 x3))) cund))) ⟶ wceq clsa (cmpt (λ x1 . cvv) (λ x1 . crn (cmpt (λ x2 . cdif (cfv (cv x1) cbs) (csn (cfv (cv x1) c0g))) (λ x2 . cfv (csn (cv x2)) (cfv (cv x1) clspn))))) ⟶ wceq clsh (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wne (cv x2) (cfv (cv x1) cbs)) (wrex (λ x3 . wceq (cfv (cun (cv x2) (csn (cv x3))) (cfv (cv x1) clspn)) (cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs))) (λ x2 . cfv (cv x1) clss))) ⟶ wceq clcv (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cfv (cv x1) clss)) (wcel (cv x3) (cfv (cv x1) clss))) (wa (wpss (cv x2) (cv x3)) (wn (wrex (λ x4 . wa (wpss (cv x2) (cv x4)) (wpss (cv x4) (cv x3))) (λ x4 . cfv (cv x1) clss))))))) ⟶ wceq clfn (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (co (co (cv x3) (cv x4) (cfv (cv x1) cvsca)) (cv x5) (cfv (cv x1) cplusg)) (cv x2)) (co (co (cv x3) (cfv (cv x4) (cv x2)) (cfv (cfv (cv x1) csca) cmulr)) (cfv (cv x5) (cv x2)) (cfv (cfv (cv x1) csca) cplusg))) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cfv (cv x1) csca) cbs)) (λ x2 . co (cfv (cfv (cv x1) csca) cbs) (cfv (cv x1) cbs) cmap))) ⟶ wceq clk (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clfn) (λ x2 . cima (ccnv (cv x2)) (csn (cfv (cfv (cv x1) csca) c0g))))) ⟶ wceq cld (cmpt (λ x1 . cvv) (λ x1 . cun (ctp (cop (cfv cnx cbs) (cfv (cv x1) clfn)) (cop (cfv cnx cplusg) (cres (cof (cfv (cfv (cv x1) csca) cplusg)) (cxp (cfv (cv x1) clfn) (cfv (cv x1) clfn)))) (cop (cfv cnx csca) (cfv (cfv (cv x1) csca) coppr))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x2 x3 . cfv (cfv (cv x1) csca) cbs) (λ x2 x3 . cfv (cv x1) clfn) (λ x2 x3 . co (cv x3) (cxp (cfv (cv x1) cbs) (csn (cv x2))) (cof (cfv (cfv (cv x1) csca) cmulr)))))))) ⟶ x0) ⟶ x0
Theorem ax_c11 : ∀ x0 : ι → ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x2)) ⟶ (∀ x3 . x0 x3 x2) ⟶ ∀ x3 . x0 x1 x3 (proof)
Theorem ax_c11_b : ∀ x0 : ι → ο . (∀ x1 . wceq (cv x1) (cv x1)) ⟶ (∀ x1 . x0 x1) ⟶ ∀ x1 . x0 x1 (proof)
Theorem ax_c11n : ∀ x0 x1 . (∀ x2 . wceq (cv x2) (cv x1)) ⟶ ∀ x2 . wceq (cv x2) (cv x0) (proof)
Theorem ax_c15 : ∀ x0 : ι → ο . ∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wceq (cv x2) (cv x1) ⟶ x0 x2 ⟶ ∀ x3 . wceq (cv x3) (cv x1) ⟶ x0 x3 (proof)
Theorem ax_c9 : ∀ x0 x1 . wn (∀ x2 . wceq (cv x2) (cv x0)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x1)) ⟶ wceq (cv x0) (cv x1) ⟶ ∀ x2 . wceq (cv x0) (cv x1) (proof)
Theorem ax_c9_b : ∀ x0 . wn (∀ x1 . wceq (cv x1) (cv x1)) ⟶ wn (∀ x1 . wceq (cv x1) (cv x1)) ⟶ wceq (cv x0) (cv x0) ⟶ ∀ x1 . wceq (cv x1) (cv x1) (proof)
Theorem ax_c9_b1 : ∀ x0 . wn (∀ x1 . wceq (cv x1) (cv x0)) ⟶ wn (∀ x1 . wceq (cv x1) (cv x0)) ⟶ wceq (cv x0) (cv x0) ⟶ ∀ x1 . wceq (cv x0) (cv x0) (proof)
Theorem ax_c9_b2 : ∀ x0 x1 . wn (∀ x2 . wceq (cv x2) (cv x2)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x0)) ⟶ wceq (cv x1) (cv x0) ⟶ ∀ x2 . wceq (cv x2) (cv x0) (proof)
Theorem ax_c9_b3 : ∀ x0 x1 . wn (∀ x2 . wceq (cv x2) (cv x0)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x2)) ⟶ wceq (cv x0) (cv x1) ⟶ ∀ x2 . wceq (cv x0) (cv x2) (proof)
Theorem ax_c14 : ∀ x0 x1 . wn (∀ x2 . wceq (cv x2) (cv x0)) ⟶ wn (∀ x2 . wceq (cv x2) (cv x1)) ⟶ wcel (cv x0) (cv x1) ⟶ ∀ x2 . wcel (cv x0) (cv x1) (proof)
Theorem ax_c16 : ∀ x0 : ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x1)) ⟶ x0 x2 ⟶ ∀ x3 . x0 x3 (proof)
Theorem ax_riotaBAD : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wceq (crio x0 x1) (cif (wreu x0 x1) (cio (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))) (cfv (cab (λ x2 . wcel (cv x2) (x1 x2))) cund)) (proof)
Theorem df_lsatoms : wceq clsa (cmpt (λ x0 . cvv) (λ x0 . crn (cmpt (λ x1 . cdif (cfv (cv x0) cbs) (csn (cfv (cv x0) c0g))) (λ x1 . cfv (csn (cv x1)) (cfv (cv x0) clspn))))) (proof)
Theorem df_lshyp : wceq clsh (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wne (cv x1) (cfv (cv x0) cbs)) (wrex (λ x2 . wceq (cfv (cun (cv x1) (csn (cv x2))) (cfv (cv x0) clspn)) (cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))) (λ x1 . cfv (cv x0) clss))) (proof)
Theorem df_lcv : wceq clcv (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cfv (cv x0) clss)) (wcel (cv x2) (cfv (cv x0) clss))) (wa (wpss (cv x1) (cv x2)) (wn (wrex (λ x3 . wa (wpss (cv x1) (cv x3)) (wpss (cv x3) (cv x2))) (λ x3 . cfv (cv x0) clss))))))) (proof)
Theorem df_lfl : wceq clfn (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cfv (co (co (cv x2) (cv x3) (cfv (cv x0) cvsca)) (cv x4) (cfv (cv x0) cplusg)) (cv x1)) (co (co (cv x2) (cfv (cv x3) (cv x1)) (cfv (cfv (cv x0) csca) cmulr)) (cfv (cv x4) (cv x1)) (cfv (cfv (cv x0) csca) cplusg))) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cfv (cv x0) csca) cbs)) (λ x1 . co (cfv (cfv (cv x0) csca) cbs) (cfv (cv x0) cbs) cmap))) (proof)
Theorem df_lkr : wceq clk (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clfn) (λ x1 . cima (ccnv (cv x1)) (csn (cfv (cfv (cv x0) csca) c0g))))) (proof)
Theorem df_ldual : wceq cld (cmpt (λ x0 . cvv) (λ x0 . cun (ctp (cop (cfv cnx cbs) (cfv (cv x0) clfn)) (cop (cfv cnx cplusg) (cres (cof (cfv (cfv (cv x0) csca) cplusg)) (cxp (cfv (cv x0) clfn) (cfv (cv x0) clfn)))) (cop (cfv cnx csca) (cfv (cfv (cv x0) csca) coppr))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x1 x2 . cfv (cfv (cv x0) csca) cbs) (λ x1 x2 . cfv (cv x0) clfn) (λ x1 x2 . co (cv x2) (cxp (cfv (cv x0) cbs) (csn (cv x1))) (cof (cfv (cfv (cv x0) csca) cmulr)))))))) (proof)