Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
odd_nat
x0
.
Apply H0 with
∀ x1 .
nat_p
x1
⟶
and
(
iff
(
even_nat
x1
)
(
odd_nat
(
add_nat
x0
x1
)
)
)
(
iff
(
odd_nat
x1
)
(
even_nat
(
add_nat
x0
x1
)
)
)
.
Assume H1:
x0
∈
omega
.
Assume H2:
∀ x1 .
x1
∈
omega
⟶
x0
=
mul_nat
2
x1
⟶
∀ x2 : ο .
x2
.
Apply nat_ind with
λ x1 .
and
(
iff
(
even_nat
x1
)
(
odd_nat
(
add_nat
x0
x1
)
)
)
(
iff
(
odd_nat
x1
)
(
even_nat
(
add_nat
x0
x1
)
)
)
leaving 2 subgoals.
Apply add_nat_0R with
x0
,
λ x1 x2 .
and
(
iff
(
even_nat
0
)
(
odd_nat
x2
)
)
(
iff
(
odd_nat
0
)
(
even_nat
x2
)
)
.
Apply andI with
iff
(
even_nat
0
)
(
odd_nat
x0
)
,
iff
(
odd_nat
0
)
(
even_nat
x0
)
leaving 2 subgoals.
Apply iffI with
even_nat
0
,
odd_nat
x0
leaving 2 subgoals.
Assume H3:
even_nat
0
.
The subproof is completed by applying H0.
Assume H3:
odd_nat
x0
.
The subproof is completed by applying even_nat_0.
Apply iffI with
odd_nat
0
,
even_nat
x0
leaving 2 subgoals.
Assume H3:
odd_nat
0
.
Apply FalseE with
even_nat
x0
.
Apply even_nat_not_odd_nat with
0
leaving 2 subgoals.
The subproof is completed by applying even_nat_0.
The subproof is completed by applying H3.
Assume H3:
even_nat
x0
.
Apply FalseE with
odd_nat
0
.
Apply even_nat_not_odd_nat with
x0
leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Let x1 of type
ι
be given.
Assume H3:
nat_p
x1
.
Assume H4:
and
(
iff
(
even_nat
x1
)
(
odd_nat
(
add_nat
x0
x1
)
)
)
(
iff
(
odd_nat
x1
)
(
even_nat
(
add_nat
x0
x1
)
)
)
.
Apply H4 with
and
(
iff
(
even_nat
(
ordsucc
x1
)
)
(
odd_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
(
iff
(
odd_nat
(
ordsucc
x1
)
)
(
even_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
.
Assume H5:
iff
(
even_nat
x1
)
(
odd_nat
(
add_nat
x0
x1
)
)
.
Assume H6:
iff
(
odd_nat
x1
)
(
even_nat
(
add_nat
x0
x1
)
)
.
Apply H5 with
and
(
iff
(
even_nat
(
ordsucc
x1
)
)
(
odd_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
(
iff
(
odd_nat
(
ordsucc
x1
)
)
(
even_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
.
Assume H7:
even_nat
x1
⟶
odd_nat
(
add_nat
x0
x1
)
.
Assume H8:
odd_nat
(
add_nat
x0
x1
)
⟶
even_nat
x1
.
Apply H6 with
and
(
iff
(
even_nat
(
ordsucc
x1
)
)
(
odd_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
(
iff
(
odd_nat
(
ordsucc
x1
)
)
(
even_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
)
.
Assume H9:
odd_nat
x1
⟶
even_nat
(
add_nat
x0
x1
)
.
Assume H10:
even_nat
(
add_nat
x0
x1
)
⟶
odd_nat
x1
.
Apply andI with
iff
(
even_nat
(
ordsucc
x1
)
)
(
odd_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
,
iff
(
odd_nat
(
ordsucc
x1
)
)
(
even_nat
(
add_nat
x0
(
ordsucc
x1
)
)
)
leaving 2 subgoals.
Apply add_nat_SR with
x0
,
x1
,
λ x2 x3 .
iff
(
even_nat
(
ordsucc
x1
)
)
(
odd_nat
x3
)
leaving 2 subgoals.
The subproof is completed by applying H3.
Apply iffI with
even_nat
(
ordsucc
x1
)
,
odd_nat
(
ordsucc
(
add_nat
x0
...
)
)
leaving 2 subgoals.
...
...
...
■