Search for blocks/addresses/...

Proofgold Proof

pf
Apply df_nfOLD__ax_gen__ax_4__ax_5__df_sb__df_sb_b__ax_6__ax_7__ax_7_b__ax_7_b1__ax_8__ax_8_b__ax_8_b1__ax_9__ax_9_b__ax_9_b1__ax_10__ax_11 with ∀ x0 x1 . wceq (cv x0) (cv x1)wceq (cv x0) (cv x0)wceq (cv x1) (cv x0).
Assume H0: ∀ x0 : ι → ο . wb (wnfOLD (λ x1 . x0 x1)) (∀ x1 . x0 x1∀ x2 . x0 x2).
Assume H1: ∀ x0 : ι → ο . (∀ x1 . x0 x1)∀ x1 . x0 x1.
Assume H2: ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2x1 x2)(∀ x2 . x0 x2)∀ x2 . x1 x2.
Assume H3: ∀ x0 : ο . x0∀ x1 . x0.
Assume H4: ∀ x0 : ι → ο . ∀ x1 x2 . wb (wsb (λ x3 . x0 x3) x1) (wa (wceq (cv x2) (cv x1)x0 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x1)) (x0 x3)))).
Assume H5: ∀ x0 : ι → ο . ∀ x1 . wb (wsb (λ x2 . x0 x2) x1) (wa (wceq (cv x1) (cv x1)x0 x1) (wex (λ x2 . wa (wceq (cv x2) (cv x2)) (x0 x2)))).
Assume H6: ∀ x0 . wn (∀ x1 . wn (wceq (cv x1) (cv x0))).
Assume H7: ∀ x0 x1 x2 . wceq (cv x0) (cv x1)wceq (cv x0) (cv x2)wceq (cv x1) (cv x2).
Assume H8: ∀ x0 x1 . wceq (cv x0) (cv x1)wceq (cv x0) (cv x0)wceq (cv x1) (cv x0).
Assume H9: ∀ x0 x1 . wceq (cv x0) (cv x1)wceq (cv x0) (cv x1)wceq (cv x1) (cv x1).
Assume H10: ∀ x0 x1 x2 . wceq (cv x0) (cv x1)wcel (cv x0) (cv x2)wcel (cv x1) (cv x2).
Assume H11: ∀ x0 x1 . wceq (cv x0) (cv x1)wcel (cv x0) (cv x0)wcel (cv x1) (cv x0).
Assume H12: ∀ x0 x1 . wceq (cv x0) (cv x1)wcel (cv x0) (cv x1)wcel (cv x1) (cv x1).
Assume H13: ∀ x0 x1 x2 . wceq (cv x0) (cv x1)wcel (cv x2) (cv x0)wcel (cv x2) (cv x1).
Assume H14: ∀ x0 x1 . wceq (cv x0) (cv x1)wcel (cv x0) (cv x0)wcel (cv x0) (cv x1).
Assume H15: ∀ x0 x1 . ......wcel (cv ...) ....
...