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: even_nat x1.
Apply H1 with even_nat (add_nat x0 x1).
Assume H2: x1 ∈ omega.
Assume H3: ∃ x2 . and (x2 ∈ omega) (x1 = mul_nat 2 x2).
Apply unknownprop_4adaec41cb5534e7de6e9f2e22a12d61a97262a6e78399e6df58393eee854625 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) (even_nat (add_nat x0 x1)).
Assume H5: iff (odd_nat x1) (odd_nat (add_nat x0 x1)).
Apply H4 with even_nat (add_nat x0 x1).
Assume H6: even_nat x1 ⟶ even_nat (add_nat x0 x1).
Assume H7: even_nat (add_nat x0 x1) ⟶ even_nat x1.
Apply H6.
The subproof is completed by applying H1.
■