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 ∈ omega.
Let x2 of type ι be given.
Assume H2: x2 ∈ omega.
Let x3 of type ι be given.
Assume H3: x3 ∈ omega.
Assume H4: nat_pair x0 x1 = nat_pair x2 x3.
Claim L5: SNo (mul_SNo 2 x1)
Apply SNo_mul_SNo with 2, x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_SNo with x1.
The subproof is completed by applying H1.
Claim L6: SNo (mul_SNo 2 x3)
Apply SNo_mul_SNo with 2, x3 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_SNo with x3.
The subproof is completed by applying H3.
Apply mul_SNo_nonzero_cancel with 2, x1, x3 leaving 5 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying neq_2_0.
Apply omega_SNo with x1.
The subproof is completed by applying H1.
Apply omega_SNo with x3.
The subproof is completed by applying H3.
Apply add_SNo_cancel_R with mul_SNo 2 x1, 1, mul_SNo 2 x3 leaving 4 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L6.
Apply mul_SNo_nonzero_cancel with exp_SNo_nat 2 x0, add_SNo (mul_SNo 2 x1) 1, add_SNo (mul_SNo 2 x3) 1 leaving 5 subgoals.
Apply SNo_exp_SNo_nat with 2, x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Assume H7: exp_SNo_nat 2 x0 = 0.
Apply neq_1_0.
Apply mul_SNo_eps_power_2 with x0, λ x4 x5 . x4 = 0 leaving 2 subgoals.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply H7 with λ x4 x5 . mul_SNo (eps_ x0) x5 = 0.
Apply mul_SNo_zeroR with eps_ x0.
Apply SNo_eps_ with x0.
The subproof is completed by applying H0.
Apply SNo_add_SNo with mul_SNo 2 x1, 1 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying SNo_1.
Apply SNo_add_SNo with mul_SNo 2 x3, 1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying SNo_1.
Apply nat_pair_0 with x0, x1, x2, x3, λ x4 x5 . mul_SNo (exp_SNo_nat 2 x0) (add_SNo (mul_SNo 2 x1) 1) = mul_SNo (exp_SNo_nat 2 x5) (add_SNo (mul_SNo 2 x3) 1) leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
■