Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Apply unknownprop_4baecc2e952eca39e113b57c19da93bc100e0ff2aac6866a57ba8ff1e36c9807 with x0, x1, λ x2 x3 . add_SNo x3 ((λ x4 . mul_SNo x4 x4) (add_SNo x0 (minus_SNo x1))) = mul_SNo 2 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_3246c662f707e330613d06e6d79b05a85e01933a2790b145f54689259b5bb287 with x0, x1, λ x2 x3 . add_SNo (add_SNo ((λ x4 . mul_SNo x4 x4) x0) (add_SNo (mul_SNo 2 (mul_SNo x0 x1)) ((λ x4 . mul_SNo x4 x4) x1))) x3 = mul_SNo 2 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply add_SNo_com_3_0_1 with (λ x2 . mul_SNo x2 x2) x0, mul_SNo 2 (mul_SNo x0 x1), (λ x2 . mul_SNo x2 x2) x1, λ x2 x3 . add_SNo x3 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo x0 x1))) ((λ x4 . mul_SNo x4 x4) x1))) = mul_SNo 2 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) leaving 4 subgoals.
Apply L2 with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply L2 with x1.
The subproof is completed by applying H1.
Apply add_SNo_com_3_0_1 with (λ x2 . mul_SNo x2 x2) x0, minus_SNo (mul_SNo 2 (mul_SNo x0 x1)), (λ x2 . mul_SNo x2 x2) x1, λ x2 x3 . add_SNo (add_SNo (mul_SNo 2 (mul_SNo x0 x1)) (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1))) x3 = mul_SNo 2 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) leaving 4 subgoals.
Apply L2 with x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with mul_SNo 2 (mul_SNo x0 x1).
The subproof is completed by applying L3.
Apply L2 with x1.
The subproof is completed by applying H1.
Apply add_SNo_com_4_inner_mid with mul_SNo 2 (mul_SNo x0 x1), add_SNo ((λ x2 . mul_SNo x2 x2) x0) ((λ x2 . mul_SNo x2 x2) x1), minus_SNo (mul_SNo 2 (mul_SNo x0 x1)), add_SNo ((λ x2 . mul_SNo x2 x2) x0) ((λ x2 . mul_SNo x2 x2) x1), λ x2 x3 . x3 = mul_SNo 2 (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) leaving 5 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply SNo_minus_SNo with mul_SNo 2 (mul_SNo x0 x1).
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply add_SNo_minus_SNo_rinv with mul_SNo 2 (mul_SNo x0 x1), λ x2 x3 . add_SNo x3 (add_SNo (add_SNo ((λ x4 . mul_SNo x4 x4) x0) ((λ x4 . mul_SNo x4 x4) x1)) (add_SNo ... ...)) = ... leaving 2 subgoals.
...
...
■