Proofgold Address

Known df_supp__df_tpos__df_cur__df_unc__df_undef__df_wrecs__df_smo__df_recs__df_rdg__df_seqom__df_1o__df_2o__df_3o__df_4o__df_oadd__df_omul__df_oexp__df_er : ∀ x0 : ο . (wceq csupp (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wne (cima (cv x1) (csn (cv x3))) (csn (cv x2))) (λ x3 . cdm (cv x1)))) ⟶ (∀ x1 : ι → ο . wceq (ctpos x1) (ccom x1 (cmpt (λ x2 . cun (ccnv (cdm x1)) (csn c0)) (λ x2 . cuni (ccnv (csn (cv x2))))))) ⟶ (∀ x1 : ι → ο . wceq (ccur x1) (cmpt (λ x2 . cdm (cdm x1)) (λ x2 . copab (λ x3 x4 . wbr (cop (cv x2) (cv x3)) (cv x4) x1)))) ⟶ (∀ x1 : ι → ο . wceq (cunc x1) (coprab (λ x2 x3 x4 . wbr (cv x3) (cv x4) (cfv (cv x2) x1)))) ⟶ wceq cund (cmpt (λ x1 . cvv) (λ x1 . cpw (cuni (cv x1)))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cwrecs x1 x2 x3) (cuni (cab (λ x4 . wex (λ x5 . w3a (wfn (cv x4) (cv x5)) (wa (wss (cv x5) x1) (wral (λ x6 . wss (cpred x1 x2 (cv x6)) (cv x5)) (λ x6 . cv x5))) (wral (λ x6 . wceq (cfv (cv x6) (cv x4)) (cfv (cres (cv x4) (cpred x1 x2 (cv x6))) x3)) (λ x6 . cv x5))))))) ⟶ (∀ x1 : ι → ο . wb (wsmo x1) (w3a (wf (cdm x1) con0 x1) (word (cdm x1)) (wral (λ x2 . wral (λ x3 . wcel (cv x2) (cv x3) ⟶ wcel (cfv (cv x2) x1) (cfv (cv x3) x1)) (λ x3 . cdm x1)) (λ x2 . cdm x1)))) ⟶ (∀ x1 : ι → ο . wceq (crecs x1) (cwrecs con0 cep x1)) ⟶ (∀ x1 x2 : ι → ο . wceq (crdg x1 x2) (crecs (cmpt (λ x3 . cvv) (λ x3 . cif (wceq (cv x3) c0) x2 (cif (wlim (cdm (cv x3))) (cuni (crn (cv x3))) (cfv (cfv (cuni (cdm (cv x3))) (cv x3)) x1)))))) ⟶ (∀ x1 x2 : ι → ο . wceq (cseqom x1 x2) (cima (crdg (cmpt2 (λ x3 x4 . com) (λ x3 x4 . cvv) (λ x3 x4 . cop (csuc (cv x3)) (co (cv x3) (cv x4) x1))) (cop c0 (cfv x2 cid))) com)) ⟶ wceq c1o (csuc c0) ⟶ wceq c2o (csuc c1o) ⟶ wceq c3o (csuc c2o) ⟶ wceq c4o (csuc c3o) ⟶ wceq coa (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . csuc (cv x3))) (cv x1)))) ⟶ wceq comu (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . co (cv x3) (cv x1) coa)) c0))) ⟶ wceq coe (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cif (wceq (cv x1) c0) (cdif c1o (cv x2)) (cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . co (cv x3) (cv x1) comu)) c1o)))) ⟶ (∀ x1 x2 : ι → ο . wb (wer x1 x2) (w3a (wrel x2) (wceq (cdm x2) x1) (wss (cun (ccnv x2) (ccom x2 x2)) x2))) ⟶ x0) ⟶ x0
Theorem df_supp : wceq csupp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wne (cima (cv x0) (csn (cv x2))) (csn (cv x1))) (λ x2 . cdm (cv x0)))) (proof)
Theorem df_tpos : ∀ x0 : ι → ο . wceq (ctpos x0) (ccom x0 (cmpt (λ x1 . cun (ccnv (cdm x0)) (csn c0)) (λ x1 . cuni (ccnv (csn (cv x1)))))) (proof)
Theorem df_cur : ∀ x0 : ι → ο . wceq (ccur x0) (cmpt (λ x1 . cdm (cdm x0)) (λ x1 . copab (λ x2 x3 . wbr (cop (cv x1) (cv x2)) (cv x3) x0))) (proof)
Theorem df_unc : ∀ x0 : ι → ο . wceq (cunc x0) (coprab (λ x1 x2 x3 . wbr (cv x2) (cv x3) (cfv (cv x1) x0))) (proof)
Theorem df_undef : wceq cund (cmpt (λ x0 . cvv) (λ x0 . cpw (cuni (cv x0)))) (proof)
Theorem df_wrecs : ∀ x0 x1 x2 : ι → ο . wceq (cwrecs x0 x1 x2) (cuni (cab (λ x3 . wex (λ x4 . w3a (wfn (cv x3) (cv x4)) (wa (wss (cv x4) x0) (wral (λ x5 . wss (cpred x0 x1 (cv x5)) (cv x4)) (λ x5 . cv x4))) (wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (cfv (cres (cv x3) (cpred x0 x1 (cv x5))) x2)) (λ x5 . cv x4)))))) (proof)
Theorem df_smo : ∀ x0 : ι → ο . wb (wsmo x0) (w3a (wf (cdm x0) con0 x0) (word (cdm x0)) (wral (λ x1 . wral (λ x2 . wcel (cv x1) (cv x2) ⟶ wcel (cfv (cv x1) x0) (cfv (cv x2) x0)) (λ x2 . cdm x0)) (λ x1 . cdm x0))) (proof)
Theorem df_recs : ∀ x0 : ι → ο . wceq (crecs x0) (cwrecs con0 cep x0) (proof)
Theorem df_rdg : ∀ x0 x1 : ι → ο . wceq (crdg x0 x1) (crecs (cmpt (λ x2 . cvv) (λ x2 . cif (wceq (cv x2) c0) x1 (cif (wlim (cdm (cv x2))) (cuni (crn (cv x2))) (cfv (cfv (cuni (cdm (cv x2))) (cv x2)) x0))))) (proof)
Theorem df_seqom : ∀ x0 x1 : ι → ο . wceq (cseqom x0 x1) (cima (crdg (cmpt2 (λ x2 x3 . com) (λ x2 x3 . cvv) (λ x2 x3 . cop (csuc (cv x2)) (co (cv x2) (cv x3) x0))) (cop c0 (cfv x1 cid))) com) (proof)
Theorem df_1o : wceq c1o (csuc c0) (proof)
Theorem df_2o : wceq c2o (csuc c1o) (proof)
Theorem df_3o : wceq c3o (csuc c2o) (proof)
Theorem df_4o : wceq c4o (csuc c3o) (proof)
Theorem df_oadd : wceq coa (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . csuc (cv x2))) (cv x0)))) (proof)
Theorem df_omul : wceq comu (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . co (cv x2) (cv x0) coa)) c0))) (proof)
Theorem df_oexp : wceq coe (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cif (wceq (cv x0) c0) (cdif c1o (cv x1)) (cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . co (cv x2) (cv x0) comu)) c1o)))) (proof)
Theorem df_er : ∀ x0 x1 : ι → ο . wb (wer x0 x1) (w3a (wrel x1) (wceq (cdm x1) x0) (wss (cun (ccnv x1) (ccom x1 x1)) x1)) (proof)