Search for blocks/addresses/...

Proofgold Proof

pf
Apply 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 with 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)))))))).
Assume H0: ∀ x0 : ι → ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x2))(∀ x3 . x0 x3 x2)∀ x3 . x0 x1 x3.
Assume H1: ∀ x0 : ι → ο . (∀ x1 . wceq (cv x1) (cv x1))(∀ x1 . x0 x1)∀ x1 . x0 x1.
Assume H2: ∀ x0 x1 . (∀ x2 . wceq (cv x2) (cv x1))∀ x2 . wceq (cv x2) (cv x0).
Assume H3: ∀ 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.
Assume H4: ∀ 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).
Assume H5: ∀ 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).
Assume H6: ∀ 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).
Assume H7: ∀ x0 x1 . ...wn (∀ x2 . wceq (cv x2) (cv x0))wceq (cv x1) (cv x0)∀ x2 . wceq (cv x2) (cv x0).
...