Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: odd_nat x0.
Assume H1: odd_nat x1.
Apply H1 with even_nat (add_nat x0 x1).
Assume H2: x1 ∈ omega.
Assume H3: ∀ x2 . x2 ∈ omega ⟶ x1 = mul_nat 2 x2 ⟶ ∀ x3 : ο . x3.
Apply unknownprop_d528c711b690b408e267d5af5f579a6a575d751567ba690169e9696970ff7ca9 with x0, x1, even_nat (add_nat x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Assume H4: iff (even_nat x1) (odd_nat (add_nat x0 x1)).
Assume H5: iff (odd_nat x1) (even_nat (add_nat x0 x1)).
Apply H5 with even_nat (add_nat x0 x1).
Assume H6: odd_nat x1 ⟶ even_nat (add_nat x0 x1).
Assume H7: even_nat (add_nat x0 x1) ⟶ odd_nat x1.
Apply H6.
The subproof is completed by applying H1.
■