Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: even_nat x0.
Assume H1: odd_nat x1.
Apply H1 with odd_nat (add_nat x0 x1).
Assume H2: x1 ∈ omega.
Assume H3: ∀ x2 . x2 ∈ omega ⟶ x1 = mul_nat 2 x2 ⟶ ∀ x3 : ο . x3.
Apply unknownprop_4adaec41cb5534e7de6e9f2e22a12d61a97262a6e78399e6df58393eee854625 with x0, x1, odd_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) (even_nat (add_nat x0 x1)).
Assume H5: iff (odd_nat x1) (odd_nat (add_nat x0 x1)).
Apply H5 with odd_nat (add_nat x0 x1).
Assume H6: odd_nat x1 ⟶ odd_nat (add_nat x0 x1).
Assume H7: odd_nat (add_nat x0 x1) ⟶ odd_nat x1.
Apply H6.
The subproof is completed by applying H1.
■