Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ο
be given.
Assume H0:
∀ x1 .
and
(
707bb..
8ac9a..
x1
)
(
∀ x2 .
d701e..
(
de327..
8ac9a..
x2
)
(
57d6a..
x1
x2
)
(
57d6a..
x2
(
57d6a..
x1
x2
)
)
)
⟶
x0
.
Apply H0 with
56103..
(
λ x1 .
57d6a..
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
)
.
Claim L1:
...
...
Claim L2:
...
...
Apply andI with
707bb..
8ac9a..
(
56103..
(
λ x1 .
57d6a..
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
)
)
,
∀ x1 .
d701e..
(
de327..
8ac9a..
x1
)
(
57d6a..
(
56103..
(
λ x2 .
57d6a..
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
)
)
x1
)
(
57d6a..
x1
(
57d6a..
(
56103..
(
λ x2 .
57d6a..
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
)
)
x1
)
)
leaving 2 subgoals.
Apply unknownprop_48bdd6a657f347e61951e7c156219665659681230736ec34551e878152deeb27 with
8ac9a..
,
λ x1 .
57d6a..
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
.
Let x1 of type
ι
be given.
Apply unknownprop_8ec5ea156e4dc55673ac5ebd5ebb022d9fce63b1e0405450a8c091cca6c01abf with
de327..
8ac9a..
x1
,
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
,
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
leaving 2 subgoals.
The subproof is completed by applying L2 with
8ac9a..
,
x1
.
The subproof is completed by applying L2 with
8ac9a..
,
x1
.
Let x1 of type
ι
be given.
Claim L3:
...
...
Claim L4:
...
...
Claim L5:
...
...
Apply unknownprop_308457d7c52152c6c671a13996e2ade50c08f50b0694cbe5ee78854c92f90b29 with
de327..
8ac9a..
x1
,
57d6a..
(
56103..
(
λ x2 .
57d6a..
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
)
)
x1
,
57d6a..
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
,
57d6a..
x1
(
57d6a..
(
56103..
(
λ x2 .
57d6a..
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
(
(
λ x3 .
56103..
(
λ x4 .
57d6a..
x3
(
57d6a..
x4
x4
)
)
)
x2
)
)
)
x1
)
leaving 2 subgoals.
The subproof is completed by applying L4.
Apply unknownprop_308457d7c52152c6c671a13996e2ade50c08f50b0694cbe5ee78854c92f90b29 with
de327..
8ac9a..
x1
,
57d6a..
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
x1
)
(
(
λ x2 .
56103..
(
λ x3 .
57d6a..
x2
(
57d6a..
x3
x3
)
)
)
...
)
,
...
,
...
leaving 2 subgoals.
...
...
■