Proofgold Address

Param mul_OSNo^mul_OSNo : ι → ι → ι
Param Complex_i^Complex_i : ι
Param Quaternion_j^Quaternion_j : ι
Param Quaternion_k^Quaternion_k : ι
Param OSNo^OSNo : ι → ο
Param OSNo_proj0^OSNo_proj0 : ι → ι
Param OSNo_proj1^OSNo_proj1 : ι → ι
Known OSNo_proj0proj1_split^{OSNo_proj0proj1_split} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj0 x0 = OSNo_proj0 x1 ⟶ OSNo_proj1 x0 = OSNo_proj1 x1 ⟶ x0 = x1
Known OSNo_p0_k^OSNo_p0_k : OSNo_proj0 Quaternion_k = Quaternion_k
Param add_HSNo^add_HSNo : ι → ι → ι
Param mul_HSNo^mul_HSNo : ι → ι → ι
Param minus_HSNo^minus_HSNo : ι → ι
Param conj_HSNo^conj_HSNo : ι → ι
Known mul_OSNo_proj0^{mul_OSNo_proj0} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj0 (mul_OSNo x0 x1) = add_HSNo (mul_HSNo (OSNo_proj0 x0) (OSNo_proj0 x1)) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 x1)) (OSNo_proj1 x0)))
Known OSNo_p0_i^OSNo_p0_i : OSNo_proj0 Complex_i = Complex_i
Known OSNo_p1_i^OSNo_p1_i : OSNo_proj1 Complex_i = 0
Known OSNo_p0_j^OSNo_p0_j : OSNo_proj0 Quaternion_j = Quaternion_j
Known OSNo_p1_j^OSNo_p1_j : OSNo_proj1 Quaternion_j = 0
Param SNo^SNo : ι → ο
Known conj_HSNo_id_SNo^{conj_HSNo_id_SNo} : ∀ x0 . SNo x0 ⟶ conj_HSNo x0 = x0
Known SNo_0^SNo_0 : SNo 0
Param HSNo^HSNo : ι → ο
Known mul_HSNo_0R^mul_HSNo_0R : ∀ x0 . HSNo x0 ⟶ mul_HSNo x0 0 = 0
Known HSNo_0^HSNo_0 : HSNo 0
Known minus_HSNo_0^minus_HSNo_0 : minus_HSNo 0 = 0
Known add_HSNo_0R^add_HSNo_0R : ∀ x0 . HSNo x0 ⟶ add_HSNo x0 0 = x0
Known HSNo_mul_HSNo^{HSNo_mul_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo (mul_HSNo x0 x1)
Known HSNo_Complex_i^{HSNo_Complex_i} : HSNo Complex_i
Known HSNo_Quaternion_j^{HSNo_Quaternion_j} : HSNo Quaternion_j
Known Quaternion_i_j^{Quaternion_i_j} : mul_HSNo Complex_i Quaternion_j = Quaternion_k
Known OSNo_p1_k^OSNo_p1_k : OSNo_proj1 Quaternion_k = 0
Known mul_OSNo_proj1^{mul_OSNo_proj1} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj1 (mul_OSNo x0 x1) = add_HSNo (mul_HSNo (OSNo_proj1 x1) (OSNo_proj0 x0)) (mul_HSNo (OSNo_proj1 x0) (conj_HSNo (OSNo_proj0 x1)))
Known mul_HSNo_0L^mul_HSNo_0L : ∀ x0 . HSNo x0 ⟶ mul_HSNo 0 x0 = 0
Known HSNo_conj_HSNo^{HSNo_conj_HSNo} : ∀ x0 . HSNo x0 ⟶ HSNo (conj_HSNo x0)
Known add_HSNo_0L^add_HSNo_0L : ∀ x0 . HSNo x0 ⟶ add_HSNo 0 x0 = x0
Known OSNo_mul_OSNo^{OSNo_mul_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo (mul_OSNo x0 x1)
Known OSNo_Quaternion_k^{OSNo_Quaternion_k} : OSNo Quaternion_k
Known OSNo_Quaternion_j^{OSNo_Quaternion_j} : OSNo Quaternion_j
Known OSNo_Complex_i^{OSNo_Complex_i} : OSNo Complex_i
Theorem Octonion_i1_i2^{Octonion_i1_i2} : mul_OSNo Complex_i Quaternion_j = Quaternion_k (proof)
Param minus_OSNo^minus_OSNo : ι → ι
Known OSNo_minus_OSNo^{OSNo_minus_OSNo} : ∀ x0 . OSNo x0 ⟶ OSNo (minus_OSNo x0)
Known minus_OSNo_proj0^{minus_OSNo_proj0} : ∀ x0 . OSNo x0 ⟶ OSNo_proj0 (minus_OSNo x0) = minus_HSNo (OSNo_proj0 x0)
Known Quaternion_j_i^{Quaternion_j_i} : mul_HSNo Quaternion_j Complex_i = minus_HSNo Quaternion_k
Known minus_OSNo_proj1^{minus_OSNo_proj1} : ∀ x0 . OSNo x0 ⟶ OSNo_proj1 (minus_OSNo x0) = minus_HSNo (OSNo_proj1 x0)
Theorem Octonion_i2_i1^{Octonion_i2_i1} : mul_OSNo Quaternion_j Complex_i = minus_OSNo Quaternion_k (proof)
Known HSNo_Quaternion_k^{HSNo_Quaternion_k} : HSNo Quaternion_k
Known Quaternion_j_k^{Quaternion_j_k} : mul_HSNo Quaternion_j Quaternion_k = Complex_i
Theorem Octonion_i2_i4^{Octonion_i2_i4} : mul_OSNo Quaternion_j Quaternion_k = Complex_i (proof)
Known Quaternion_k_j^{Quaternion_k_j} : mul_HSNo Quaternion_k Quaternion_j = minus_HSNo Complex_i
Theorem Octonion_i4_i2^{Octonion_i4_i2} : mul_OSNo Quaternion_k Quaternion_j = minus_OSNo Complex_i (proof)
Known Quaternion_k_i^{Quaternion_k_i} : mul_HSNo Quaternion_k Complex_i = Quaternion_j
Theorem Octonion_i4_i1^{Octonion_i4_i1} : mul_OSNo Quaternion_k Complex_i = Quaternion_j (proof)
Known Quaternion_i_k^{Quaternion_i_k} : mul_HSNo Complex_i Quaternion_k = minus_HSNo Quaternion_j
Theorem Octonion_i1_i4^{Octonion_i1_i4} : mul_OSNo Complex_i Quaternion_k = minus_OSNo Quaternion_j (proof)
Param Octonion_i3^Octonion_i3 : ι
Param Octonion_i5^Octonion_i5 : ι
Known OSNo_p0_i5^OSNo_p0_i5 : OSNo_proj0 Octonion_i5 = 0
Known OSNo_p0_i3^OSNo_p0_i3 : OSNo_proj0 Octonion_i3 = 0
Known OSNo_p1_i3^OSNo_p1_i3 : OSNo_proj1 Octonion_i3 = minus_HSNo Complex_i
Known HSNo_minus_HSNo^{HSNo_minus_HSNo} : ∀ x0 . HSNo x0 ⟶ HSNo (minus_HSNo x0)
Known OSNo_p1_i5^OSNo_p1_i5 : OSNo_proj1 Octonion_i5 = minus_HSNo Quaternion_k
Known minus_mul_HSNo_distrL^{minus_mul_HSNo_distrL} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ mul_HSNo (minus_HSNo x0) x1 = minus_HSNo (mul_HSNo x0 x1)
Known OSNo_Octonion_i5^{OSNo_Octonion_i5} : OSNo Octonion_i5
Known OSNo_Octonion_i3^{OSNo_Octonion_i3} : OSNo Octonion_i3
Theorem Octonion_i2_i3^{Octonion_i2_i3} : mul_OSNo Quaternion_j Octonion_i3 = Octonion_i5 (proof)
Known conj_HSNo_j^conj_HSNo_j : conj_HSNo Quaternion_j = minus_HSNo Quaternion_j
Known minus_mul_HSNo_distrR^{minus_mul_HSNo_distrR} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ mul_HSNo x0 (minus_HSNo x1) = minus_HSNo (mul_HSNo x0 x1)
Known minus_HSNo_invol^{minus_HSNo_invol} : ∀ x0 . HSNo x0 ⟶ minus_HSNo (minus_HSNo x0) = x0
Theorem Octonion_i3_i2^{Octonion_i3_i2} : mul_OSNo Octonion_i3 Quaternion_j = minus_OSNo Octonion_i5 (proof)
Known conj_minus_HSNo^{conj_minus_HSNo} : ∀ x0 . HSNo x0 ⟶ conj_HSNo (minus_HSNo x0) = minus_HSNo (conj_HSNo x0)
Known conj_HSNo_k^conj_HSNo_k : conj_HSNo Quaternion_k = minus_HSNo Quaternion_k
Theorem Octonion_i3_i5^{Octonion_i3_i5} : mul_OSNo Octonion_i3 Octonion_i5 = Quaternion_j (proof)
Known conj_HSNo_i^conj_HSNo_i : conj_HSNo Complex_i = minus_HSNo Complex_i
Theorem Octonion_i5_i3^{Octonion_i5_i3} : mul_OSNo Octonion_i5 Octonion_i3 = minus_OSNo Quaternion_j (proof)
Theorem Octonion_i5_i2^{Octonion_i5_i2} : mul_OSNo Octonion_i5 Quaternion_j = Octonion_i3 (proof)
Theorem Octonion_i2_i5^{Octonion_i2_i5} : mul_OSNo Quaternion_j Octonion_i5 = minus_OSNo Octonion_i3 (proof)
Param Octonion_i6^Octonion_i6 : ι
Known OSNo_p0_i6^OSNo_p0_i6 : OSNo_proj0 Octonion_i6 = 0
Known OSNo_p1_i6^OSNo_p1_i6 : OSNo_proj1 Octonion_i6 = minus_HSNo Quaternion_j
Known OSNo_Octonion_i6^{OSNo_Octonion_i6} : OSNo Octonion_i6
Theorem Octonion_i3_i4^{Octonion_i3_i4} : mul_OSNo Octonion_i3 Quaternion_k = Octonion_i6 (proof)
Theorem Octonion_i4_i3^{Octonion_i4_i3} : mul_OSNo Quaternion_k Octonion_i3 = minus_OSNo Octonion_i6 (proof)
Theorem Octonion_i4_i6^{Octonion_i4_i6} : mul_OSNo Quaternion_k Octonion_i6 = Octonion_i3 (proof)
Theorem Octonion_i6_i4^{Octonion_i6_i4} : mul_OSNo Octonion_i6 Quaternion_k = minus_OSNo Octonion_i3 (proof)
Theorem Octonion_i6_i3^{Octonion_i6_i3} : mul_OSNo Octonion_i6 Octonion_i3 = Quaternion_k (proof)
Theorem Octonion_i3_i6^{Octonion_i3_i6} : mul_OSNo Octonion_i3 Octonion_i6 = minus_OSNo Quaternion_k (proof)
Param Octonion_i0^Octonion_i0 : ι
Known OSNo_p0_i0^OSNo_p0_i0 : OSNo_proj0 Octonion_i0 = 0
Param ordsucc^ordsucc : ι → ι
Known OSNo_p1_i0^OSNo_p1_i0 : OSNo_proj1 Octonion_i0 = 1
Known Quaternion_k_sqr^{Quaternion_k_sqr} : mul_HSNo Quaternion_k Quaternion_k = minus_HSNo 1
Known HSNo_1^HSNo_1 : HSNo 1
Known OSNo_Octonion_i0^{OSNo_Octonion_i0} : OSNo Octonion_i0
Theorem Octonion_i4_i5^{Octonion_i4_i5} : mul_OSNo Quaternion_k Octonion_i5 = Octonion_i0 (proof)
Theorem Octonion_i5_i4^{Octonion_i5_i4} : mul_OSNo Octonion_i5 Quaternion_k = minus_OSNo Octonion_i0 (proof)
Known SNo_1^SNo_1 : SNo 1
Known mul_HSNo_1L^mul_HSNo_1L : ∀ x0 . HSNo x0 ⟶ mul_HSNo 1 x0 = x0
Theorem Octonion_i5_i0^{Octonion_i5_i0} : mul_OSNo Octonion_i5 Octonion_i0 = Quaternion_k (proof)
Known mul_HSNo_1R^mul_HSNo_1R : ∀ x0 . HSNo x0 ⟶ mul_HSNo x0 1 = x0
Theorem Octonion_i0_i5^{Octonion_i0_i5} : mul_OSNo Octonion_i0 Octonion_i5 = minus_OSNo Quaternion_k (proof)
Theorem Octonion_i0_i4^{Octonion_i0_i4} : mul_OSNo Octonion_i0 Quaternion_k = Octonion_i5 (proof)
Theorem Octonion_i4_i0^{Octonion_i4_i0} : mul_OSNo Quaternion_k Octonion_i0 = minus_OSNo Octonion_i5 (proof)
Theorem Octonion_i5_i6^{Octonion_i5_i6} : mul_OSNo Octonion_i5 Octonion_i6 = Complex_i (proof)
Theorem Octonion_i6_i5^{Octonion_i6_i5} : mul_OSNo Octonion_i6 Octonion_i5 = minus_OSNo Complex_i (proof)
Theorem Octonion_i6_i1^{Octonion_i6_i1} : mul_OSNo Octonion_i6 Complex_i = Octonion_i5 (proof)
Theorem Octonion_i1_i6^{Octonion_i1_i6} : mul_OSNo Complex_i Octonion_i6 = minus_OSNo Octonion_i5 (proof)
Theorem Octonion_i1_i5^{Octonion_i1_i5} : mul_OSNo Complex_i Octonion_i5 = Octonion_i6 (proof)
Theorem Octonion_i5_i1^{Octonion_i5_i1} : mul_OSNo Octonion_i5 Complex_i = minus_OSNo Octonion_i6 (proof)
Theorem Octonion_i6_i0^{Octonion_i6_i0} : mul_OSNo Octonion_i6 Octonion_i0 = Quaternion_j (proof)
Theorem Octonion_i0_i6^{Octonion_i0_i6} : mul_OSNo Octonion_i0 Octonion_i6 = minus_OSNo Quaternion_j (proof)
Theorem Octonion_i0_i2^{Octonion_i0_i2} : mul_OSNo Octonion_i0 Quaternion_j = Octonion_i6 (proof)
Theorem Octonion_i2_i0^{Octonion_i2_i0} : mul_OSNo Quaternion_j Octonion_i0 = minus_OSNo Octonion_i6 (proof)
Known Quaternion_j_sqr^{Quaternion_j_sqr} : mul_HSNo Quaternion_j Quaternion_j = minus_HSNo 1
Theorem Octonion_i2_i6^{Octonion_i2_i6} : mul_OSNo Quaternion_j Octonion_i6 = Octonion_i0 (proof)
Theorem Octonion_i6_i2^{Octonion_i6_i2} : mul_OSNo Octonion_i6 Quaternion_j = minus_OSNo Octonion_i0 (proof)
Theorem Octonion_i0_i1^{Octonion_i0_i1} : mul_OSNo Octonion_i0 Complex_i = Octonion_i3 (proof)
Theorem Octonion_i1_i0^{Octonion_i1_i0} : mul_OSNo Complex_i Octonion_i0 = minus_OSNo Octonion_i3 (proof)
Known Quaternion_i_sqr^{Quaternion_i_sqr} : mul_HSNo Complex_i Complex_i = minus_HSNo 1
Theorem Octonion_i1_i3^{Octonion_i1_i3} : mul_OSNo Complex_i Octonion_i3 = Octonion_i0 (proof)
Theorem Octonion_i3_i1^{Octonion_i3_i1} : mul_OSNo Octonion_i3 Complex_i = minus_OSNo Octonion_i0 (proof)
Theorem Octonion_i3_i0^{Octonion_i3_i0} : mul_OSNo Octonion_i3 Octonion_i0 = Complex_i (proof)
Theorem Octonion_i0_i3^{Octonion_i0_i3} : mul_OSNo Octonion_i0 Octonion_i3 = minus_OSNo Complex_i (proof)