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:
∀ x5 .
x5
∈
x2
⟶
x3
x5
=
x4
x5
.
Apply famunion_ext with
x0
,
λ x5 .
{
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x3
x6
)
|x6 ∈
x2
}
,
λ x5 .
{
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x4
x6
)
|x6 ∈
x2
}
.
Let x5 of type
ι
be given.
Assume H1:
x5
∈
x0
.
Apply ReplEq_ext with
x2
,
λ x6 .
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x3
x6
)
,
λ x6 .
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x4
x6
)
.
Let x6 of type
ι
be given.
Assume H2:
x6
∈
x2
.
set y7 to be
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x4
x6
)
Claim L3:
∀ x8 :
ι → ο
.
x8
y7
⟶
x8
(
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x6
(
minus_SNo
x1
)
)
x5
)
)
(
x3
x6
)
)
Let x8 of type
ι
→
ο
be given.
Apply H0 with
y7
,
λ x9 x10 .
(
λ x11 .
x8
)
(
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
y7
(
minus_SNo
x2
)
)
x6
)
)
x9
)
(
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
y7
(
minus_SNo
x2
)
)
x6
)
)
x10
)
.
The subproof is completed by applying H2.
Let x8 of type
ι
→
ι
→
ο
be given.
Apply L3 with
λ x9 .
x8
x9
y7
⟶
x8
y7
x9
.
Assume H4:
x8
y7
y7
.
The subproof is completed by applying H4.
■