Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ quaternion.
Let x1 of type ι be given.
Assume H1: x1 ∈ quaternion.
Apply quaternion_I with add_CSNo (HSNo_proj0 x0) (HSNo_proj0 x1), add_CSNo (HSNo_proj1 x0) (HSNo_proj1 x1) leaving 2 subgoals.
Apply complex_add_CSNo with HSNo_proj0 x0, HSNo_proj0 x1 leaving 2 subgoals.
Apply quaternion_p0_complex with x0.
The subproof is completed by applying H0.
Apply quaternion_p0_complex with x1.
The subproof is completed by applying H1.
Apply complex_add_CSNo with HSNo_proj1 x0, HSNo_proj1 x1 leaving 2 subgoals.
Apply quaternion_p1_complex with x0.
The subproof is completed by applying H0.
Apply quaternion_p1_complex with x1.
The subproof is completed by applying H1.
■