Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
→
ι
be given.
Let x2 of type
ι
be given.
Assume H0:
x2
∈
Pi
x0
x1
.
Apply Pi_eta with
x0
,
x1
,
x2
,
λ x3 x4 .
x3
∈
V_
(
ordsucc
(
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x5 .
ordsucc
(
9d271..
(
x1
x5
)
)
)
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_283f8fc5ea1a3c99f01ef684040d36f3b3e77f532f79e28eeabcc4dccf9b7028 with
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
)
,
lam
x0
(
λ x3 .
ap
x2
x3
)
.
Claim L1:
...
...
Claim L2:
...
...
Claim L3:
...
...
Claim L4:
...
...
Claim L5:
...
...
Apply Subq_tra with
lam
x0
(
λ x3 .
ap
x2
x3
)
,
V_
(
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
)
)
)
,
V_
(
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying unknownprop_28964ee8cad97b0e7f84687c91ac3b2c14907ff8ade27945336d88e3a0d67591 with
x0
,
λ x3 .
ap
x2
x3
.
Apply V_Subq_2 with
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
)
)
,
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
)
.
Apply Subq_tra with
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
)
)
,
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
)
,
V_
(
ordsucc
(
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
)
)
leaving 2 subgoals.
Apply unknownprop_7efa9b0eb4a7672f89f79f79d5dfd89fdd189d47f4be668ddc1bdc4223ecb821 with
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
)
,
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply binunion_Subq_min with
ordsucc
(
9d271..
x0
)
,
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
,
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying binunion_Subq_1 with
ordsucc
(
9d271..
x0
)
,
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
.
Apply Subq_tra with
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
ap
x2
x3
)
)
)
,
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
,
binunion
(
ordsucc
(
9d271..
x0
)
)
(
famunion
x0
(
λ x3 .
ordsucc
(
9d271..
(
x1
x3
)
)
)
)
leaving 2 subgoals.
Let x3 of type
ι
be given.
Assume H6:
x3
∈
famunion
x0
(
λ x4 .
ordsucc
(
9d271..
(
ap
x2
x4
)
)
)
.
Apply famunionE_impred with
x0
,
λ x4 .
ordsucc
(
9d271..
(
ap
x2
x4
)
)
,
x3
,
x3
∈
famunion
x0
(
λ x4 .
ordsucc
(
9d271..
(
x1
x4
)
)
)
leaving 2 subgoals.
The subproof is completed by applying H6.
Let x4 of type
ι
be given.
Assume H7:
x4
∈
x0
.
Assume H8:
...
∈
...
.
...
...
...
■