Search for blocks/addresses/...

Proofgold Proof

pf
Apply 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 with wceq c3o (csuc c2o).
Assume H0: 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)))).
Assume H1: ∀ x0 : ι → ο . wceq (ctpos x0) (ccom x0 (cmpt (λ x1 . cun (ccnv (cdm x0)) (csn c0)) (λ x1 . cuni (ccnv (csn (cv x1)))))).
Assume H2: ∀ x0 : ι → ο . wceq (ccur x0) (cmpt (λ x1 . cdm (cdm x0)) (λ x1 . copab (λ x2 x3 . wbr (cop (cv x1) (cv x2)) (cv x3) x0))).
Assume H3: ∀ x0 : ι → ο . wceq (cunc x0) (coprab (λ x1 x2 x3 . wbr (cv x2) (cv x3) (cfv (cv x1) x0))).
Assume H4: wceq cund (cmpt (λ x0 . cvv) (λ x0 . cpw (cuni (cv x0)))).
Assume H5: ∀ 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)))))).
Assume H6: ∀ 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))).
Assume H7: ∀ x0 : ι → ο . wceq (crecs x0) (cwrecs con0 cep x0).
Assume H8: ∀ 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))))).
Assume H9: ∀ x0 x1 : ι → ο . wceq (cseqom x0 x1) (cima (crdg (cmpt2 (λ x2 x3 . com) (λ x2 x3 . cvv) (λ x2 x3 . cop (csuc (cv x2)) ...)) ...) ...).
...