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.
Let x3 of type
ι
→
ι
be given.
Let x4 of type
ι
be given.
Assume H0:
x4
∈
x0
.
Let x5 of type
ι
be given.
Assume H1:
x5
∈
x2
.
Apply famunionI with
x0
,
λ x6 .
{
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x7
(
minus_SNo
x1
)
)
x6
)
)
(
x3
x7
)
|x7 ∈
x2
}
,
x4
,
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x5
(
minus_SNo
x1
)
)
x4
)
)
(
x3
x5
)
leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ReplI with
x2
,
λ x6 .
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x4
)
)
(
x3
x6
)
,
x5
.
The subproof is completed by applying H1.
■