Proofgold Address

Param ordsucc^ordsucc : ι → ι
Known ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2
Known neq_0_2^neq_0_2 : 0 = 2 ⟶ ∀ x0 : ο . x0
Theorem neq_1_3^neq_1_3 : 1 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_1_2^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0
Theorem neq_2_3^neq_2_3 : 2 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_2_4^neq_2_4 : 2 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_3_4^neq_3_4 : 3 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Param CD_mul^CD_mul : ι → (ι → ο) → (ι → ι) → (ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Definition CD_exp_nat^CD_exp_nat := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 . nat_primrec 1 (λ x7 . CD_mul x0 x1 x2 x3 x4 x5 x6)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 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 (proof)
Param nat_p^nat_p : ι → ο
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem 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) (proof)
Param CD_carr^CD_carr : ι → (ι → ο) → ι → ο
Known nat_0^nat_0 : nat_p 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
Theorem 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 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem 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 (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
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 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)
Theorem 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) (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param Sing^Sing : ι → ι
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_0_1^In_0_1 : 0 ∈ 1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Theorem not_TransSet_Sing_tagn^{not_TransSet_Sing_tagn} : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ not (TransSet (Sing x0)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem not_ordinal_Sing_tagn^{not_ordinal_Sing_tagn} : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ not (ordinal (Sing x0)) (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition ExtendedSNoElt_^{ExtendedSNoElt_} := λ x0 x1 . ∀ x2 . x2 ∈ prim3 x1 ⟶ or (ordinal x2) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = Sing x4) ⟶ x3) ⟶ x3)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem extension_SNoElt_mon^{extension_SNoElt_mon} : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 . ExtendedSNoElt_ x0 x2 ⟶ ExtendedSNoElt_ x1 x2 (proof)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known Sing_inj^Sing_inj : ∀ x0 x1 . Sing x0 = Sing x1 ⟶ x0 = x1
Known UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Theorem 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 (proof)
Param SNo^SNo : ι → ο
Known UnionE_impred^{UnionE_impred} : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2) ⟶ x2
Param binunion^binunion : ι → ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Definition SNoElts_^SNoElts_ := λ x0 . binunion x0 {SetAdjoin x1 (Sing 1)|x1 ∈ x0}
Param exactly1of2^exactly1of2 : ο → ο → ο
Definition SNo_^SNo_ := λ x0 x1 . and (x1 ⊆ SNoElts_ x0) (∀ x2 . x2 ∈ x0 ⟶ exactly1of2 (SetAdjoin x2 (Sing 1) ∈ x1) (x2 ∈ x1))
Param SNoLev^SNoLev : ι → ι
Known SNoLev_^SNoLev_ : ∀ x0 . SNo x0 ⟶ SNo_ (SNoLev x0) x0
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known SNoLev_ordinal^{SNoLev_ordinal} : ∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem SNo_ExtendedSNoElt_2^{SNo_ExtendedSNoElt_2} : ∀ x0 . SNo x0 ⟶ ExtendedSNoElt_ 2 x0 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem complex_tag_fresh^{complex_tag_fresh} : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nIn (Sing 2) x1 (proof)
Definition pair_tag^pair_tag := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 x0|x3 ∈ x2}
Definition SNo_pair^SNo_pair := pair_tag (Sing 2)
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 SNo_pair_0^SNo_pair_0 : ∀ x0 . SNo_pair x0 0 = x0 (proof)
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 SNo_pair_prop_1^{SNo_pair_prop_1} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x2 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x0 = x2 (proof)
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 SNo_pair_prop_2^{SNo_pair_prop_2} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x1 = x3 (proof)
Definition CSNo^CSNo := CD_carr (Sing 2) SNo
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 CSNo_I^CSNo_I : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo (SNo_pair x0 x1) (proof)
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 CSNo_E^CSNo_E : ∀ x0 . CSNo x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = SNo_pair x2 x3 ⟶ x1 (SNo_pair x2 x3)) ⟶ x1 x0 (proof)
Known SNo_0^SNo_0 : SNo 0
Theorem SNo_CSNo^SNo_CSNo : ∀ x0 . SNo x0 ⟶ CSNo x0 (proof)
Theorem CSNo_0^CSNo_0 : CSNo 0 (proof)
Known SNo_1^SNo_1 : SNo 1
Theorem CSNo_1^CSNo_1 : CSNo 1 (proof)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known In_2_3^In_2_3 : 2 ∈ 3
Theorem CSNo_ExtendedSNoElt_3^{CSNo_ExtendedSNoElt_3} : ∀ x0 . CSNo x0 ⟶ ExtendedSNoElt_ 3 x0 (proof)
Definition Complex_i^Complex_i := SNo_pair 0 1
Param CD_proj0^CD_proj0 : ι → (ι → ο) → ι → ι
Definition CSNo_Re^CSNo_Re := CD_proj0 (Sing 2) SNo
Param CD_proj1^CD_proj1 : ι → (ι → ο) → ι → ι
Definition CSNo_Im^CSNo_Im := CD_proj1 (Sing 2) SNo
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 : ο . (∀ x4 . and (x1 x4) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) x4) ⟶ x3) ⟶ x3)
Theorem CSNo_Re1^CSNo_Re1 : ∀ x0 . CSNo x0 ⟶ and (SNo (CSNo_Re x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = SNo_pair (CSNo_Re x0) x2) ⟶ x1) ⟶ x1) (proof)
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 CSNo_Re2^CSNo_Re2 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo_Re (SNo_pair x0 x1) = x0 (proof)
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 CSNo_Im1^CSNo_Im1 : ∀ x0 . CSNo x0 ⟶ and (SNo (CSNo_Im x0)) (x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0)) (proof)
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 CSNo_Im2^CSNo_Im2 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo_Im (SNo_pair x0 x1) = x1 (proof)
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 CSNo_ReR^CSNo_ReR : ∀ x0 . CSNo x0 ⟶ SNo (CSNo_Re x0) (proof)
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 CSNo_ImR^CSNo_ImR : ∀ x0 . CSNo x0 ⟶ SNo (CSNo_Im x0) (proof)
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 CSNo_ReIm^CSNo_ReIm : ∀ x0 . CSNo x0 ⟶ x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0) (proof)
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 CSNo_ReIm_split^{CSNo_ReIm_split} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Re x0 = CSNo_Re x1 ⟶ CSNo_Im x0 = CSNo_Im x1 ⟶ x0 = x1 (proof)
Definition CSNoLev^CSNoLev := λ x0 . binunion (SNoLev (CSNo_Re x0)) (SNoLev (CSNo_Im x0))
Known ordinal_binunion^{ordinal_binunion} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binunion x0 x1)
Theorem CSNoLev_ordinal^{CSNoLev_ordinal} : ∀ x0 . CSNo x0 ⟶ ordinal (CSNoLev x0) (proof)
Param CD_minus^CD_minus : ι → (ι → ο) → (ι → ι) → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Definition minus_CSNo^minus_CSNo := CD_minus (Sing 2) SNo minus_SNo
Param CD_conj^CD_conj : ι → (ι → ο) → (ι → ι) → (ι → ι) → ι → ι
Definition conj_CSNo^conj_CSNo := CD_conj (Sing 2) SNo minus_SNo (λ x0 . x0)
Param CD_add^CD_add : ι → (ι → ο) → (ι → ι → ι) → ι → ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Definition add_CSNo^add_CSNo := CD_add (Sing 2) SNo add_SNo
Param mul_SNo^mul_SNo : ι → ι → ι
Definition mul_CSNo^mul_CSNo := CD_mul (Sing 2) SNo minus_SNo (λ x0 . x0) add_SNo mul_SNo
Definition exp_CSNo_nat^exp_CSNo_nat := CD_exp_nat (Sing 2) SNo minus_SNo (λ x0 . x0) add_SNo mul_SNo
Param exp_SNo_nat^exp_SNo_nat : ι → ι → ι
Definition abs_sqr_CSNo^abs_sqr_CSNo := λ x0 . add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2)
Param div_SNo^div_SNo : ι → ι → ι
Definition recip_CSNo^recip_CSNo := λ x0 . SNo_pair (div_SNo (CSNo_Re x0) (abs_sqr_CSNo x0)) (minus_SNo (div_SNo (CSNo_Im x0) (abs_sqr_CSNo x0)))
Definition div_CSNo^div_CSNo := λ x0 x1 . mul_CSNo x0 (recip_CSNo x1)
Theorem CSNo_Complex_i^{CSNo_Complex_i} : CSNo Complex_i (proof)
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 SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem CSNo_minus_CSNo^{CSNo_minus_CSNo} : ∀ x0 . CSNo x0 ⟶ CSNo (minus_CSNo x0) (proof)
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_CSNo_CRe^{minus_CSNo_CRe} : ∀ x0 . CSNo x0 ⟶ CSNo_Re (minus_CSNo x0) = minus_SNo (CSNo_Re x0) (proof)
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_CSNo_CIm^{minus_CSNo_CIm} : ∀ x0 . CSNo x0 ⟶ CSNo_Im (minus_CSNo x0) = minus_SNo (CSNo_Im x0) (proof)
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)
Theorem CSNo_conj_CSNo^{CSNo_conj_CSNo} : ∀ x0 . CSNo x0 ⟶ CSNo (conj_CSNo x0) (proof)
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_CSNo_CRe^{conj_CSNo_CRe} : ∀ x0 . CSNo x0 ⟶ CSNo_Re (conj_CSNo x0) = CSNo_Re x0 (proof)
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_CSNo_CIm^{conj_CSNo_CIm} : ∀ x0 . CSNo x0 ⟶ CSNo_Im (conj_CSNo x0) = minus_SNo (CSNo_Im x0) (proof)
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 SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Theorem CSNo_add_CSNo^{CSNo_add_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (add_CSNo x0 x1) (proof)
Theorem CSNo_add_CSNo_3^{CSNo_add_CSNo_3} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo (add_CSNo x0 (add_CSNo x1 x2)) (proof)
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_CSNo_CRe^add_CSNo_CRe : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Re (add_CSNo x0 x1) = add_SNo (CSNo_Re x0) (CSNo_Re x1) (proof)
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_CSNo_CIm^add_CSNo_CIm : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Im (add_CSNo x0 x1) = add_SNo (CSNo_Im x0) (CSNo_Im x1) (proof)
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Theorem CSNo_mul_CSNo^{CSNo_mul_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (mul_CSNo x0 x1) (proof)
Theorem CSNo_mul_CSNo_3^{CSNo_mul_CSNo_3} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo (mul_CSNo x0 (mul_CSNo x1 x2)) (proof)
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_CSNo_CRe^mul_CSNo_CRe : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Re (mul_CSNo x0 x1) = add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x1) (CSNo_Im x0))) (proof)
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_CSNo_CIm^mul_CSNo_CIm : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Im (mul_CSNo x0 x1) = add_SNo (mul_SNo (CSNo_Im x1) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)) (proof)
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 SNo_Re^SNo_Re : ∀ x0 . SNo x0 ⟶ CSNo_Re x0 = x0 (proof)
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 SNo_Im^SNo_Im : ∀ x0 . SNo x0 ⟶ CSNo_Im x0 = 0 (proof)
Theorem Re_0^Re_0 : CSNo_Re 0 = 0 (proof)
Theorem Im_0^Im_0 : CSNo_Im 0 = 0 (proof)
Theorem Re_1^Re_1 : CSNo_Re 1 = 1 (proof)
Theorem Im_1^Im_1 : CSNo_Im 1 = 0 (proof)
Theorem Re_i^Re_i : CSNo_Re Complex_i = 0 (proof)
Theorem Im_i^Im_i : CSNo_Im Complex_i = 1 (proof)
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
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Theorem conj_CSNo_id_SNo^{conj_CSNo_id_SNo} : ∀ x0 . SNo x0 ⟶ conj_CSNo x0 = x0 (proof)
Theorem conj_CSNo_0^conj_CSNo_0 : conj_CSNo 0 = 0 (proof)
Theorem conj_CSNo_1^conj_CSNo_1 : conj_CSNo 1 = 1 (proof)
Theorem conj_CSNo_i^conj_CSNo_i : conj_CSNo Complex_i = minus_CSNo Complex_i (proof)
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
Theorem minus_CSNo_minus_SNo^{minus_CSNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ minus_CSNo x0 = minus_SNo x0 (proof)
Theorem minus_CSNo_0^minus_CSNo_0 : minus_CSNo 0 = 0 (proof)
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_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Theorem add_CSNo_add_SNo^{add_CSNo_add_SNo} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_CSNo x0 x1 = add_SNo x0 x1 (proof)
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_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Known mul_SNo_zeroL^{mul_SNo_zeroL} : ∀ x0 . SNo x0 ⟶ mul_SNo 0 x0 = 0
Known mul_SNo_zeroR^{mul_SNo_zeroR} : ∀ x0 . SNo x0 ⟶ mul_SNo x0 0 = 0
Theorem mul_CSNo_mul_SNo^{mul_CSNo_mul_SNo} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_CSNo x0 x1 = mul_SNo x0 x1 (proof)
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_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Theorem minus_CSNo_invol^{minus_CSNo_invol} : ∀ x0 . CSNo x0 ⟶ minus_CSNo (minus_CSNo x0) = x0 (proof)
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
Theorem conj_CSNo_invol^{conj_CSNo_invol} : ∀ x0 . CSNo x0 ⟶ conj_CSNo (conj_CSNo x0) = x0 (proof)
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)
Theorem conj_minus_CSNo^{conj_minus_CSNo} : ∀ x0 . CSNo x0 ⟶ conj_CSNo (minus_CSNo x0) = minus_CSNo (conj_CSNo x0) (proof)
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_SNo_distr^{minus_add_SNo_distr} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Theorem 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) (proof)
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)
Theorem 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) (proof)
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_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Theorem add_CSNo_com^add_CSNo_com : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ add_CSNo x0 x1 = add_CSNo x1 x0 (proof)
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_SNo_assoc^{add_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Theorem 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) (proof)
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_CSNo_0L^add_CSNo_0L : ∀ x0 . CSNo x0 ⟶ add_CSNo 0 x0 = x0 (proof)
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_CSNo_0R^add_CSNo_0R : ∀ x0 . CSNo x0 ⟶ add_CSNo x0 0 = x0 (proof)
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_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Theorem add_CSNo_minus_CSNo_linv^{add_CSNo_minus_CSNo_linv} : ∀ x0 . CSNo x0 ⟶ add_CSNo (minus_CSNo x0) x0 = 0 (proof)
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_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Theorem add_CSNo_minus_CSNo_rinv^{add_CSNo_minus_CSNo_rinv} : ∀ x0 . CSNo x0 ⟶ add_CSNo x0 (minus_CSNo x0) = 0 (proof)
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_CSNo_0R^mul_CSNo_0R : ∀ x0 . CSNo x0 ⟶ mul_CSNo x0 0 = 0 (proof)
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_CSNo_0L^mul_CSNo_0L : ∀ x0 . CSNo x0 ⟶ mul_CSNo 0 x0 = 0 (proof)
Known mul_SNo_oneR^mul_SNo_oneR : ∀ x0 . SNo x0 ⟶ mul_SNo x0 1 = x0
Theorem mul_CSNo_1R^mul_CSNo_1R : ∀ x0 . CSNo x0 ⟶ mul_CSNo x0 1 = x0 (proof)
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_SNo_oneL^mul_SNo_oneL : ∀ x0 . SNo x0 ⟶ mul_SNo 1 x0 = x0
Theorem mul_CSNo_1L^mul_CSNo_1L : ∀ x0 . CSNo x0 ⟶ mul_CSNo 1 x0 = x0 (proof)
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 mul_SNo_com^mul_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 x1 = mul_SNo x1 x0
Known mul_SNo_minus_distrR^{mul_SNo_minus_distrR} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_minus_distrL^{mul_SNo_minus_distrL} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Theorem 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) (proof)
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_SNo_distrL^{mul_SNo_distrL} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known mul_SNo_distrR^{mul_SNo_distrR} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Theorem 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) (proof)
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_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) (proof)
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_CSNo_distrR^{minus_mul_CSNo_distrR} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 (minus_CSNo x1) = minus_CSNo (mul_CSNo x0 x1) (proof)
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_CSNo_distrL^{minus_mul_CSNo_distrL} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo (minus_CSNo x0) x1 = minus_CSNo (mul_CSNo x0 x1) (proof)
Theorem exp_CSNo_nat_0^{exp_CSNo_nat_0} : ∀ x0 . exp_CSNo_nat x0 0 = 1 (proof)
Theorem exp_CSNo_nat_S^{exp_CSNo_nat_S} : ∀ x0 x1 . nat_p x1 ⟶ exp_CSNo_nat x0 (ordsucc x1) = mul_CSNo x0 (exp_CSNo_nat x0 x1) (proof)
Theorem exp_CSNo_nat_1^{exp_CSNo_nat_1} : ∀ x0 . CSNo x0 ⟶ exp_CSNo_nat x0 1 = x0 (proof)
Theorem exp_CSNo_nat_2^{exp_CSNo_nat_2} : ∀ x0 . CSNo x0 ⟶ exp_CSNo_nat x0 2 = mul_CSNo x0 x0 (proof)
Theorem CSNo_exp_CSNo_nat^{CSNo_exp_CSNo_nat} : ∀ x0 . CSNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ CSNo (exp_CSNo_nat x0 x1) (proof)
Known add_SNo_com_4_inner_mid^{add_SNo_com_4_inner_mid} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x2) (add_SNo x1 x3)
Theorem add_SNo_rotate_4_0312^{add_SNo_rotate_4_0312} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x3) (add_SNo x1 x2) (proof)
Theorem mul_CSNo_com^mul_CSNo_com : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 x1 = mul_CSNo x1 x0 (proof)
Known mul_SNo_assoc^{mul_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known SNo_mul_SNo_3^{SNo_mul_SNo_3} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo (mul_SNo x0 (mul_SNo x1 x2))
Known mul_SNo_com_3_0_1^{mul_SNo_com_3_0_1} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo x1 (mul_SNo x0 x2)
Theorem 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 (proof)
Theorem Complex_i_sqr^{Complex_i_sqr} : mul_CSNo Complex_i Complex_i = minus_CSNo 1 (proof)