Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0int.
Let x1 of type ι be given.
Assume H1: x1int.
Assume H2: mul_SNo 2 x0 = add_SNo (mul_SNo 2 x1) 1.
Apply unknownprop_b9f761a9aaf971afc2c321abccc5415a4ba796124b1aaa309d3f974fda1d3d26 with 2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_3729fc97c8b5f21188ac361733273781ed00775a9662ac2f2237f0346be243d1.
Claim L3: SNo x1
Apply int_SNo with x1.
The subproof is completed by applying H1.
Claim L4: SNo (mul_SNo 2 x1)
Apply SNo_mul_SNo with 2, x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L3.
Claim L5: SNo (mul_SNo 2 x0)
Apply SNo_mul_SNo with 2, x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply int_SNo with x0.
The subproof is completed by applying H0.
Apply mul_SNo_distrL with 2, x0, minus_SNo x1, λ x2 x3 . x3 = 1, λ x2 x3 . divides_int 2 x2 leaving 5 subgoals.
The subproof is completed by applying SNo_2.
Apply int_SNo with x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L3.
Apply mul_SNo_minus_distrR with 2, x1, λ x2 x3 . add_SNo (mul_SNo 2 x0) x3 = 1 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L3.
Apply add_SNo_cancel_L with mul_SNo 2 x1, add_SNo (mul_SNo 2 x0) (minus_SNo (mul_SNo 2 x1)), 1 leaving 4 subgoals.
The subproof is completed by applying L4.
Apply SNo_add_SNo with mul_SNo 2 x0, minus_SNo (mul_SNo 2 x1) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply SNo_minus_SNo with mul_SNo 2 x1.
The subproof is completed by applying L4.
The subproof is completed by applying SNo_1.
Apply H2 with λ x2 x3 . add_SNo (mul_SNo 2 x1) (add_SNo (mul_SNo 2 x0) (minus_SNo (mul_SNo 2 x1))) = x2.
Apply add_SNo_rotate_3_1 with mul_SNo 2 x1, mul_SNo 2 x0, minus_SNo (mul_SNo 2 x1), λ x2 x3 . x3 = mul_SNo 2 x0 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply SNo_minus_SNo with mul_SNo 2 x1.
The subproof is completed by applying L4.
Apply add_SNo_minus_L2 with mul_SNo 2 x1, mul_SNo 2 x0 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply divides_int_mul_SNo_L with 2, 2, add_SNo x0 (minus_SNo x1) leaving 2 subgoals.
Apply int_add_SNo with x0, minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply int_minus_SNo with x1.
The subproof is completed by applying H1.
Apply divides_int_ref with 2.
Apply Subq_omega_int with 2.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.