Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CSNo x0.
Claim L1: SNo (minus_SNo (CSNo_Re x0))
Apply SNo_minus_SNo with CSNo_Re x0.
Apply CSNo_ReR with x0.
The subproof is completed by applying H0.
Claim L2: SNo (minus_SNo (CSNo_Im x0))
Apply SNo_minus_SNo with CSNo_Im x0.
Apply CSNo_ImR with x0.
The subproof is completed by applying H0.
Apply CSNo_Re2 with minus_SNo (CSNo_Re x0), minus_SNo (CSNo_Im x0), λ x1 x2 . SNo_pair (add_SNo x2 (CSNo_Re x0)) (add_SNo (CSNo_Im (SNo_pair (minus_SNo (CSNo_Re x0)) (minus_SNo (CSNo_Im x0)))) (CSNo_Im x0)) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply CSNo_Im2 with minus_SNo (CSNo_Re x0), minus_SNo (CSNo_Im x0), λ x1 x2 . SNo_pair (add_SNo (minus_SNo (CSNo_Re x0)) (CSNo_Re x0)) (add_SNo x2 (CSNo_Im x0)) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply add_SNo_minus_SNo_linv with CSNo_Re x0, λ x1 x2 . SNo_pair x2 (add_SNo (minus_SNo (CSNo_Im x0)) (CSNo_Im x0)) = 0 leaving 2 subgoals.
Apply CSNo_ReR with x0.
The subproof is completed by applying H0.
Apply add_SNo_minus_SNo_linv with CSNo_Im x0, λ x1 x2 . SNo_pair 0 x2 = 0 leaving 2 subgoals.
Apply CSNo_ImR with x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_pair_0 with 0.