Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_ind with
λ x0 .
exactly1of2
(
even_nat
x0
)
(
even_nat
(
ordsucc
x0
)
)
leaving 2 subgoals.
Apply exactly1of2_I1 with
even_nat
0
,
even_nat
1
leaving 2 subgoals.
Apply andI with
0
∈
omega
,
∃ x0 .
and
(
x0
∈
omega
)
(
0
=
mul_nat
2
x0
)
leaving 2 subgoals.
Apply nat_p_omega with
0
.
The subproof is completed by applying nat_0.
Let x0 of type
ο
be given.
Assume H0:
∀ x1 .
and
(
x1
∈
omega
)
(
0
=
mul_nat
2
x1
)
⟶
x0
.
Apply H0 with
0
.
Apply andI with
0
∈
omega
,
0
=
mul_nat
2
0
leaving 2 subgoals.
Apply nat_p_omega with
0
.
The subproof is completed by applying nat_0.
Let x1 of type
ι
→
ι
→
ο
be given.
The subproof is completed by applying mul_nat_0R with
2
,
λ x2 x3 .
x1
x3
x2
.
Assume H0:
even_nat
1
.
Apply even_nat_not_odd_nat with
1
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying odd_nat_1.
Let x0 of type
ι
be given.
Assume H0:
nat_p
x0
.
Assume H1:
exactly1of2
(
even_nat
x0
)
(
even_nat
(
ordsucc
x0
)
)
.
Apply exactly1of2_E with
even_nat
x0
,
even_nat
(
ordsucc
x0
)
,
exactly1of2
(
even_nat
(
ordsucc
x0
)
)
(
even_nat
(
ordsucc
(
ordsucc
x0
)
)
)
leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2:
even_nat
x0
.
Assume H3:
not
(
even_nat
(
ordsucc
x0
)
)
.
Apply exactly1of2_I2 with
even_nat
(
ordsucc
x0
)
,
even_nat
(
ordsucc
(
ordsucc
x0
)
)
leaving 2 subgoals.
The subproof is completed by applying H3.
Apply even_nat_S_S with
x0
.
The subproof is completed by applying H2.
Assume H2:
not
(
even_nat
x0
)
.
Assume H3:
even_nat
(
ordsucc
x0
)
.
Apply exactly1of2_I1 with
even_nat
(
ordsucc
x0
)
,
even_nat
(
ordsucc
(
ordsucc
x0
)
)
leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4:
even_nat
(
ordsucc
(
ordsucc
x0
)
)
.
Apply H2.
Apply even_nat_S_S_inv with
x0
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
■