Proofgold Asset

Param HSNo^HSNo : ι → ο
Param nIn^nIn : ι → ι → ο
Param Sing^Sing : ι → ι
Param ordsucc^ordsucc : ι → ι
Param nat_p^nat_p : ι → ο
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param ordinal^ordinal : ι → ο
Param and^and : ο → ο → ο
Definition ExtendedSNoElt_^{ExtendedSNoElt_} := λ x0 x1 . ∀ x2 . x2 ∈ prim3 x1 ⟶ or (ordinal x2) (∃ x3 . and (x3 ∈ x0) (x2 = Sing x3))
Known Sing_nat_fresh_extension^{Sing_nat_fresh_extension} : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 . ExtendedSNoElt_ x0 x1 ⟶ ∀ x2 . x2 ∈ x1 ⟶ nIn (Sing x0) x2
Known nat_4^nat_4 : nat_p 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known HSNo_ExtendedSNoElt_4^{HSNo_ExtendedSNoElt_4} : ∀ x0 . HSNo x0 ⟶ ExtendedSNoElt_ 4 x0
Theorem octonion_tag_fresh^{octonion_tag_fresh} : ∀ x0 . HSNo x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nIn (Sing 4) x1
Param binunion^binunion : ι → ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Definition pair_tag^pair_tag := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 x0|x3 ∈ x2}
Definition HSNo_pair^HSNo_pair := pair_tag (Sing 4)
Known pair_tag_0^pair_tag_0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . pair_tag x0 x2 0 = x2
Theorem HSNo_pair_0^HSNo_pair_0 : ∀ x0 . HSNo_pair x0 0 = x0
Known pair_tag_prop_1^{pair_tag_prop_1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x2 ⟶ x1 x4 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x2 = x4
Theorem HSNo_pair_prop_1^{HSNo_pair_prop_1} : ∀ x0 x1 x2 x3 . HSNo x0 ⟶ HSNo x2 ⟶ HSNo_pair x0 x1 = HSNo_pair x2 x3 ⟶ x0 = x2
Known pair_tag_prop_2^{pair_tag_prop_2} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x3 = x5
Theorem HSNo_pair_prop_2^{HSNo_pair_prop_2} : ∀ x0 x1 x2 x3 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ HSNo x3 ⟶ HSNo_pair x0 x1 = HSNo_pair x2 x3 ⟶ x1 = x3
Param CD_carr^CD_carr : ι → (ι → ο) → ι → ο
Definition OSNo^OSNo := CD_carr (Sing 4) HSNo
Known CD_carr_I^CD_carr_I : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_carr x0 x1 (pair_tag x0 x2 x3)
Theorem OSNo_I^OSNo_I : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo (HSNo_pair x0 x1)
Known CD_carr_E^CD_carr_E : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x2 = pair_tag x0 x4 x5 ⟶ x3 (pair_tag x0 x4 x5)) ⟶ x3 x2
Theorem OSNo_E^OSNo_E : ∀ x0 . OSNo x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . HSNo x2 ⟶ HSNo x3 ⟶ x0 = HSNo_pair x2 x3 ⟶ x1 (HSNo_pair x2 x3)) ⟶ x1 x0
Known CD_carr_0ext^CD_carr_0ext : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_carr x0 x1 x2
Known HSNo_0^HSNo_0 : HSNo 0
Theorem HSNo_OSNo^HSNo_OSNo : ∀ x0 . HSNo x0 ⟶ OSNo x0
Theorem OSNo_0^OSNo_0 : OSNo 0
Known HSNo_1^HSNo_1 : HSNo 1
Theorem OSNo_1^OSNo_1 : OSNo 1
Known UnionE_impred^{UnionE_impred} : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2) ⟶ x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Param Subq^Subq : ι → ι → ο
Known extension_SNoElt_mon^{extension_SNoElt_mon} : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 . ExtendedSNoElt_ x0 x2 ⟶ ExtendedSNoElt_ x1 x2
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known In_4_5^In_4_5 : 4 ∈ 5
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Theorem OSNo_ExtendedSNoElt_5^{OSNo_ExtendedSNoElt_5} : ∀ x0 . OSNo x0 ⟶ ExtendedSNoElt_ 5 x0
Param CD_proj0^CD_proj0 : ι → (ι → ο) → ι → ι
Definition OSNo_proj0^OSNo_proj0 := CD_proj0 (Sing 4) HSNo
Param CD_proj1^CD_proj1 : ι → (ι → ο) → ι → ι
Definition OSNo_proj1^OSNo_proj1 := CD_proj1 (Sing 4) HSNo
Known CD_proj0_1^CD_proj0_1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ and (x1 (CD_proj0 x0 x1 x2)) (∃ x3 . and (x1 x3) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) x3))
Theorem OSNo_proj0_1^OSNo_proj0_1 : ∀ x0 . OSNo x0 ⟶ and (HSNo (OSNo_proj0 x0)) (∃ x1 . and (HSNo x1) (x0 = HSNo_pair (OSNo_proj0 x0) x1))
Known CD_proj0_2^CD_proj0_2 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_proj0 x0 x1 (pair_tag x0 x2 x3) = x2
Theorem OSNo_proj0_2^OSNo_proj0_2 : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo_proj0 (HSNo_pair x0 x1) = x0
Known CD_proj1_1^CD_proj1_1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ and (x1 (CD_proj1 x0 x1 x2)) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) (CD_proj1 x0 x1 x2))
Theorem OSNo_proj1_1^OSNo_proj1_1 : ∀ x0 . OSNo x0 ⟶ and (HSNo (OSNo_proj1 x0)) (x0 = HSNo_pair (OSNo_proj0 x0) (OSNo_proj1 x0))
Known CD_proj1_2^CD_proj1_2 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_proj1 x0 x1 (pair_tag x0 x2 x3) = x3
Theorem OSNo_proj1_2^OSNo_proj1_2 : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo_proj1 (HSNo_pair x0 x1) = x1
Known CD_proj0R^CD_proj0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x1 (CD_proj0 x0 x1 x2)
Theorem OSNo_proj0R^OSNo_proj0R : ∀ x0 . OSNo x0 ⟶ HSNo (OSNo_proj0 x0)
Known CD_proj1R^CD_proj1R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x1 (CD_proj1 x0 x1 x2)
Theorem OSNo_proj1R^OSNo_proj1R : ∀ x0 . OSNo x0 ⟶ HSNo (OSNo_proj1 x0)
Known CD_proj0proj1_eta^{CD_proj0proj1_eta} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x2 = pair_tag x0 (CD_proj0 x0 x1 x2) (CD_proj1 x0 x1 x2)
Theorem OSNo_proj0p1^OSNo_proj0p1 : ∀ x0 . OSNo x0 ⟶ x0 = HSNo_pair (OSNo_proj0 x0) (OSNo_proj1 x0)
Known CD_proj0proj1_split^{CD_proj0proj1_split} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . CD_carr x0 x1 x2 ⟶ CD_carr x0 x1 x3 ⟶ CD_proj0 x0 x1 x2 = CD_proj0 x0 x1 x3 ⟶ CD_proj1 x0 x1 x2 = CD_proj1 x0 x1 x3 ⟶ x2 = x3
Theorem 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
Param HSNoLev^HSNoLev : ι → ι
Definition OSNoLev^OSNoLev := λ x0 . binunion (HSNoLev (OSNo_proj0 x0)) (HSNoLev (OSNo_proj1 x0))
Known ordinal_binunion^{ordinal_binunion} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binunion x0 x1)
Known HSNoLev_ordinal^{HSNoLev_ordinal} : ∀ x0 . HSNo x0 ⟶ ordinal (HSNoLev x0)
Theorem OSNoLev_ordinal^{OSNoLev_ordinal} : ∀ x0 . OSNo x0 ⟶ ordinal (OSNoLev x0)
Param CD_minus^CD_minus : ι → (ι → ο) → (ι → ι) → ι → ι
Param minus_HSNo^minus_HSNo : ι → ι
Definition minus_OSNo^minus_OSNo := CD_minus (Sing 4) HSNo minus_HSNo
Param CD_conj^CD_conj : ι → (ι → ο) → (ι → ι) → (ι → ι) → ι → ι
Param conj_HSNo^conj_HSNo : ι → ι
Definition conj_OSNo^conj_OSNo := CD_conj (Sing 4) HSNo minus_HSNo conj_HSNo
Param CD_add^CD_add : ι → (ι → ο) → (ι → ι → ι) → ι → ι → ι
Param add_HSNo^add_HSNo : ι → ι → ι
Definition add_OSNo^add_OSNo := CD_add (Sing 4) HSNo add_HSNo
Param CD_mul^CD_mul : ι → (ι → ο) → (ι → ι) → (ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Param mul_HSNo^mul_HSNo : ι → ι → ι
Definition mul_OSNo^mul_OSNo := CD_mul (Sing 4) HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo
Param CD_exp_nat^CD_exp_nat : ι → (ι → ο) → (ι → ι) → (ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Definition exp_OSNo_nat^exp_OSNo_nat := CD_exp_nat (Sing 4) HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo
Known CD_minus_CD^CD_minus_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 (CD_minus x0 x1 x2 x3)
Known HSNo_minus_HSNo^{HSNo_minus_HSNo} : ∀ x0 . HSNo x0 ⟶ HSNo (minus_HSNo x0)
Theorem OSNo_minus_OSNo^{OSNo_minus_OSNo} : ∀ x0 . OSNo x0 ⟶ OSNo (minus_OSNo x0)
Known CD_minus_proj0^{CD_minus_proj0} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_proj0 x0 x1 (CD_minus x0 x1 x2 x3) = x2 (CD_proj0 x0 x1 x3)
Theorem minus_OSNo_proj0^{minus_OSNo_proj0} : ∀ x0 . OSNo x0 ⟶ OSNo_proj0 (minus_OSNo x0) = minus_HSNo (OSNo_proj0 x0)
Known CD_minus_proj1^{CD_minus_proj1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_proj1 x0 x1 (CD_minus x0 x1 x2 x3) = x2 (CD_proj1 x0 x1 x3)
Theorem minus_OSNo_proj1^{minus_OSNo_proj1} : ∀ x0 . OSNo x0 ⟶ OSNo_proj1 (minus_OSNo x0) = minus_HSNo (OSNo_proj1 x0)
Known CD_conj_CD^CD_conj_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 (CD_conj x0 x1 x2 x3 x4)
Known HSNo_conj_HSNo^{HSNo_conj_HSNo} : ∀ x0 . HSNo x0 ⟶ HSNo (conj_HSNo x0)
Theorem OSNo_conj_OSNo^{OSNo_conj_OSNo} : ∀ x0 . OSNo x0 ⟶ OSNo (conj_OSNo x0)
Known CD_conj_proj0^{CD_conj_proj0} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_proj0 x0 x1 (CD_conj x0 x1 x2 x3 x4) = x3 (CD_proj0 x0 x1 x4)
Theorem conj_OSNo_proj0^{conj_OSNo_proj0} : ∀ x0 . OSNo x0 ⟶ OSNo_proj0 (conj_OSNo x0) = conj_HSNo (OSNo_proj0 x0)
Known CD_conj_proj1^{CD_conj_proj1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_proj1 x0 x1 (CD_conj x0 x1 x2 x3 x4) = x2 (CD_proj1 x0 x1 x4)
Theorem conj_OSNo_proj1^{conj_OSNo_proj1} : ∀ x0 . OSNo x0 ⟶ OSNo_proj1 (conj_OSNo x0) = minus_HSNo (OSNo_proj1 x0)
Known CD_add_CD^CD_add_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 (CD_add x0 x1 x2 x3 x4)
Known HSNo_add_HSNo^{HSNo_add_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo (add_HSNo x0 x1)
Theorem OSNo_add_OSNo^{OSNo_add_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo (add_OSNo x0 x1)
Known CD_add_proj0^CD_add_proj0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_proj0 x0 x1 (CD_add x0 x1 x2 x3 x4) = x2 (CD_proj0 x0 x1 x3) (CD_proj0 x0 x1 x4)
Theorem add_OSNo_proj0^{add_OSNo_proj0} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj0 (add_OSNo x0 x1) = add_HSNo (OSNo_proj0 x0) (OSNo_proj0 x1)
Known CD_add_proj1^CD_add_proj1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_proj1 x0 x1 (CD_add x0 x1 x2 x3 x4) = x2 (CD_proj1 x0 x1 x3) (CD_proj1 x0 x1 x4)
Theorem add_OSNo_proj1^{add_OSNo_proj1} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj1 (add_OSNo x0 x1) = add_HSNo (OSNo_proj1 x0) (OSNo_proj1 x1)
Known CD_mul_CD^CD_mul_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7)
Known HSNo_mul_HSNo^{HSNo_mul_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo (mul_HSNo x0 x1)
Theorem OSNo_mul_OSNo^{OSNo_mul_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo (mul_OSNo x0 x1)
Known CD_mul_proj0^CD_mul_proj0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_proj0 x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = x4 (x5 (CD_proj0 x0 x1 x6) (CD_proj0 x0 x1 x7)) (x2 (x5 (x3 (CD_proj1 x0 x1 x7)) (CD_proj1 x0 x1 x6)))
Theorem 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 CD_mul_proj1^CD_mul_proj1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_proj1 x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = x4 (x5 (CD_proj1 x0 x1 x7) (CD_proj0 x0 x1 x6)) (x5 (CD_proj1 x0 x1 x6) (x3 (CD_proj0 x0 x1 x7)))
Theorem 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 CD_proj0_F^CD_proj0_F : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_proj0 x0 x1 x2 = x2
Theorem HSNo_OSNo_proj0^{HSNo_OSNo_proj0} : ∀ x0 . HSNo x0 ⟶ OSNo_proj0 x0 = x0
Known CD_proj1_F^CD_proj1_F : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_proj1 x0 x1 x2 = 0
Theorem HSNo_OSNo_proj1^{HSNo_OSNo_proj1} : ∀ x0 . HSNo x0 ⟶ OSNo_proj1 x0 = 0
Theorem OSNo_p0_0^OSNo_p0_0 : OSNo_proj0 0 = 0
Theorem OSNo_p1_0^OSNo_p1_0 : OSNo_proj1 0 = 0
Theorem OSNo_p0_1^OSNo_p0_1 : OSNo_proj0 1 = 1
Theorem OSNo_p1_1^OSNo_p1_1 : OSNo_proj1 1 = 0
Param Complex_i^Complex_i : ι
Known HSNo_Complex_i^{HSNo_Complex_i} : HSNo Complex_i
Theorem OSNo_p0_i^OSNo_p0_i : OSNo_proj0 Complex_i = Complex_i
Theorem OSNo_p1_i^OSNo_p1_i : OSNo_proj1 Complex_i = 0
Param Quaternion_j^Quaternion_j : ι
Known HSNo_Quaternion_j^{HSNo_Quaternion_j} : HSNo Quaternion_j
Theorem OSNo_p0_j^OSNo_p0_j : OSNo_proj0 Quaternion_j = Quaternion_j
Theorem OSNo_p1_j^OSNo_p1_j : OSNo_proj1 Quaternion_j = 0
Param Quaternion_k^Quaternion_k : ι
Known HSNo_Quaternion_k^{HSNo_Quaternion_k} : HSNo Quaternion_k
Theorem OSNo_p0_k^OSNo_p0_k : OSNo_proj0 Quaternion_k = Quaternion_k
Theorem OSNo_p1_k^OSNo_p1_k : OSNo_proj1 Quaternion_k = 0
Known CD_minus_F_eq^{CD_minus_F_eq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ ∀ x3 . x1 x3 ⟶ CD_minus x0 x1 x2 x3 = x2 x3
Known minus_HSNo_0^minus_HSNo_0 : minus_HSNo 0 = 0
Theorem minus_OSNo_minus_HSNo^{minus_OSNo_minus_HSNo} : ∀ x0 . HSNo x0 ⟶ minus_OSNo x0 = minus_HSNo x0
Theorem minus_OSNo_0^minus_OSNo_0 : minus_OSNo 0 = 0
Known CD_conj_F_eq^CD_conj_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ ∀ x3 : ι → ι . ∀ x4 . x1 x4 ⟶ CD_conj x0 x1 x2 x3 x4 = x3 x4
Theorem conj_OSNo_conj_HSNo^{conj_OSNo_conj_HSNo} : ∀ x0 . HSNo x0 ⟶ conj_OSNo x0 = conj_HSNo x0
Known conj_HSNo_0^conj_HSNo_0 : conj_HSNo 0 = 0
Theorem conj_OSNo_0^conj_OSNo_0 : conj_OSNo 0 = 0
Known conj_HSNo_1^conj_HSNo_1 : conj_HSNo 1 = 1
Theorem conj_OSNo_1^conj_OSNo_1 : conj_OSNo 1 = 1
Known CD_add_F_eq^CD_add_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ x2 0 0 = 0 ⟶ ∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ CD_add x0 x1 x2 x3 x4 = x2 x3 x4
Known add_HSNo_0L^add_HSNo_0L : ∀ x0 . HSNo x0 ⟶ add_HSNo 0 x0 = x0
Theorem add_OSNo_add_HSNo^{add_OSNo_add_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ add_OSNo x0 x1 = add_HSNo x0 x1
Known CD_mul_F_eq^CD_mul_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ x2 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 x7 = x5 x6 x7
Known add_HSNo_0R^add_HSNo_0R : ∀ x0 . HSNo x0 ⟶ add_HSNo x0 0 = x0
Known mul_HSNo_0L^mul_HSNo_0L : ∀ x0 . HSNo x0 ⟶ mul_HSNo 0 x0 = 0
Known mul_HSNo_0R^mul_HSNo_0R : ∀ x0 . HSNo x0 ⟶ mul_HSNo x0 0 = 0
Theorem mul_OSNo_mul_HSNo^{mul_OSNo_mul_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ mul_OSNo x0 x1 = mul_HSNo x0 x1
Known CD_minus_invol^{CD_minus_invol} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x2 x3) = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_minus x0 x1 x2 (CD_minus x0 x1 x2 x3) = x3
Known minus_HSNo_invol^{minus_HSNo_invol} : ∀ x0 . HSNo x0 ⟶ minus_HSNo (minus_HSNo x0) = x0
Theorem minus_OSNo_invol^{minus_OSNo_invol} : ∀ x0 . OSNo x0 ⟶ minus_OSNo (minus_OSNo x0) = x0
Known CD_conj_invol^{CD_conj_invol} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x2 (x2 x4) = x4) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x3 x4) = x4) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_conj x0 x1 x2 x3 (CD_conj x0 x1 x2 x3 x4) = x4
Known conj_HSNo_invol^{conj_HSNo_invol} : ∀ x0 . HSNo x0 ⟶ conj_HSNo (conj_HSNo x0) = x0
Theorem conj_OSNo_invol^{conj_OSNo_invol} : ∀ x0 . OSNo x0 ⟶ conj_OSNo (conj_OSNo x0) = x0
Known CD_conj_minus^{CD_conj_minus} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x2 x4) = x2 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_conj x0 x1 x2 x3 (CD_minus x0 x1 x2 x4) = CD_minus x0 x1 x2 (CD_conj x0 x1 x2 x3 x4)
Known conj_minus_HSNo^{conj_minus_HSNo} : ∀ x0 . HSNo x0 ⟶ conj_HSNo (minus_HSNo x0) = minus_HSNo (conj_HSNo x0)
Theorem conj_minus_OSNo^{conj_minus_OSNo} : ∀ x0 . OSNo x0 ⟶ conj_OSNo (minus_OSNo x0) = minus_OSNo (conj_OSNo x0)
Known CD_minus_add^CD_minus_add : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x1 (x3 x4 x5)) ⟶ (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x2 (x3 x4 x5) = x3 (x2 x4) (x2 x5)) ⟶ ∀ x4 x5 . CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 x5 ⟶ CD_minus x0 x1 x2 (CD_add x0 x1 x3 x4 x5) = CD_add x0 x1 x3 (CD_minus x0 x1 x2 x4) (CD_minus x0 x1 x2 x5)
Known minus_add_HSNo^{minus_add_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ minus_HSNo (add_HSNo x0 x1) = add_HSNo (minus_HSNo x0) (minus_HSNo x1)
Theorem minus_add_OSNo^{minus_add_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ minus_OSNo (add_OSNo x0 x1) = add_OSNo (minus_OSNo x0) (minus_OSNo x1)
Known CD_conj_add^CD_conj_add : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 : ι → ι → ι . (∀ x5 . x1 x5 ⟶ x1 (x2 x5)) ⟶ (∀ x5 . x1 x5 ⟶ x1 (x3 x5)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x1 (x4 x5 x6)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x2 (x4 x5 x6) = x4 (x2 x5) (x2 x6)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x3 (x4 x5 x6) = x4 (x3 x5) (x3 x6)) ⟶ ∀ x5 x6 . CD_carr x0 x1 x5 ⟶ CD_carr x0 x1 x6 ⟶ CD_conj x0 x1 x2 x3 (CD_add x0 x1 x4 x5 x6) = CD_add x0 x1 x4 (CD_conj x0 x1 x2 x3 x5) (CD_conj x0 x1 x2 x3 x6)
Known conj_add_HSNo^{conj_add_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ conj_HSNo (add_HSNo x0 x1) = add_HSNo (conj_HSNo x0) (conj_HSNo x1)
Theorem conj_add_OSNo^{conj_add_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ conj_OSNo (add_OSNo x0 x1) = add_OSNo (conj_OSNo x0) (conj_OSNo x1)
Known CD_add_com^CD_add_com : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x2 x3 x4 = x2 x4 x3) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x2 x3 x4 = CD_add x0 x1 x2 x4 x3
Known add_HSNo_com^add_HSNo_com : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ add_HSNo x0 x1 = add_HSNo x1 x0
Theorem add_OSNo_com^add_OSNo_com : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ add_OSNo x0 x1 = add_OSNo x1 x0
Known CD_add_assoc^CD_add_assoc : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ (∀ x3 x4 x5 . x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)) ⟶ ∀ x3 x4 x5 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 x5 ⟶ CD_add x0 x1 x2 (CD_add x0 x1 x2 x3 x4) x5 = CD_add x0 x1 x2 x3 (CD_add x0 x1 x2 x4 x5)
Known add_HSNo_assoc^{add_HSNo_assoc} : ∀ x0 x1 x2 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ add_HSNo (add_HSNo x0 x1) x2 = add_HSNo x0 (add_HSNo x1 x2)
Theorem add_OSNo_assoc^{add_OSNo_assoc} : ∀ x0 x1 x2 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo x2 ⟶ add_OSNo (add_OSNo x0 x1) x2 = add_OSNo x0 (add_OSNo x1 x2)
Known CD_add_0L^CD_add_0L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ (∀ x3 . x1 x3 ⟶ x2 0 x3 = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_add x0 x1 x2 0 x3 = x3
Theorem add_OSNo_0L^add_OSNo_0L : ∀ x0 . OSNo x0 ⟶ add_OSNo 0 x0 = x0
Known CD_add_0R^CD_add_0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ (∀ x3 . x1 x3 ⟶ x2 x3 0 = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_add x0 x1 x2 x3 0 = x3
Theorem add_OSNo_0R^add_OSNo_0R : ∀ x0 . OSNo x0 ⟶ add_OSNo x0 0 = x0
Known CD_add_minus_linv^{CD_add_minus_linv} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x2 x4) x4 = 0) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x3 (CD_minus x0 x1 x2 x4) x4 = 0
Known add_HSNo_minus_HSNo_linv^{add_HSNo_minus_HSNo_linv} : ∀ x0 . HSNo x0 ⟶ add_HSNo (minus_HSNo x0) x0 = 0
Theorem add_OSNo_minus_OSNo_linv^{add_OSNo_minus_OSNo_linv} : ∀ x0 . OSNo x0 ⟶ add_OSNo (minus_OSNo x0) x0 = 0
Known CD_add_minus_rinv^{CD_add_minus_rinv} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 x4 (x2 x4) = 0) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x3 x4 (CD_minus x0 x1 x2 x4) = 0
Known add_HSNo_minus_HSNo_rinv^{add_HSNo_minus_HSNo_rinv} : ∀ x0 . HSNo x0 ⟶ add_HSNo x0 (minus_HSNo x0) = 0
Theorem add_OSNo_minus_OSNo_rinv^{add_OSNo_minus_OSNo_rinv} : ∀ x0 . OSNo x0 ⟶ add_OSNo x0 (minus_OSNo x0) = 0
Known CD_mul_0R^CD_mul_0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x4 0 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 0 = 0
Theorem mul_OSNo_0R^mul_OSNo_0R : ∀ x0 . OSNo x0 ⟶ mul_OSNo x0 0 = 0
Known CD_mul_0L^CD_mul_0L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ x2 0 = 0 ⟶ x4 0 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 0 x6 = 0
Theorem mul_OSNo_0L^mul_OSNo_0L : ∀ x0 . OSNo x0 ⟶ mul_OSNo 0 x0 = 0
Known CD_mul_1R^CD_mul_1R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x3 1 = 1 ⟶ (∀ x6 . x1 x6 ⟶ x4 0 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 1 = x6
Known mul_HSNo_1R^mul_HSNo_1R : ∀ x0 . HSNo x0 ⟶ mul_HSNo x0 1 = x0
Theorem mul_OSNo_1R^mul_OSNo_1R : ∀ x0 . OSNo x0 ⟶ mul_OSNo x0 1 = x0
Known CD_mul_1L^CD_mul_1L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ x2 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 1 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 1 x6 = x6
Known mul_HSNo_1L^mul_HSNo_1L : ∀ x0 . HSNo x0 ⟶ mul_HSNo 1 x0 = x0
Theorem mul_OSNo_1L^mul_OSNo_1L : ∀ x0 . OSNo x0 ⟶ mul_OSNo 1 x0 = x0
Known CD_conj_mul^CD_conj_mul : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 . x1 x6 ⟶ x2 (x2 x6) = x6) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x3 x6) = x6) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x2 x6) = x2 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x4 x6 x7) = x4 (x3 x6) (x3 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x5 x6 x7) = x5 (x3 x7) (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_conj x0 x1 x2 x3 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = CD_mul x0 x1 x2 x3 x4 x5 (CD_conj x0 x1 x2 x3 x7) (CD_conj x0 x1 x2 x3 x6)
Known conj_mul_HSNo^{conj_mul_HSNo} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ conj_HSNo (mul_HSNo x0 x1) = mul_HSNo (conj_HSNo x1) (conj_HSNo x0)
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_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)
Theorem conj_mul_OSNo^{conj_mul_OSNo} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ conj_OSNo (mul_OSNo x0 x1) = mul_OSNo (conj_OSNo x1) (conj_OSNo x0)
Known CD_add_mul_distrL^{CD_add_mul_distrL} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x4 x6 x7) = x4 (x3 x6) (x3 x7)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x4 (x4 x6 x7) x8 = x4 x6 (x4 x7 x8)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 x6 (x4 x7 x8) = x4 (x5 x6 x7) (x5 x6 x8)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 (x4 x6 x7) x8 = x4 (x5 x6 x8) (x5 x7 x8)) ⟶ ∀ x6 x7 x8 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 x8 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_add x0 x1 x4 x7 x8) = CD_add x0 x1 x4 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) (CD_mul x0 x1 x2 x3 x4 x5 x6 x8)
Known mul_HSNo_distrL^{mul_HSNo_distrL} : ∀ x0 x1 x2 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ mul_HSNo x0 (add_HSNo x1 x2) = add_HSNo (mul_HSNo x0 x1) (mul_HSNo x0 x2)
Known mul_HSNo_distrR^{mul_HSNo_distrR} : ∀ x0 x1 x2 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ mul_HSNo (add_HSNo x0 x1) x2 = add_HSNo (mul_HSNo x0 x2) (mul_HSNo x1 x2)
Theorem mul_OSNo_distrL^{mul_OSNo_distrL} : ∀ x0 x1 x2 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo x2 ⟶ mul_OSNo x0 (add_OSNo x1 x2) = add_OSNo (mul_OSNo x0 x1) (mul_OSNo x0 x2)
Known CD_add_mul_distrR^{CD_add_mul_distrR} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x4 (x4 x6 x7) x8 = x4 x6 (x4 x7 x8)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 x6 (x4 x7 x8) = x4 (x5 x6 x7) (x5 x6 x8)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 (x4 x6 x7) x8 = x4 (x5 x6 x8) (x5 x7 x8)) ⟶ ∀ x6 x7 x8 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 x8 ⟶ CD_mul x0 x1 x2 x3 x4 x5 (CD_add x0 x1 x4 x6 x7) x8 = CD_add x0 x1 x4 (CD_mul x0 x1 x2 x3 x4 x5 x6 x8) (CD_mul x0 x1 x2 x3 x4 x5 x7 x8)
Theorem mul_OSNo_distrR^{mul_OSNo_distrR} : ∀ x0 x1 x2 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo x2 ⟶ mul_OSNo (add_OSNo x0 x1) x2 = add_OSNo (mul_OSNo x0 x2) (mul_OSNo x1 x2)
Known CD_minus_mul_distrR^{CD_minus_mul_distrR} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x2 x6) = x2 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_minus x0 x1 x2 x7) = CD_minus x0 x1 x2 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7)
Theorem minus_mul_OSNo_distrR^{minus_mul_OSNo_distrR} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ mul_OSNo x0 (minus_OSNo x1) = minus_OSNo (mul_OSNo x0 x1)
Known CD_minus_mul_distrL^{CD_minus_mul_distrL} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 (CD_minus x0 x1 x2 x6) x7 = CD_minus x0 x1 x2 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7)
Theorem minus_mul_OSNo_distrL^{minus_mul_OSNo_distrL} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ mul_OSNo (minus_OSNo x0) x1 = minus_OSNo (mul_OSNo x0 x1)
Known CD_exp_nat_0^CD_exp_nat_0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . ∀ x6 . CD_exp_nat x0 x1 x2 x3 x4 x5 x6 0 = 1
Theorem exp_OSNo_nat_0^{exp_OSNo_nat_0} : ∀ x0 . exp_OSNo_nat x0 0 = 1
Known CD_exp_nat_S^CD_exp_nat_S : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . ∀ x6 x7 . nat_p x7 ⟶ CD_exp_nat x0 x1 x2 x3 x4 x5 x6 (ordsucc x7) = CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_exp_nat x0 x1 x2 x3 x4 x5 x6 x7)
Theorem exp_OSNo_nat_S^{exp_OSNo_nat_S} : ∀ x0 x1 . nat_p x1 ⟶ exp_OSNo_nat x0 (ordsucc x1) = mul_OSNo x0 (exp_OSNo_nat x0 x1)
Known CD_exp_nat_1^CD_exp_nat_1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x3 1 = 1 ⟶ (∀ x6 . x1 x6 ⟶ x4 0 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_exp_nat x0 x1 x2 x3 x4 x5 x6 1 = x6
Theorem exp_OSNo_nat_1^{exp_OSNo_nat_1} : ∀ x0 . OSNo x0 ⟶ exp_OSNo_nat x0 1 = x0
Known CD_exp_nat_2^CD_exp_nat_2 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x3 1 = 1 ⟶ (∀ x6 . x1 x6 ⟶ x4 0 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_exp_nat x0 x1 x2 x3 x4 x5 x6 2 = CD_mul x0 x1 x2 x3 x4 x5 x6 x6
Theorem exp_OSNo_nat_2^{exp_OSNo_nat_2} : ∀ x0 . OSNo x0 ⟶ exp_OSNo_nat x0 2 = mul_OSNo x0 x0
Known CD_exp_nat_CD^{CD_exp_nat_CD} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ x1 0 ⟶ x1 1 ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ ∀ x7 . nat_p x7 ⟶ CD_carr x0 x1 (CD_exp_nat x0 x1 x2 x3 x4 x5 x6 x7)
Theorem OSNo_exp_OSNo_nat^{OSNo_exp_OSNo_nat} : ∀ x0 . OSNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ OSNo (exp_OSNo_nat x0 x1)
Theorem add_HSNo_com_3b_1_2^{add_HSNo_com_3b_1_2} : ∀ x0 x1 x2 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ add_HSNo (add_HSNo x0 x1) x2 = add_HSNo (add_HSNo x0 x2) x1
Theorem add_HSNo_com_4_inner_mid^{add_HSNo_com_4_inner_mid} : ∀ x0 x1 x2 x3 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ HSNo x3 ⟶ add_HSNo (add_HSNo x0 x1) (add_HSNo x2 x3) = add_HSNo (add_HSNo x0 x2) (add_HSNo x1 x3)
Theorem add_HSNo_rotate_4_0312^{add_HSNo_rotate_4_0312} : ∀ x0 x1 x2 x3 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo x2 ⟶ HSNo x3 ⟶ add_HSNo (add_HSNo x0 x1) (add_HSNo x2 x3) = add_HSNo (add_HSNo x0 x3) (add_HSNo x1 x2)
Definition Octonion_i0^Octonion_i0 := HSNo_pair 0 1
Definition Octonion_i3^Octonion_i3 := HSNo_pair 0 (minus_HSNo Complex_i)
Definition Octonion_i5^Octonion_i5 := HSNo_pair 0 (minus_HSNo Quaternion_k)
Definition Octonion_i6^Octonion_i6 := HSNo_pair 0 (minus_HSNo Quaternion_j)
Theorem OSNo_Complex_i^{OSNo_Complex_i} : OSNo Complex_i
Theorem OSNo_Quaternion_j^{OSNo_Quaternion_j} : OSNo Quaternion_j
Theorem OSNo_Quaternion_k^{OSNo_Quaternion_k} : OSNo Quaternion_k
Theorem OSNo_Octonion_i0^{OSNo_Octonion_i0} : OSNo Octonion_i0
Theorem OSNo_Octonion_i3^{OSNo_Octonion_i3} : OSNo Octonion_i3
Theorem OSNo_Octonion_i5^{OSNo_Octonion_i5} : OSNo Octonion_i5
Theorem OSNo_Octonion_i6^{OSNo_Octonion_i6} : OSNo Octonion_i6
Theorem OSNo_p0_i0^OSNo_p0_i0 : OSNo_proj0 Octonion_i0 = 0
Theorem OSNo_p1_i0^OSNo_p1_i0 : OSNo_proj1 Octonion_i0 = 1
Theorem OSNo_p0_i3^OSNo_p0_i3 : OSNo_proj0 Octonion_i3 = 0
Theorem OSNo_p1_i3^OSNo_p1_i3 : OSNo_proj1 Octonion_i3 = minus_HSNo Complex_i
Theorem OSNo_p0_i5^OSNo_p0_i5 : OSNo_proj0 Octonion_i5 = 0
Theorem OSNo_p1_i5^OSNo_p1_i5 : OSNo_proj1 Octonion_i5 = minus_HSNo Quaternion_k
Theorem OSNo_p0_i6^OSNo_p0_i6 : OSNo_proj0 Octonion_i6 = 0
Theorem OSNo_p1_i6^OSNo_p1_i6 : OSNo_proj1 Octonion_i6 = minus_HSNo Quaternion_j
Known Quaternion_i_sqr^{Quaternion_i_sqr} : mul_HSNo Complex_i Complex_i = minus_HSNo 1
Theorem Octonion_i1_sqr^{Octonion_i1_sqr} : mul_OSNo Complex_i Complex_i = minus_OSNo 1
Known Quaternion_j_sqr^{Quaternion_j_sqr} : mul_HSNo Quaternion_j Quaternion_j = minus_HSNo 1
Theorem Octonion_i2_sqr^{Octonion_i2_sqr} : mul_OSNo Quaternion_j Quaternion_j = minus_OSNo 1
Known Quaternion_k_sqr^{Quaternion_k_sqr} : mul_HSNo Quaternion_k Quaternion_k = minus_HSNo 1
Theorem Octonion_i4_sqr^{Octonion_i4_sqr} : mul_OSNo Quaternion_k Quaternion_k = minus_OSNo 1
Param SNo^SNo : ι → ο
Known conj_HSNo_id_SNo^{conj_HSNo_id_SNo} : ∀ x0 . SNo x0 ⟶ conj_HSNo x0 = x0
Known SNo_1^SNo_1 : SNo 1
Known SNo_0^SNo_0 : SNo 0
Theorem Octonion_i0_sqr^{Octonion_i0_sqr} : mul_OSNo Octonion_i0 Octonion_i0 = minus_OSNo 1
Known conj_HSNo_i^conj_HSNo_i : conj_HSNo Complex_i = minus_HSNo Complex_i
Theorem Octonion_i3_sqr^{Octonion_i3_sqr} : mul_OSNo Octonion_i3 Octonion_i3 = minus_OSNo 1
Known conj_HSNo_k^conj_HSNo_k : conj_HSNo Quaternion_k = minus_HSNo Quaternion_k
Theorem Octonion_i5_sqr^{Octonion_i5_sqr} : mul_OSNo Octonion_i5 Octonion_i5 = minus_OSNo 1
Known conj_HSNo_j^conj_HSNo_j : conj_HSNo Quaternion_j = minus_HSNo Quaternion_j
Theorem Octonion_i6_sqr^{Octonion_i6_sqr} : mul_OSNo Octonion_i6 Octonion_i6 = minus_OSNo 1