Search for blocks/addresses/...

Proofgold Address

address
PUVtnjvVWYH1wGRXF1CARC3bcab4KjKPmWu
total
0
mg
-
conjpub
-
current assets
2d7e6../1d8c7.. bday: 5161 doc published by Pr6Pc..
Param omegaomega : ι
Param mul_natmul_nat : ιιι
Param mul_SNomul_SNo : ιιι
Param nat_pnat_p : ιο
Param ordinalordinal : ιο
Param SNoSNo : ιο
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Param add_natadd_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Param add_SNoadd_SNo : ιιι
Known add_nat_add_SNoadd_nat_add_SNo : ∀ x0 . x0omega∀ x1 . x1omegaadd_nat x0 x1 = add_SNo x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known add_SNo_ordinal_SLadd_SNo_ordinal_SL : ∀ x0 . ordinal x0∀ x1 . ordinal x1add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1)
Known ordinal_Emptyordinal_Empty : ordinal 0
Known mul_SNo_distrLmul_SNo_distrL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_1SNo_1 : SNo 1
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Theorem mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1 (proof)
Param minus_SNominus_SNo : ιι
Param binunionbinunion : ιιι
Param minus_CSNominus_CSNo : ιι
Definition int_alt1int := binunion omega (prim5 omega minus_CSNo)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known minus_SNo_minus_CSNominus_SNo_minus_CSNo : ∀ x0 . SNo x0minus_SNo x0 = minus_CSNo x0
Theorem a3283..int_SNo_cases : ∀ x0 : ι → ο . (∀ x1 . x1omegax0 x1)(∀ x1 . x1omegax0 (minus_SNo x1))∀ x1 . x1int_alt1x0 x1 (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Theorem c3d99..Subq_omega_int : omegaint_alt1 (proof)
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Theorem 1b4d5..int_minus_SNo_omega : ∀ x0 . x0omegaminus_SNo x0int_alt1 (proof)
Theorem ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0 (proof)
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_com_3_0_1add_SNo_com_3_0_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x1 (add_SNo x0 x2)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known nat_1nat_1 : nat_p 1
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known add_SNo_minus_SNo_prop2add_SNo_minus_SNo_prop2 : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Theorem 6fbb0..int_add_SNo_lem : ∀ x0 . x0omega∀ x1 . nat_p x1add_SNo (minus_SNo x0) x1int_alt1 (proof)
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Theorem a0aa5..int_add_SNo : ∀ x0 . x0int_alt1∀ x1 . x1int_alt1add_SNo x0 x1int_alt1 (proof)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Theorem daaad..int_minus_SNo : ∀ x0 . x0int_alt1minus_SNo x0int_alt1 (proof)
Theorem mul_SNo_In_omegamul_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegamul_SNo x0 x1omega (proof)
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Theorem eefdf..int_mul_SNo : ∀ x0 . x0int_alt1∀ x1 . x1int_alt1mul_SNo x0 x1int_alt1 (proof)
Param SNo_pairSNo_pair : ιιι
Param CSNo_ReCSNo_Re : ιι
Param CSNo_ImCSNo_Im : ιι
Definition mul_CSNomul_CSNo := λ x0 x1 . SNo_pair (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1)))) (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)))
Known SNo_ReSNo_Re : ∀ x0 . SNo x0CSNo_Re x0 = x0
Known SNo_pair_0SNo_pair_0 : ∀ x0 . SNo_pair x0 0 = x0
Known SNo_ImSNo_Im : ∀ x0 . SNo x0CSNo_Im x0 = 0
Known SNo_0SNo_0 : SNo 0
Theorem 15de6..mul_SNo_mul_CSNo : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_CSNo x0 x1 (proof)
Known add_SNo_rotate_4_1add_SNo_rotate_4_1 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo x0 (add_SNo x1 (add_SNo x2 x3)) = add_SNo x3 (add_SNo x0 (add_SNo x1 x2))
Known SNo_add_SNo_3SNo_add_SNo_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (add_SNo x0 (add_SNo x1 x2))
Theorem add_SNo_rotate_5_1add_SNo_rotate_5_1 : ∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 x4))) = add_SNo x4 (add_SNo x0 (add_SNo x1 (add_SNo x2 x3))) (proof)
Theorem add_SNo_rotate_5_2add_SNo_rotate_5_2 : ∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 x4))) = add_SNo x3 (add_SNo x4 (add_SNo x0 (add_SNo x1 x2))) (proof)
Param SNoLSNoL : ιι
Param SNoLeSNoLe : ιιο
Param SNoRSNoR : ιι
Param SNoLtSNoLt : ιιο
Param SNoS_SNoS_ : ιι
Param SNoLevSNoLev : ιι
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Known SNoL_SNoSSNoL_SNoS : ∀ x0 . SNo x0∀ x1 . x1SNoL x0x1SNoS_ (SNoLev x0)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known SNoR_SNoSSNoR_SNoS : ∀ x0 . SNo x0∀ x1 . x1SNoR x0x1SNoS_ (SNoLev x0)
Param SNo_SNo_ : ιιο
Known SNoS_E2SNoS_E2 : ∀ x0 . ordinal x0∀ x1 . x1SNoS_ x0∀ x2 : ο . (SNoLev x1x0ordinal (SNoLev x1)SNo x1SNo_ (SNoLev x1) x1x2)x2
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Known add_SNo_minus_Lt1b3add_SNo_minus_Lt1b3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt (add_SNo x0 x1) (add_SNo x3 x2)SNoLt (add_SNo x0 (add_SNo x1 (minus_SNo x2))) x3
Known add_SNo_Lt1_canceladd_SNo_Lt1_cancel : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)SNoLt x0 x2
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known SNo_add_SNo_4SNo_add_SNo_4 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 x3)))
Known add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Theorem mul_SNo_assoc_lem1mul_SNo_assoc_lem1 : ∀ x0 : ι → ι → ι . (∀ x1 x2 . SNo x1SNo x2SNo (x0 x1 x2))(∀ x1 x2 x3 . SNo x1SNo x2SNo x3x0 x1 (add_SNo x2 x3) = add_SNo (x0 x1 x2) (x0 x1 x3))(∀ x1 x2 x3 . SNo x1SNo x2SNo x3x0 (add_SNo x1 x2) x3 = add_SNo (x0 x1 x3) (x0 x2 x3))(∀ x1 x2 . SNo x1SNo x2∀ x3 . x3SNoL (x0 x1 x2)∀ x4 : ο . (∀ x5 . x5SNoL x1∀ x6 . x6SNoL x2SNoLe (add_SNo x3 (x0 x5 x6)) (add_SNo (x0 x5 x2) (x0 x1 x6))x4)(∀ x5 . x5SNoR x1∀ x6 . x6SNoR x2SNoLe (add_SNo x3 (x0 x5 x6)) (add_SNo (x0 x5 x2) (x0 x1 x6))x4)x4)(∀ x1 x2 . SNo x1SNo x2∀ x3 . x3SNoR (x0 x1 x2)∀ x4 : ο . (∀ x5 . x5SNoL x1∀ x6 . x6SNoR x2SNoLe (add_SNo (x0 x5 x2) (x0 x1 x6)) (add_SNo x3 (x0 x5 x6))x4)(∀ x5 . x5SNoR x1∀ x6 . x6SNoL x2SNoLe (add_SNo (x0 x5 x2) (x0 x1 x6)) (add_SNo x3 (x0 x5 x6))x4)x4)(∀ x1 x2 x3 x4 . SNo x1SNo x2SNo x3SNo x4SNoLt x3 x1SNoLt x4 x2SNoLt (add_SNo (x0 x3 x2) (x0 x1 x4)) (add_SNo (x0 x1 x2) (x0 x3 x4)))(∀ x1 x2 x3 x4 . SNo x1SNo x2SNo x3SNo x4SNoLe x3 x1SNoLe x4 x2SNoLe (add_SNo (x0 x3 x2) (x0 x1 x4)) (add_SNo (x0 x1 x2) (x0 x3 x4)))∀ x1 x2 x3 . SNo x1SNo x2SNo x3(∀ x4 . x4SNoS_ (SNoLev x1)x0 x4 (x0 x2 x3) = x0 (x0 x4 x2) x3)(∀ x4 . x4SNoS_ (SNoLev x2)x0 x1 (x0 x4 x3) = x0 (x0 x1 x4) x3)(∀ x4 . x4SNoS_ (SNoLev x3)x0 x1 (x0 x2 x4) = x0 (x0 x1 x2) x4)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)x0 x4 (x0 x5 x3) = x0 (x0 x4 x5) x3)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x3)x0 x4 (x0 x2 x5) = x0 (x0 x4 x2) x5)(∀ x4 . x4SNoS_ (SNoLev x2)∀ x5 . x5SNoS_ (SNoLev x3)x0 x1 (x0 x4 x5) = x0 (x0 x1 x4) x5)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)∀ x6 . x6SNoS_ (SNoLev x3)x0 x4 (x0 x5 x6) = x0 (x0 x4 x5) x6)∀ x4 . (∀ x5 . x5x4∀ x6 : ο . (∀ x7 . x7SNoL x1∀ x8 . x8SNoL (x0 x2 x3)x5 = add_SNo (x0 x7 (x0 x2 x3)) (add_SNo (x0 x1 x8) (minus_SNo (x0 x7 x8)))x6)(∀ x7 . x7SNoR x1∀ x8 . x8SNoR (x0 x2 x3)x5 = add_SNo (x0 x7 (x0 x2 x3)) (add_SNo (x0 x1 x8) (minus_SNo (x0 x7 x8)))x6)x6)∀ x5 . x5x4SNoLt x5 (x0 (x0 x1 x2) x3) (proof)
Known add_SNo_minus_Lt2b3add_SNo_minus_Lt2b3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt (add_SNo x3 x2) (add_SNo x0 x1)SNoLt x3 (add_SNo x0 (add_SNo x1 (minus_SNo x2)))
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Theorem mul_SNo_assoc_lem2mul_SNo_assoc_lem2 : ∀ x0 : ι → ι → ι . (∀ x1 x2 . SNo x1SNo x2SNo (x0 x1 x2))(∀ x1 x2 x3 . SNo x1SNo x2SNo x3x0 x1 (add_SNo x2 x3) = add_SNo (x0 x1 x2) (x0 x1 x3))(∀ x1 x2 x3 . SNo x1SNo x2SNo x3x0 (add_SNo x1 x2) x3 = add_SNo (x0 x1 x3) (x0 x2 x3))(∀ x1 x2 . SNo x1SNo x2∀ x3 . x3SNoL (x0 x1 x2)∀ x4 : ο . (∀ x5 . x5SNoL x1∀ x6 . x6SNoL x2SNoLe (add_SNo x3 (x0 x5 x6)) (add_SNo (x0 x5 x2) (x0 x1 x6))x4)(∀ x5 . x5SNoR x1∀ x6 . x6SNoR x2SNoLe (add_SNo x3 (x0 x5 x6)) (add_SNo (x0 x5 x2) (x0 x1 x6))x4)x4)(∀ x1 x2 . SNo x1SNo x2∀ x3 . x3SNoR (x0 x1 x2)∀ x4 : ο . (∀ x5 . x5SNoL x1∀ x6 . x6SNoR x2SNoLe (add_SNo (x0 x5 x2) (x0 x1 x6)) (add_SNo x3 (x0 x5 x6))x4)(∀ x5 . x5SNoR x1∀ x6 . x6SNoL x2SNoLe (add_SNo (x0 x5 x2) (x0 x1 x6)) (add_SNo x3 (x0 x5 x6))x4)x4)(∀ x1 x2 x3 x4 . SNo x1SNo x2SNo x3SNo x4SNoLt x3 x1SNoLt x4 x2SNoLt (add_SNo (x0 x3 x2) (x0 x1 x4)) (add_SNo (x0 x1 x2) (x0 x3 x4)))(∀ x1 x2 x3 x4 . SNo x1SNo x2SNo x3SNo x4SNoLe x3 x1SNoLe x4 x2SNoLe (add_SNo (x0 x3 x2) (x0 x1 x4)) (add_SNo (x0 x1 x2) (x0 x3 x4)))∀ x1 x2 x3 . SNo x1SNo x2SNo x3(∀ x4 . x4SNoS_ (SNoLev x1)x0 x4 (x0 x2 x3) = x0 (x0 x4 x2) x3)(∀ x4 . x4SNoS_ (SNoLev x2)x0 x1 (x0 x4 x3) = x0 (x0 x1 x4) x3)(∀ x4 . x4SNoS_ (SNoLev x3)x0 x1 (x0 x2 x4) = x0 (x0 x1 x2) x4)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)x0 x4 (x0 x5 x3) = x0 (x0 x4 x5) x3)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x3)x0 x4 (x0 x2 x5) = x0 (x0 x4 x2) x5)(∀ x4 . x4SNoS_ (SNoLev x2)∀ x5 . x5SNoS_ (SNoLev x3)x0 x1 (x0 x4 x5) = x0 (x0 x1 x4) x5)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)∀ x6 . x6SNoS_ (SNoLev x3)x0 x4 (x0 x5 x6) = x0 (x0 x4 x5) x6)∀ x4 . (∀ x5 . x5x4∀ x6 : ο . (∀ x7 . x7SNoL x1∀ x8 . x8SNoR (x0 x2 x3)x5 = add_SNo (x0 x7 (x0 x2 x3)) (add_SNo (x0 x1 x8) (minus_SNo (x0 x7 x8)))x6)(∀ x7 . x7SNoR x1∀ x8 . x8SNoL (x0 x2 x3)x5 = add_SNo (x0 x7 (x0 x2 x3)) (add_SNo (x0 x1 x8) (minus_SNo (x0 x7 x8)))x6)x6)∀ x5 . x5x4SNoLt (x0 (x0 x1 x2) x3) x5 (proof)
Known SNoLev_ind3SNoLev_ind3 : ∀ x0 : ι → ι → ι → ο . (∀ x1 x2 x3 . SNo x1SNo x2SNo x3(∀ x4 . x4SNoS_ (SNoLev x1)x0 x4 x2 x3)(∀ x4 . x4SNoS_ (SNoLev x2)x0 x1 x4 x3)(∀ x4 . x4SNoS_ (SNoLev x3)x0 x1 x2 x4)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)x0 x4 x5 x3)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x3)x0 x4 x2 x5)(∀ x4 . x4SNoS_ (SNoLev x2)∀ x5 . x5SNoS_ (SNoLev x3)x0 x1 x4 x5)(∀ x4 . x4SNoS_ (SNoLev x1)∀ x5 . x5SNoS_ (SNoLev x2)∀ x6 . x6SNoS_ (SNoLev x3)x0 x4 x5 x6)x0 x1 x2 x3)∀ x1 x2 x3 . SNo x1SNo x2SNo x3x0 x1 x2 x3
Param SNoCutPSNoCutP : ιιο
Param SNoCutSNoCut : ιιι
Known mul_SNo_eq_3mul_SNo_eq_3 : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (∀ x3 x4 . SNoCutP x3 x4(∀ x5 . x5x3∀ x6 : ο . (∀ x7 . x7SNoL x0∀ x8 . x8SNoL x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)(∀ x7 . x7SNoR x0∀ x8 . x8SNoR x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)x6)(∀ x5 . x5SNoL x0∀ x6 . x6SNoL x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x3)(∀ x5 . x5SNoR x0∀ x6 . x6SNoR x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x3)(∀ x5 . x5x4∀ x6 : ο . (∀ x7 . x7SNoL x0∀ x8 . x8SNoR x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)(∀ x7 . x7SNoR x0∀ x8 . x8SNoL x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)x6)(∀ x5 . x5SNoL x0∀ x6 . x6SNoR x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)(∀ x5 . x5SNoR x0∀ x6 . x6SNoL x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)mul_SNo x0 x1 = SNoCut x3 x4x2)x2
Known SNoCut_extSNoCut_ext : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3(∀ x4 . x4x0SNoLt x4 (SNoCut x2 x3))(∀ x4 . x4x1SNoLt (SNoCut x2 x3) x4)(∀ x4 . x4x2SNoLt x4 (SNoCut x0 x1))(∀ x4 . x4x3SNoLt (SNoCut x0 x1) x4)SNoCut x0 x1 = SNoCut x2 x3
Known mul_SNo_distrRmul_SNo_distrR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Known mul_SNo_SNoL_interpolate_impredmul_SNo_SNoL_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoL (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoL x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoR x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)x3
Known mul_SNo_SNoR_interpolate_impredmul_SNo_SNoR_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoR (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoR x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoL x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)x3
Known mul_SNo_Ltmul_SNo_Lt : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x2 x0SNoLt x3 x1SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3))
Known mul_SNo_Lemul_SNo_Le : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x2 x0SNoLe x3 x1SNoLe (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3))
Theorem mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2 (proof)

previous assets