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
.
Claim L2:
...
...
Claim L3:
∀ x2 .
SNo
x2
⟶
SNoLev
x2
∈
SNoLev
(
mul_SNo
x0
x1
)
⟶
SNoLt
(
mul_SNo
x0
x1
)
x2
⟶
(
λ x3 .
or
(
(
λ x4 .
∃ x5 .
and
(
x5
∈
SNoL
x0
)
(
∃ x6 .
and
(
x6
∈
SNoR
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x5
x1
)
(
mul_SNo
x0
x6
)
)
(
add_SNo
x4
(
mul_SNo
x5
x6
)
)
)
)
)
x3
)
(
(
λ x4 .
∃ x5 .
and
(
x5
∈
SNoR
x0
)
(
∃ x6 .
and
(
x6
∈
SNoL
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x5
x1
)
(
mul_SNo
x0
x6
)
)
(
add_SNo
x4
(
mul_SNo
x5
x6
)
)
)
)
)
x3
)
)
x2
Apply SNoLev_ind with
λ x2 .
SNoLev
x2
∈
SNoLev
(
mul_SNo
x0
x1
)
⟶
SNoLt
(
mul_SNo
x0
x1
)
x2
⟶
(
λ x3 .
or
(
(
λ x4 .
∃ x5 .
and
(
x5
∈
SNoL
x0
)
(
∃ x6 .
and
(
x6
∈
SNoR
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x5
x1
)
(
mul_SNo
x0
x6
)
)
(
add_SNo
x4
(
mul_SNo
x5
x6
)
)
)
)
)
x3
)
(
(
λ x4 .
∃ x5 .
and
(
x5
∈
SNoR
x0
)
(
∃ x6 .
and
(
x6
∈
SNoL
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x5
x1
)
(
mul_SNo
x0
x6
)
)
(
add_SNo
x4
(
mul_SNo
x5
x6
)
)
)
)
)
x3
)
)
x2
.
Let x2 of type
ι
be given.
Assume H3:
SNo
x2
.
Assume H4:
∀ x3 .
...
⟶
...
⟶
...
⟶
(
λ x4 .
or
(
(
λ x5 .
∃ x6 .
and
(
x6
∈
SNoL
x0
)
(
∃ x7 .
and
(
x7
∈
SNoR
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x6
x1
)
(
mul_SNo
x0
x7
)
)
(
add_SNo
x5
(
mul_SNo
...
...
)
)
)
)
)
...
)
...
)
...
.
...
Let x2 of type
ι
be given.
Assume H4:
x2
∈
SNoR
(
mul_SNo
x0
x1
)
.
Apply SNoR_E with
mul_SNo
x0
x1
,
x2
,
or
(
∃ x3 .
and
(
x3
∈
SNoL
x0
)
(
∃ x4 .
and
(
x4
∈
SNoR
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x3
x1
)
(
mul_SNo
x0
x4
)
)
(
add_SNo
x2
(
mul_SNo
x3
x4
)
)
)
)
)
(
∃ x3 .
and
(
x3
∈
SNoR
x0
)
(
∃ x4 .
and
(
x4
∈
SNoL
x1
)
(
SNoLe
(
add_SNo
(
mul_SNo
x3
x1
)
(
mul_SNo
x0
x4
)
)
(
add_SNo
x2
(
mul_SNo
x3
x4
)
)
)
)
)
leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H4.
Assume H5:
SNo
x2
.
Assume H6:
SNoLev
x2
∈
SNoLev
(
mul_SNo
x0
x1
)
.
Assume H7:
SNoLt
(
mul_SNo
x0
x1
)
x2
.
Apply L3 with
x2
leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
■