Search for blocks/addresses/...

Proofgold Asset

asset id
0018b1beed025c8f1e40268977468110ac850759e42f306058f197c3b53b990b
asset hash
99910c1dd3943fe5e02ad4a23189d8bf1b81f382f7d602f91185a9382619041d
bday / block
28532
tx
8dbba..
preasset
doc published by PrQUS..
Param mul_OSNomul_OSNo : ιιι
Param Complex_iComplex_i : ι
Param Quaternion_jQuaternion_j : ι
Param Quaternion_kQuaternion_k : ι
Param OSNoOSNo : ιο
Param OSNo_proj0OSNo_proj0 : ιι
Param OSNo_proj1OSNo_proj1 : ιι
Known OSNo_proj0proj1_splitOSNo_proj0proj1_split : ∀ x0 x1 . OSNo x0OSNo x1OSNo_proj0 x0 = OSNo_proj0 x1OSNo_proj1 x0 = OSNo_proj1 x1x0 = x1
Known OSNo_p0_kOSNo_p0_k : OSNo_proj0 Quaternion_k = Quaternion_k
Param add_HSNoadd_HSNo : ιιι
Param mul_HSNomul_HSNo : ιιι
Param minus_HSNominus_HSNo : ιι
Param conj_HSNoconj_HSNo : ιι
Known mul_OSNo_proj0mul_OSNo_proj0 : ∀ x0 x1 . OSNo x0OSNo x1OSNo_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_iOSNo_p0_i : OSNo_proj0 Complex_i = Complex_i
Known OSNo_p1_iOSNo_p1_i : OSNo_proj1 Complex_i = 0
Known OSNo_p0_jOSNo_p0_j : OSNo_proj0 Quaternion_j = Quaternion_j
Known OSNo_p1_jOSNo_p1_j : OSNo_proj1 Quaternion_j = 0
Param SNoSNo : ιο
Known conj_HSNo_id_SNoconj_HSNo_id_SNo : ∀ x0 . SNo x0conj_HSNo x0 = x0
Known SNo_0SNo_0 : SNo 0
Param HSNoHSNo : ιο
Known mul_HSNo_0Rmul_HSNo_0R : ∀ x0 . HSNo x0mul_HSNo x0 0 = 0
Known HSNo_0HSNo_0 : HSNo 0
Known minus_HSNo_0minus_HSNo_0 : minus_HSNo 0 = 0
Known add_HSNo_0Radd_HSNo_0R : ∀ x0 . HSNo x0add_HSNo x0 0 = x0
Known HSNo_mul_HSNoHSNo_mul_HSNo : ∀ x0 x1 . HSNo x0HSNo x1HSNo (mul_HSNo x0 x1)
Known HSNo_Complex_iHSNo_Complex_i : HSNo Complex_i
Known HSNo_Quaternion_jHSNo_Quaternion_j : HSNo Quaternion_j
Known Quaternion_i_jQuaternion_i_j : mul_HSNo Complex_i Quaternion_j = Quaternion_k
Known OSNo_p1_kOSNo_p1_k : OSNo_proj1 Quaternion_k = 0
Known mul_OSNo_proj1mul_OSNo_proj1 : ∀ x0 x1 . OSNo x0OSNo x1OSNo_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_0Lmul_HSNo_0L : ∀ x0 . HSNo x0mul_HSNo 0 x0 = 0
Known HSNo_conj_HSNoHSNo_conj_HSNo : ∀ x0 . HSNo x0HSNo (conj_HSNo x0)
Known add_HSNo_0Ladd_HSNo_0L : ∀ x0 . HSNo x0add_HSNo 0 x0 = x0
Known OSNo_mul_OSNoOSNo_mul_OSNo : ∀ x0 x1 . OSNo x0OSNo x1OSNo (mul_OSNo x0 x1)
Known OSNo_Quaternion_kOSNo_Quaternion_k : OSNo Quaternion_k
Known OSNo_Quaternion_jOSNo_Quaternion_j : OSNo Quaternion_j
Known OSNo_Complex_iOSNo_Complex_i : OSNo Complex_i
Theorem Octonion_i1_i2Octonion_i1_i2 : mul_OSNo Complex_i Quaternion_j = Quaternion_k (proof)
Param minus_OSNominus_OSNo : ιι
Known OSNo_minus_OSNoOSNo_minus_OSNo : ∀ x0 . OSNo x0OSNo (minus_OSNo x0)
Known minus_OSNo_proj0minus_OSNo_proj0 : ∀ x0 . OSNo x0OSNo_proj0 (minus_OSNo x0) = minus_HSNo (OSNo_proj0 x0)
Known Quaternion_j_iQuaternion_j_i : mul_HSNo Quaternion_j Complex_i = minus_HSNo Quaternion_k
Known minus_OSNo_proj1minus_OSNo_proj1 : ∀ x0 . OSNo x0OSNo_proj1 (minus_OSNo x0) = minus_HSNo (OSNo_proj1 x0)
Theorem Octonion_i2_i1Octonion_i2_i1 : mul_OSNo Quaternion_j Complex_i = minus_OSNo Quaternion_k (proof)
Known HSNo_Quaternion_kHSNo_Quaternion_k : HSNo Quaternion_k
Known Quaternion_j_kQuaternion_j_k : mul_HSNo Quaternion_j Quaternion_k = Complex_i
Theorem Octonion_i2_i4Octonion_i2_i4 : mul_OSNo Quaternion_j Quaternion_k = Complex_i (proof)
Known Quaternion_k_jQuaternion_k_j : mul_HSNo Quaternion_k Quaternion_j = minus_HSNo Complex_i
Theorem Octonion_i4_i2Octonion_i4_i2 : mul_OSNo Quaternion_k Quaternion_j = minus_OSNo Complex_i (proof)
Known Quaternion_k_iQuaternion_k_i : mul_HSNo Quaternion_k Complex_i = Quaternion_j
Theorem Octonion_i4_i1Octonion_i4_i1 : mul_OSNo Quaternion_k Complex_i = Quaternion_j (proof)
Known Quaternion_i_kQuaternion_i_k : mul_HSNo Complex_i Quaternion_k = minus_HSNo Quaternion_j
Theorem Octonion_i1_i4Octonion_i1_i4 : mul_OSNo Complex_i Quaternion_k = minus_OSNo Quaternion_j (proof)
Param Octonion_i3Octonion_i3 : ι
Param Octonion_i5Octonion_i5 : ι
Known OSNo_p0_i5OSNo_p0_i5 : OSNo_proj0 Octonion_i5 = 0
Known OSNo_p0_i3OSNo_p0_i3 : OSNo_proj0 Octonion_i3 = 0
Known OSNo_p1_i3OSNo_p1_i3 : OSNo_proj1 Octonion_i3 = minus_HSNo Complex_i
Known HSNo_minus_HSNoHSNo_minus_HSNo : ∀ x0 . HSNo x0HSNo (minus_HSNo x0)
Known OSNo_p1_i5OSNo_p1_i5 : OSNo_proj1 Octonion_i5 = minus_HSNo Quaternion_k
Known minus_mul_HSNo_distrLminus_mul_HSNo_distrL : ∀ x0 x1 . HSNo x0HSNo x1mul_HSNo (minus_HSNo x0) x1 = minus_HSNo (mul_HSNo x0 x1)
Known OSNo_Octonion_i5OSNo_Octonion_i5 : OSNo Octonion_i5
Known OSNo_Octonion_i3OSNo_Octonion_i3 : OSNo Octonion_i3
Theorem Octonion_i2_i3Octonion_i2_i3 : mul_OSNo Quaternion_j Octonion_i3 = Octonion_i5 (proof)
Known conj_HSNo_jconj_HSNo_j : conj_HSNo Quaternion_j = minus_HSNo Quaternion_j
Known minus_mul_HSNo_distrRminus_mul_HSNo_distrR : ∀ x0 x1 . HSNo x0HSNo x1mul_HSNo x0 (minus_HSNo x1) = minus_HSNo (mul_HSNo x0 x1)
Known minus_HSNo_involminus_HSNo_invol : ∀ x0 . HSNo x0minus_HSNo (minus_HSNo x0) = x0
Theorem Octonion_i3_i2Octonion_i3_i2 : mul_OSNo Octonion_i3 Quaternion_j = minus_OSNo Octonion_i5 (proof)
Known conj_minus_HSNoconj_minus_HSNo : ∀ x0 . HSNo x0conj_HSNo (minus_HSNo x0) = minus_HSNo (conj_HSNo x0)
Known conj_HSNo_kconj_HSNo_k : conj_HSNo Quaternion_k = minus_HSNo Quaternion_k
Theorem Octonion_i3_i5Octonion_i3_i5 : mul_OSNo Octonion_i3 Octonion_i5 = Quaternion_j (proof)
Known conj_HSNo_iconj_HSNo_i : conj_HSNo Complex_i = minus_HSNo Complex_i
Theorem Octonion_i5_i3Octonion_i5_i3 : mul_OSNo Octonion_i5 Octonion_i3 = minus_OSNo Quaternion_j (proof)
Theorem Octonion_i5_i2Octonion_i5_i2 : mul_OSNo Octonion_i5 Quaternion_j = Octonion_i3 (proof)
Theorem Octonion_i2_i5Octonion_i2_i5 : mul_OSNo Quaternion_j Octonion_i5 = minus_OSNo Octonion_i3 (proof)
Param Octonion_i6Octonion_i6 : ι
Known OSNo_p0_i6OSNo_p0_i6 : OSNo_proj0 Octonion_i6 = 0
Known OSNo_p1_i6OSNo_p1_i6 : OSNo_proj1 Octonion_i6 = minus_HSNo Quaternion_j
Known OSNo_Octonion_i6OSNo_Octonion_i6 : OSNo Octonion_i6
Theorem Octonion_i3_i4Octonion_i3_i4 : mul_OSNo Octonion_i3 Quaternion_k = Octonion_i6 (proof)
Theorem Octonion_i4_i3Octonion_i4_i3 : mul_OSNo Quaternion_k Octonion_i3 = minus_OSNo Octonion_i6 (proof)
Theorem Octonion_i4_i6Octonion_i4_i6 : mul_OSNo Quaternion_k Octonion_i6 = Octonion_i3 (proof)
Theorem Octonion_i6_i4Octonion_i6_i4 : mul_OSNo Octonion_i6 Quaternion_k = minus_OSNo Octonion_i3 (proof)
Theorem Octonion_i6_i3Octonion_i6_i3 : mul_OSNo Octonion_i6 Octonion_i3 = Quaternion_k (proof)
Theorem Octonion_i3_i6Octonion_i3_i6 : mul_OSNo Octonion_i3 Octonion_i6 = minus_OSNo Quaternion_k (proof)
Param Octonion_i0Octonion_i0 : ι
Known OSNo_p0_i0OSNo_p0_i0 : OSNo_proj0 Octonion_i0 = 0
Param ordsuccordsucc : ιι
Known OSNo_p1_i0OSNo_p1_i0 : OSNo_proj1 Octonion_i0 = 1
Known Quaternion_k_sqrQuaternion_k_sqr : mul_HSNo Quaternion_k Quaternion_k = minus_HSNo 1
Known HSNo_1HSNo_1 : HSNo 1
Known OSNo_Octonion_i0OSNo_Octonion_i0 : OSNo Octonion_i0
Theorem Octonion_i4_i5Octonion_i4_i5 : mul_OSNo Quaternion_k Octonion_i5 = Octonion_i0 (proof)
Theorem Octonion_i5_i4Octonion_i5_i4 : mul_OSNo Octonion_i5 Quaternion_k = minus_OSNo Octonion_i0 (proof)
Known SNo_1SNo_1 : SNo 1
Known mul_HSNo_1Lmul_HSNo_1L : ∀ x0 . HSNo x0mul_HSNo 1 x0 = x0
Theorem Octonion_i5_i0Octonion_i5_i0 : mul_OSNo Octonion_i5 Octonion_i0 = Quaternion_k (proof)
Known mul_HSNo_1Rmul_HSNo_1R : ∀ x0 . HSNo x0mul_HSNo x0 1 = x0
Theorem Octonion_i0_i5Octonion_i0_i5 : mul_OSNo Octonion_i0 Octonion_i5 = minus_OSNo Quaternion_k (proof)
Theorem Octonion_i0_i4Octonion_i0_i4 : mul_OSNo Octonion_i0 Quaternion_k = Octonion_i5 (proof)
Theorem Octonion_i4_i0Octonion_i4_i0 : mul_OSNo Quaternion_k Octonion_i0 = minus_OSNo Octonion_i5 (proof)
Theorem Octonion_i5_i6Octonion_i5_i6 : mul_OSNo Octonion_i5 Octonion_i6 = Complex_i (proof)
Theorem Octonion_i6_i5Octonion_i6_i5 : mul_OSNo Octonion_i6 Octonion_i5 = minus_OSNo Complex_i (proof)
Theorem Octonion_i6_i1Octonion_i6_i1 : mul_OSNo Octonion_i6 Complex_i = Octonion_i5 (proof)
Theorem Octonion_i1_i6Octonion_i1_i6 : mul_OSNo Complex_i Octonion_i6 = minus_OSNo Octonion_i5 (proof)
Theorem Octonion_i1_i5Octonion_i1_i5 : mul_OSNo Complex_i Octonion_i5 = Octonion_i6 (proof)
Theorem Octonion_i5_i1Octonion_i5_i1 : mul_OSNo Octonion_i5 Complex_i = minus_OSNo Octonion_i6 (proof)
Theorem Octonion_i6_i0Octonion_i6_i0 : mul_OSNo Octonion_i6 Octonion_i0 = Quaternion_j (proof)
Theorem Octonion_i0_i6Octonion_i0_i6 : mul_OSNo Octonion_i0 Octonion_i6 = minus_OSNo Quaternion_j (proof)
Theorem Octonion_i0_i2Octonion_i0_i2 : mul_OSNo Octonion_i0 Quaternion_j = Octonion_i6 (proof)
Theorem Octonion_i2_i0Octonion_i2_i0 : mul_OSNo Quaternion_j Octonion_i0 = minus_OSNo Octonion_i6 (proof)
Known Quaternion_j_sqrQuaternion_j_sqr : mul_HSNo Quaternion_j Quaternion_j = minus_HSNo 1
Theorem Octonion_i2_i6Octonion_i2_i6 : mul_OSNo Quaternion_j Octonion_i6 = Octonion_i0 (proof)
Theorem Octonion_i6_i2Octonion_i6_i2 : mul_OSNo Octonion_i6 Quaternion_j = minus_OSNo Octonion_i0 (proof)
Theorem Octonion_i0_i1Octonion_i0_i1 : mul_OSNo Octonion_i0 Complex_i = Octonion_i3 (proof)
Theorem Octonion_i1_i0Octonion_i1_i0 : mul_OSNo Complex_i Octonion_i0 = minus_OSNo Octonion_i3 (proof)
Known Quaternion_i_sqrQuaternion_i_sqr : mul_HSNo Complex_i Complex_i = minus_HSNo 1
Theorem Octonion_i1_i3Octonion_i1_i3 : mul_OSNo Complex_i Octonion_i3 = Octonion_i0 (proof)
Theorem Octonion_i3_i1Octonion_i3_i1 : mul_OSNo Octonion_i3 Complex_i = minus_OSNo Octonion_i0 (proof)
Theorem Octonion_i3_i0Octonion_i3_i0 : mul_OSNo Octonion_i3 Octonion_i0 = Complex_i (proof)
Theorem Octonion_i0_i3Octonion_i0_i3 : mul_OSNo Octonion_i0 Octonion_i3 = minus_OSNo Complex_i (proof)