Proofgold Address

Param nat_p^nat_p : ι → ο
Param CSNo^CSNo : ι → ο
Param SNo^SNo : ι → ο
Known SNo_CSNo^SNo_CSNo : ∀ x0 . SNo x0 ⟶ CSNo x0
Known nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0
Theorem 8e48f.. : ∀ x0 . nat_p x0 ⟶ CSNo x0 (proof)
Param omega^omega : ι
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Theorem cda83.. : ∀ x0 . x0 ∈ omega ⟶ CSNo x0 (proof)
Param ordsucc^ordsucc : ι → ι
Known nat_2^nat_2 : nat_p 2
Theorem b5896.. : CSNo 2 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 4ca87.. : CSNo 3 (proof)
Known nat_4^nat_4 : nat_p 4
Theorem 867a5.. : CSNo 4 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem 39239.. : CSNo 5 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem 178fe.. : CSNo 6 (proof)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem nat_7^nat_7 : nat_p 7 (proof)
Theorem nat_8^nat_8 : nat_p 8 (proof)
Theorem nat_9^nat_9 : nat_p 9 (proof)
Theorem nat_10^nat_10 : nat_p 10 (proof)
Theorem nat_11^nat_11 : nat_p 11 (proof)
Theorem nat_12^nat_12 : nat_p 12 (proof)
Theorem 98eed.. : CSNo 7 (proof)
Theorem ffd25.. : CSNo 8 (proof)
Theorem 805c6.. : CSNo 9 (proof)
Theorem 46c70.. : CSNo 10 (proof)
Theorem d5cda.. : CSNo 11 (proof)
Theorem bcdcb.. : CSNo 12 (proof)
Param add_nat^add_nat : ι → ι → ι
Param add_CSNo^add_CSNo : ι → ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Known add_nat_add_SNo^{add_nat_add_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = add_SNo x0 x1
Known add_SNo_add_CSNo^{add_SNo_add_CSNo} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_CSNo x0 x1
Theorem e3ea0.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = add_CSNo x0 x1 (proof)
Param mul_nat^mul_nat : ι → ι → ι
Param mul_CSNo^mul_CSNo : ι → ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Known mul_nat_mul_SNo^{mul_nat_mul_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Known 15de6..^{mul_SNo_mul_CSNo} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 x1 = mul_CSNo x0 x1
Theorem 3fd00.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_CSNo x0 x1 (proof)
Known SNo_1^SNo_1 : SNo 1
Known add_SNo_1_ordsucc^{add_SNo_1_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ add_SNo x0 1 = ordsucc x0
Theorem ba236.. : ∀ x0 . x0 ∈ omega ⟶ add_CSNo x0 1 = ordsucc x0 (proof)
Known add_SNo_1_1_2^{add_SNo_1_1_2} : add_SNo 1 1 = 2
Theorem ac420.. : add_CSNo 1 1 = 2 (proof)
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Theorem d87c7.. : ∀ x0 . x0 ∈ omega ⟶ add_CSNo x0 1 ∈ omega (proof)
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Theorem d7cb6.. : ∀ x0 . nat_p x0 ⟶ nat_p (add_CSNo x0 1) (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem 0d126.. : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (add_CSNo x1 1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1 (proof)
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Theorem 5322b.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_CSNo x0 x1) (proof)
Theorem 3ca48.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_CSNo x0 x1 ∈ omega (proof)
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Theorem 62e8d.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_CSNo x0 x1) (proof)
Theorem cad16.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_CSNo x0 x1 ∈ omega (proof)
Param minus_CSNo^minus_CSNo : ι → ι
Param minus_SNo^minus_SNo : ι → ι
Known minus_SNo_minus_CSNo^{minus_SNo_minus_CSNo} : ∀ x0 . SNo x0 ⟶ minus_SNo x0 = minus_CSNo x0
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem 38e3f.. : ∀ x0 . SNo x0 ⟶ SNo (minus_CSNo x0) (proof)
Param ordinal^ordinal : ι → ο
Param SNoS_^SNoS_ : ι → ι
Param SNoLev^SNoLev : ι → ι
Param SNo_^SNo_ : ι → ι → ο
Known SNoS_E2^SNoS_E2 : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (SNoLev x1 ∈ x0 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNo_ (SNoLev x1) x1 ⟶ x2) ⟶ x2
Known minus_SNo_SNoS_^{minus_SNo_SNoS_} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ minus_SNo x1 ∈ SNoS_ x0
Theorem 4be12.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ minus_CSNo x1 ∈ SNoS_ x0 (proof)
Known omega_ordinal^{omega_ordinal} : ordinal omega
Theorem d19ee.. : ∀ x0 . x0 ∈ SNoS_ omega ⟶ minus_CSNo x0 ∈ SNoS_ omega (proof)
Known SNo_0^SNo_0 : SNo 0
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Theorem 49d57.. : minus_CSNo 0 = 0 (proof)
Known add_SNo_SNoS_omega^{add_SNo_SNoS_omega} : ∀ x0 . x0 ∈ SNoS_ omega ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ add_SNo x0 x1 ∈ SNoS_ omega
Theorem a2a5a.. : ∀ x0 . x0 ∈ SNoS_ omega ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ add_CSNo x0 x1 ∈ SNoS_ omega (proof)
Known mul_SNo_SNoS_omega^{mul_SNo_SNoS_omega} : ∀ x0 . x0 ∈ SNoS_ omega ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ mul_SNo x0 x1 ∈ SNoS_ omega
Theorem c48a8.. : ∀ x0 . x0 ∈ SNoS_ omega ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ mul_CSNo x0 x1 ∈ SNoS_ omega (proof)
Param real^real : ι
Known real_SNo^real_SNo : ∀ x0 . x0 ∈ real ⟶ SNo x0
Theorem 19f04.. : ∀ x0 . x0 ∈ real ⟶ CSNo x0 (proof)
Known real_minus_SNo^{real_minus_SNo} : ∀ x0 . x0 ∈ real ⟶ minus_SNo x0 ∈ real
Theorem 3b174.. : ∀ x0 . x0 ∈ real ⟶ minus_CSNo x0 ∈ real (proof)
Known real_add_SNo^real_add_SNo : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ add_SNo x0 x1 ∈ real
Theorem 050a2.. : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ add_CSNo x0 x1 ∈ real (proof)
Known real_mul_SNo^real_mul_SNo : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ mul_SNo x0 x1 ∈ real
Theorem 10a08.. : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ mul_CSNo x0 x1 ∈ real (proof)
Param SNoLt^SNoLt : ι → ι → ο
Known pos_mul_SNo_Lt^{pos_mul_SNo_Lt} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt 0 x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x1 x2 ⟶ SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem f01a1.. : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt 0 x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x1 x2 ⟶ SNoLt (mul_CSNo x0 x1) (mul_CSNo x0 x2) (proof)
Param SNoLe^SNoLe : ι → ι → ο
Known nonneg_mul_SNo_Le^{nonneg_mul_SNo_Le} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLe 0 x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x1 x2 ⟶ SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem c79f0.. : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLe 0 x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x1 x2 ⟶ SNoLe (mul_CSNo x0 x1) (mul_CSNo x0 x2) (proof)
Known neg_mul_SNo_Lt^{neg_mul_SNo_Lt} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt x0 0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x2 x1 ⟶ SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem 8c948.. : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt x0 0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x2 x1 ⟶ SNoLt (mul_CSNo x0 x1) (mul_CSNo x0 x2) (proof)
Known nonpos_mul_SNo_Le^{nonpos_mul_SNo_Le} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLe x0 0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x2 x1 ⟶ SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem 7eaf7.. : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLe x0 0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x2 x1 ⟶ SNoLe (mul_CSNo x0 x1) (mul_CSNo x0 x2) (proof)
Param int^int : ι
Known int_SNo^int_SNo : ∀ x0 . x0 ∈ int ⟶ SNo x0
Theorem 17997.. : ∀ x0 . x0 ∈ int ⟶ CSNo x0 (proof)
Known int_SNo_cases^{int_SNo_cases} : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int ⟶ x0 x1
Theorem 8d681.. : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_CSNo x1)) ⟶ ∀ x1 . x1 ∈ int ⟶ x0 x1 (proof)
Known int_minus_SNo_omega^{int_minus_SNo_omega} : ∀ x0 . x0 ∈ omega ⟶ minus_SNo x0 ∈ int
Theorem 5f1f1.. : ∀ x0 . x0 ∈ omega ⟶ minus_CSNo x0 ∈ int (proof)
Known int_minus_SNo^{int_minus_SNo} : ∀ x0 . x0 ∈ int ⟶ minus_SNo x0 ∈ int
Theorem fd579.. : ∀ x0 . x0 ∈ int ⟶ minus_CSNo x0 ∈ int (proof)
Known int_add_SNo^int_add_SNo : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ add_SNo x0 x1 ∈ int
Theorem 17a6b.. : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ add_CSNo x0 x1 ∈ int (proof)
Known int_mul_SNo^int_mul_SNo : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ mul_SNo x0 x1 ∈ int
Theorem 2ed53.. : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ mul_CSNo x0 x1 ∈ int (proof)
Param and^and : ο → ο → ο
Known nonpos_nonneg_0^{nonpos_nonneg_0} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ x0 = minus_SNo x1 ⟶ and (x0 = 0) (x1 = 0)
Theorem 7a28f.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ x0 = minus_CSNo x1 ⟶ and (x0 = 0) (x1 = 0) (proof)
Known add_CSNo_0L^add_CSNo_0L : ∀ x0 . CSNo x0 ⟶ add_CSNo 0 x0 = x0
Known add_CSNo_minus_CSNo_linv^{add_CSNo_minus_CSNo_linv} : ∀ x0 . CSNo x0 ⟶ add_CSNo (minus_CSNo x0) x0 = 0
Known b63e9..^{add_CSNo_assoc} : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 (add_CSNo x1 x2) = add_CSNo (add_CSNo x0 x1) x2
Known CSNo_minus_CSNo^{CSNo_minus_CSNo} : ∀ x0 . CSNo x0 ⟶ CSNo (minus_CSNo x0)
Theorem 774b1.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 x1 = add_CSNo x0 x2 ⟶ x1 = x2 (proof)
Known 80a5b..^add_CSNo_com : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ add_CSNo x0 x1 = add_CSNo x1 x0
Theorem 91217.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 x2 = add_CSNo x1 x2 ⟶ x0 = x1 (proof)
Known add_CSNo_minus_CSNo_rinv^{add_CSNo_minus_CSNo_rinv} : ∀ x0 . CSNo x0 ⟶ add_CSNo x0 (minus_CSNo x0) = 0
Theorem f31b7.. : ∀ x0 . CSNo x0 ⟶ minus_CSNo (minus_CSNo x0) = x0 (proof)
Known b5ed6..^CSNo_0 : CSNo 0
Known b904d..^{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 d8721..^{CSNo_mul_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (mul_CSNo x0 x1)
Theorem 8910b.. : ∀ x0 . CSNo x0 ⟶ mul_CSNo x0 0 = 0 (proof)
Known 1e9ba..^mul_CSNo_com : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 x1 = mul_CSNo x1 x0
Theorem c498d.. : ∀ x0 . CSNo x0 ⟶ mul_CSNo 0 x0 = 0 (proof)
Known ca69e..^CSNo_1 : CSNo 1
Theorem 402a9.. : CSNo (minus_CSNo 1) (proof)
Known b0c29.. : ∀ 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)
Theorem 83fc4.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo (minus_CSNo x0) x1 = minus_CSNo (mul_CSNo x0 x1) (proof)
Known 42258..^{mul_CSNo_oneL} : ∀ x0 . CSNo x0 ⟶ mul_CSNo 1 x0 = x0
Theorem 4367a.. : ∀ x0 . CSNo x0 ⟶ minus_CSNo x0 = mul_CSNo (minus_CSNo 1) x0 (proof)
Theorem 7c9be.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo x0 (minus_CSNo x1) = minus_CSNo (mul_CSNo x0 x1) (proof)
Theorem c2cf9.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ mul_CSNo (minus_CSNo x0) (minus_CSNo x1) = mul_CSNo x0 x1 (proof)
Known CSNo_add_CSNo^{CSNo_add_CSNo} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo (add_CSNo x0 x1)
Theorem 07327.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo (add_CSNo x0 (add_CSNo x1 x2)) (proof)
Theorem c0d7a.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo (add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3))) (proof)
Theorem 3b0a9.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3)) = add_CSNo (add_CSNo x0 (add_CSNo x1 x2)) x3 (proof)
Theorem 77d52.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 (add_CSNo x1 x2) = add_CSNo x1 (add_CSNo x0 x2) (proof)
Theorem d50ac.. : ∀ x0 x1 x2 x3 . CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3)) = add_CSNo x0 (add_CSNo x2 (add_CSNo x1 x3)) (proof)
Theorem 0158e.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo (add_CSNo x0 x1) x2 = add_CSNo (add_CSNo x0 x2) x1 (proof)
Theorem 9cf3a.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo (add_CSNo x0 x1) (add_CSNo x2 x3) = add_CSNo (add_CSNo x0 x2) (add_CSNo x1 x3) (proof)
Theorem 830c3.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ add_CSNo x0 (add_CSNo x1 x2) = add_CSNo x2 (add_CSNo x0 x1) (proof)
Theorem bc2ff.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3)) = add_CSNo x3 (add_CSNo x0 (add_CSNo x1 x2)) (proof)
Theorem f4c9f.. : ∀ x0 x1 x2 x3 x4 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo x4 ⟶ add_CSNo x0 (add_CSNo x1 (add_CSNo x2 (add_CSNo x3 x4))) = add_CSNo x4 (add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3))) (proof)
Theorem fda98.. : ∀ x0 x1 x2 x3 x4 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo x4 ⟶ add_CSNo x0 (add_CSNo x1 (add_CSNo x2 (add_CSNo x3 x4))) = add_CSNo x3 (add_CSNo x4 (add_CSNo x0 (add_CSNo x1 x2))) (proof)
Theorem 23844.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ add_CSNo (minus_CSNo x0) (add_CSNo x0 x1) = x1 (proof)
Theorem c3fb2.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ add_CSNo x0 (add_CSNo (minus_CSNo x0) x1) = x1 (proof)
Theorem f6d70.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo (add_CSNo x0 (add_CSNo x1 x2)) (add_CSNo (minus_CSNo x2) x3) = add_CSNo x0 (add_CSNo x1 x3) (proof)
Theorem a5bd5.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo (add_CSNo x0 (add_CSNo x1 x2)) (add_CSNo x3 (minus_CSNo x2)) = add_CSNo x0 (add_CSNo x1 x3) (proof)
Theorem da08a.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ add_CSNo (add_CSNo x0 (add_CSNo x1 (minus_CSNo x2))) (add_CSNo x2 x3) = add_CSNo x0 (add_CSNo x1 x3) (proof)
Theorem be33e.. : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ minus_CSNo (add_CSNo x0 x1) = add_CSNo (minus_CSNo x0) (minus_CSNo x1) (proof)
Theorem 08a29.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo (mul_CSNo x0 (mul_CSNo x1 x2)) (proof)
Theorem 58b75.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo (mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3))) (proof)
Known 8912c..^{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
Theorem ca54e.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3)) = mul_CSNo (mul_CSNo x0 (mul_CSNo x1 x2)) x3 (proof)
Theorem 4ef1d.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo x0 (mul_CSNo x1 x2) = mul_CSNo x1 (mul_CSNo x0 x2) (proof)
Theorem 68fb9.. : ∀ x0 x1 x2 x3 . CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3)) = mul_CSNo x0 (mul_CSNo x2 (mul_CSNo x1 x3)) (proof)
Theorem f89cf.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo (mul_CSNo x0 x1) x2 = mul_CSNo (mul_CSNo x0 x2) x1 (proof)
Theorem 4f364.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ mul_CSNo (mul_CSNo x0 x1) (mul_CSNo x2 x3) = mul_CSNo (mul_CSNo x0 x2) (mul_CSNo x1 x3) (proof)
Theorem 95f36.. : ∀ x0 x1 x2 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ mul_CSNo x0 (mul_CSNo x1 x2) = mul_CSNo x2 (mul_CSNo x0 x1) (proof)
Theorem dc318.. : ∀ x0 x1 x2 x3 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3)) = mul_CSNo x3 (mul_CSNo x0 (mul_CSNo x1 x2)) (proof)
Theorem 7db7f.. : ∀ x0 x1 x2 x3 x4 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo x4 ⟶ mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 (mul_CSNo x3 x4))) = mul_CSNo x4 (mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3))) (proof)
Theorem aa263.. : ∀ x0 x1 x2 x3 x4 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo x2 ⟶ CSNo x3 ⟶ CSNo x4 ⟶ mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 (mul_CSNo x3 x4))) = mul_CSNo x3 (mul_CSNo x4 (mul_CSNo x0 (mul_CSNo x1 x2))) (proof)