Proofgold Address

Param HSNo^HSNo : ι → ο
Param mul_HSNo^mul_HSNo : ι → ι → ι
Param CSNo^CSNo : ι → ο
Param HSNo_proj0^HSNo_proj0 : ι → ι
Param HSNo_proj1^HSNo_proj1 : ι → ι
Param conj_CSNo^conj_CSNo : ι → ι
Param mul_CSNo^mul_CSNo : ι → ι → ι
Param minus_CSNo^minus_CSNo : ι → ι
Param add_CSNo^add_CSNo : ι → ι → ι
Known HSNo_proj0proj1_split^{HSNo_proj0proj1_split} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo_proj0 x0 = HSNo_proj0 x1 ⟶ HSNo_proj1 x0 = HSNo_proj1 x1 ⟶ x0 = x1
Known mul_HSNo_proj0^{mul_HSNo_proj0} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo_proj0 (mul_HSNo x0 x1) = add_CSNo (mul_CSNo (HSNo_proj0 x0) (HSNo_proj0 x1)) (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 x1)) (HSNo_proj1 x0)))
Known mul_HSNo_proj1^{mul_HSNo_proj1} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo_proj1 (mul_HSNo x0 x1) = add_CSNo (mul_CSNo (HSNo_proj1 x1) (HSNo_proj0 x0)) (mul_CSNo (HSNo_proj1 x0) (conj_CSNo (HSNo_proj0 x1)))
Known add_CSNo_assoc^{add_CSNo_assoc} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo (add_CSNo x0 x1) x2 = add_CSNo x0 (add_CSNo x1 x2)
Known mul_CSNo_distrL^{mul_CSNo_distrL} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo x0 (add_CSNo x1 x2) = add_CSNo (mul_CSNo x0 x1) (mul_CSNo x0 x2)
Known minus_mul_CSNo_distrR^{minus_mul_CSNo_distrR} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 (minus_CSNo x1) = minus_CSNo (mul_CSNo x0 x1)
Known conj_add_CSNo^{conj_add_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ conj_CSNo (add_CSNo x0 x1) = add_CSNo (conj_CSNo x0) (conj_CSNo x1)
Known conj_mul_CSNo^{conj_mul_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ conj_CSNo (mul_CSNo x0 x1) = mul_CSNo (conj_CSNo x1) (conj_CSNo x0)
Known conj_CSNo_invol^{conj_CSNo_invol} : ∀ x0 . CSNo x0 ⟶ conj_CSNo (conj_CSNo x0) = x0
Known mul_CSNo_distrR^{mul_CSNo_distrR} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo (add_CSNo x0 x1) x2 = add_CSNo (mul_CSNo x0 x2) (mul_CSNo x1 x2)
Known mul_CSNo_assoc^{mul_CSNo_assoc} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo x0 (mul_CSNo x1 x2) = mul_CSNo (mul_CSNo x0 x1) x2
Known minus_add_CSNo^{minus_add_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ minus_CSNo (add_CSNo x0 x1) = add_CSNo (minus_CSNo x0) (minus_CSNo x1)
Known add_CSNo_rotate_3_1^{add_CSNo_rotate_3_1} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 (add_CSNo x1 x2) = add_CSNo x2 (add_CSNo x0 x1)
Known mul_CSNo_rotate_3_1^{mul_CSNo_rotate_3_1} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo x0 (mul_CSNo x1 x2) = mul_CSNo x2 (mul_CSNo x0 x1)
Known minus_mul_CSNo_distrL^{minus_mul_CSNo_distrL} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo (minus_CSNo x0) x1 = minus_CSNo (mul_CSNo x0 x1)
Known conj_minus_CSNo^{conj_minus_CSNo} : ∀ x0 . CSNo x0 ⟶ conj_CSNo (minus_CSNo x0) = minus_CSNo (conj_CSNo x0)
Known mul_CSNo_com^mul_CSNo_com : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 x1 = mul_CSNo x1 x0
Known CSNo_minus_CSNo^{CSNo_minus_CSNo} : ∀ x0 . CSNo x0 ⟶ CSNo (minus_CSNo x0)
Known CSNo_add_CSNo^{CSNo_add_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (add_CSNo x0 x1)
Known CSNo_mul_CSNo^{CSNo_mul_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (mul_CSNo x0 x1)
Known CSNo_conj_CSNo^{CSNo_conj_CSNo} : ∀ x0 . CSNo x0 ⟶ CSNo (conj_CSNo x0)
Known HSNo_proj1R^HSNo_proj1R : ∀ x0 . HSNo x0 ⟶ CSNo (HSNo_proj1 x0)
Known HSNo_proj0R^HSNo_proj0R : ∀ x0 . HSNo x0 ⟶ CSNo (HSNo_proj0 x0)
Known HSNo_mul_HSNo^{HSNo_mul_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo (mul_HSNo x0 x1)
Theorem mul_HSNo_assoc^{mul_HSNo_assoc} : ∀ x0 x1 x2 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ mul_HSNo x0 (mul_HSNo x1 x2) = mul_HSNo (mul_HSNo x0 x1) x2 (proof)