Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Assume H0:
80242..
x0
.
Assume H1:
80242..
x1
.
Let x2 of type
ο
be given.
Assume H2:
∀ x3 x4 .
(
∀ x5 .
prim1
x5
x3
⟶
∀ x6 : ο .
(
∀ x7 .
prim1
x7
(
23e07..
x0
)
⟶
∀ x8 .
prim1
x8
(
23e07..
x1
)
⟶
x5
=
bc82c..
(
e6316..
x7
x1
)
(
bc82c..
(
e6316..
x0
x8
)
(
f4dc0..
(
e6316..
x7
x8
)
)
)
⟶
x6
)
⟶
(
∀ x7 .
prim1
x7
(
5246e..
x0
)
⟶
∀ x8 .
prim1
x8
(
5246e..
x1
)
⟶
x5
=
bc82c..
(
e6316..
x7
x1
)
(
bc82c..
(
e6316..
x0
x8
)
(
f4dc0..
(
e6316..
x7
x8
)
)
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
prim1
x5
(
23e07..
x0
)
⟶
∀ x6 .
prim1
x6
(
23e07..
x1
)
⟶
prim1
(
bc82c..
(
e6316..
x5
x1
)
(
bc82c..
(
e6316..
x0
x6
)
(
f4dc0..
(
e6316..
x5
x6
)
)
)
)
x3
)
⟶
(
∀ x5 .
prim1
x5
(
5246e..
x0
)
⟶
∀ x6 .
prim1
x6
(
5246e..
x1
)
⟶
prim1
(
bc82c..
(
e6316..
x5
x1
)
(
bc82c..
(
e6316..
x0
x6
)
(
f4dc0..
(
e6316..
x5
x6
)
)
)
)
x3
)
⟶
(
∀ x5 .
prim1
x5
x4
⟶
∀ x6 : ο .
(
∀ x7 .
prim1
x7
(
23e07..
x0
)
⟶
∀ x8 .
prim1
x8
(
5246e..
x1
)
⟶
x5
=
bc82c..
(
e6316..
x7
x1
)
(
bc82c..
(
e6316..
x0
x8
)
(
f4dc0..
(
e6316..
x7
x8
)
)
)
⟶
x6
)
⟶
(
∀ x7 .
prim1
x7
(
5246e..
x0
)
⟶
∀ x8 .
prim1
x8
(
23e07..
x1
)
⟶
x5
=
bc82c..
(
e6316..
x7
x1
)
(
bc82c..
(
e6316..
x0
x8
)
(
f4dc0..
(
e6316..
x7
x8
)
)
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
prim1
x5
(
23e07..
x0
)
⟶
∀ x6 .
prim1
x6
(
5246e..
x1
)
⟶
prim1
(
bc82c..
(
e6316..
x5
x1
)
(
bc82c..
(
e6316..
x0
x6
)
(
f4dc0..
(
e6316..
x5
x6
)
)
)
)
x4
)
⟶
(
∀ x5 .
prim1
x5
(
5246e..
x0
)
⟶
∀ x6 .
prim1
x6
(
23e07..
x1
)
⟶
prim1
(
bc82c..
(
e6316..
x5
x1
)
(
bc82c..
(
e6316..
x0
x6
)
(
f4dc0..
(
e6316..
x5
x6
)
)
)
)
x4
)
⟶
e6316..
x0
x1
=
02a50..
x3
x4
⟶
x2
.
Apply H2 with
0ac37..
(
94f9e..
(
ac767..
(
23e07..
x0
)
(
23e07..
x1
)
)
(
λ x3 .
bc82c..
(
e6316..
(
f482f..
x3
4a7ef..
)
x1
)
(
bc82c..
(
e6316..
x0
(
f482f..
x3
(
4ae4a..
4a7ef..
)
)
)
(
f4dc0..
(
e6316..
(
f482f..
x3
4a7ef..
)
(
f482f..
x3
(
4ae4a..
...
)
)
)
)
)
)
)
...
,
...
leaving 7 subgoals.
...
...
...
...
...
...
...
■