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
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
)
)
)
.
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
...
⟶
wceq
(
cv
x1
)
(
cv
x0
)
⟶
∀ x2 .
wceq
(
cv
x2
)
(
cv
x0
)
.
...
■