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.
Assume H2: SNoLe x0 x1.
Apply H0 with even_nat (add_SNo x1 (minus_SNo x0)).
Assume H3: x0omega.
Assume H4: ∀ x2 . x2omegax0 = mul_nat 2 x2∀ x3 : ο . x3.
Apply H1 with even_nat (add_SNo x1 (minus_SNo x0)).
Assume H5: x1omega.
Assume H6: ∀ x2 . x2omegax1 = mul_nat 2 x2∀ x3 : ο . x3.
Claim L7: SNo x0
Apply omega_SNo with x0.
The subproof is completed by applying H3.
Claim L8: SNo x1
Apply omega_SNo with x1.
The subproof is completed by applying H5.
Claim L9: nat_p (add_SNo x1 (minus_SNo x0))
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with add_SNo x1 (minus_SNo x0) leaving 2 subgoals.
Apply int_add_SNo with x1, minus_SNo x0 leaving 2 subgoals.
Apply nat_p_int with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H5.
Apply int_minus_SNo with x0.
Apply nat_p_int with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H3.
Apply add_SNo_minus_Le2b with x1, x0, 0 leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L7.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with x0, λ x2 x3 . SNoLe x3 x1 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H2.
Apply unknownprop_d528c711b690b408e267d5af5f579a6a575d751567ba690169e9696970ff7ca9 with x0, add_SNo x1 (minus_SNo x0), even_nat (add_SNo x1 (minus_SNo x0)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L9.
Assume H10: iff (even_nat (add_SNo x1 (minus_SNo x0))) (odd_nat (add_nat x0 (add_SNo x1 (minus_SNo x0)))).
Assume H11: iff (odd_nat (add_SNo x1 (minus_SNo x0))) (even_nat (add_nat x0 (add_SNo x1 (minus_SNo x0)))).
Apply H10 with even_nat (add_SNo x1 (minus_SNo x0)).
Assume H12: even_nat (add_SNo x1 (minus_SNo x0))odd_nat (add_nat x0 (add_SNo x1 (minus_SNo x0))).
Assume H13: odd_nat (add_nat x0 (add_SNo x1 (minus_SNo x0)))even_nat (add_SNo x1 (minus_SNo x0)).
Apply H13.
Apply add_nat_add_SNo with x0, add_SNo x1 (minus_SNo x0), λ x2 x3 . odd_nat x3 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply nat_p_omega with add_SNo x1 (minus_SNo x0).
The subproof is completed by applying L9.
Apply add_SNo_com with x1, minus_SNo x0, λ x2 x3 . odd_nat (add_SNo x0 x3) leaving 3 subgoals.
The subproof is completed by applying L8.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying L7.
Apply add_SNo_minus_SNo_prop2 with x0, x1, λ x2 x3 . odd_nat x3 leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
The subproof is completed by applying H1.