Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Assume H0:
SNo
x0
.
Assume H1:
SNo
x1
.
Let x2 of type
ο
be given.
Assume H2:
∀ x3 x4 .
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 : ο .
(
∀ x7 .
x7
∈
SNoL
x0
⟶
∀ x8 .
x8
∈
SNoL
x1
⟶
x5
=
add_SNo
(
mul_SNo
x7
x1
)
(
add_SNo
(
mul_SNo
x0
x8
)
(
minus_SNo
(
mul_SNo
x7
x8
)
)
)
⟶
x6
)
⟶
(
∀ x7 .
x7
∈
SNoR
x0
⟶
∀ x8 .
x8
∈
SNoR
x1
⟶
x5
=
add_SNo
(
mul_SNo
x7
x1
)
(
add_SNo
(
mul_SNo
x0
x8
)
(
minus_SNo
(
mul_SNo
x7
x8
)
)
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
x5
∈
SNoL
x0
⟶
∀ x6 .
x6
∈
SNoL
x1
⟶
add_SNo
(
mul_SNo
x5
x1
)
(
add_SNo
(
mul_SNo
x0
x6
)
(
minus_SNo
(
mul_SNo
x5
x6
)
)
)
∈
x3
)
⟶
(
∀ x5 .
x5
∈
SNoR
x0
⟶
∀ x6 .
x6
∈
SNoR
x1
⟶
add_SNo
(
mul_SNo
x5
x1
)
(
add_SNo
(
mul_SNo
x0
x6
)
(
minus_SNo
(
mul_SNo
x5
x6
)
)
)
∈
x3
)
⟶
(
∀ x5 .
x5
∈
x4
⟶
∀ x6 : ο .
(
∀ x7 .
x7
∈
SNoL
x0
⟶
∀ x8 .
x8
∈
SNoR
x1
⟶
x5
=
add_SNo
(
mul_SNo
x7
x1
)
(
add_SNo
(
mul_SNo
x0
x8
)
(
minus_SNo
(
mul_SNo
x7
x8
)
)
)
⟶
x6
)
⟶
(
∀ x7 .
x7
∈
SNoR
x0
⟶
∀ x8 .
x8
∈
SNoL
x1
⟶
x5
=
add_SNo
(
mul_SNo
x7
x1
)
(
add_SNo
(
mul_SNo
x0
x8
)
(
minus_SNo
(
mul_SNo
x7
x8
)
)
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
x5
∈
SNoL
x0
⟶
∀ x6 .
x6
∈
SNoR
x1
⟶
add_SNo
(
mul_SNo
x5
x1
)
(
add_SNo
(
mul_SNo
x0
x6
)
(
minus_SNo
(
mul_SNo
x5
x6
)
)
)
∈
x4
)
⟶
(
∀ x5 .
x5
∈
SNoR
x0
⟶
∀ x6 .
x6
∈
SNoL
x1
⟶
add_SNo
(
mul_SNo
x5
x1
)
(
add_SNo
(
mul_SNo
x0
x6
)
(
minus_SNo
(
mul_SNo
x5
x6
)
)
)
∈
x4
)
⟶
mul_SNo
x0
x1
=
SNoCut
x3
x4
⟶
x2
.
Apply H2 with
binunion
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
(
mul_SNo
x0
(
ap
x3
1
)
)
(
minus_SNo
(
mul_SNo
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoL
x1
)
}
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
...
...
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoR
x1
)
}
,
...
leaving 7 subgoals.
...
...
...
...
...
...
...
■