Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: CSNo x0.
Assume H1: CSNo x1.
Apply CSNo_Re2 with add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1))), add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)) leaving 2 subgoals.
Apply unknownprop_49f3cf70b605b44eb2822fe91c57bca94bae304f4b9278fa190485d2a33fdf59 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_57767f805436b599e99b8ac6663fa6b7758904d24620ff860a059bb817bebc7c with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.