Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
nat_p
x0
.
Claim L1:
nat_p
(
mul_nat
2
x0
)
Apply mul_nat_p with
2
,
x0
leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying H0.
Apply exactly1of2_E with
even_nat
(
mul_nat
2
x0
)
,
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
,
not
(
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
)
leaving 3 subgoals.
Apply even_nat_xor_S with
mul_nat
2
x0
.
The subproof is completed by applying L1.
Assume H2:
even_nat
(
mul_nat
2
x0
)
.
Assume H3:
not
(
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
)
.
The subproof is completed by applying H3.
Assume H2:
not
(
even_nat
(
mul_nat
2
x0
)
)
.
Apply FalseE with
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
⟶
not
(
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
)
.
Apply H2.
Apply even_nat_double with
x0
.
The subproof is completed by applying H0.
■