Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Let x1 of type ι be given.
Assume H1: x1 ∈ setminus omega 1.
Assume H2: mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1).
Apply setminusE with omega, 1, x1, False leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: x1 ∈ omega.
Assume H4: nIn x1 1.
Apply H4.
Apply unknownprop_8d3f603e20bf97bfe46bf78193b0e8c647d78f221edb2afdbdb8c7a12534b868 with x0, x1, λ x2 x3 . x3 ∈ 1 leaving 4 subgoals.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply omega_nat_p with x1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
The subproof is completed by applying In_0_1.
■