Search for blocks/addresses/...

Proofgold Asset

asset id
a62bd21a0ab14bbcd0127e7278d2034c57eac600c1de5284cc52198f4d942aef
asset hash
f47713b676614d271ceb6bdc7b5f69cfd389e5b357d7b994e5d8409a7f4b838e
bday / block
4981
tx
0d8c8..
preasset
doc published by Pr6Pc..
Param famunionfamunion : ι(ιι) → ι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem famunion_Emptyfamunion_Empty : ∀ x0 : ι → ι . famunion 0 x0 = 0 (proof)
Param SNoSNo : ιο
Param andand : οοο
Param SNoLtSNoLt : ιιο
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem SNoCutP_L_0SNoCutP_L_0 : ∀ x0 . (∀ x1 . x1x0SNo x1)SNoCutP x0 0 (proof)
Theorem SNoCutP_0_RSNoCutP_0_R : ∀ x0 . (∀ x1 . x1x0SNo x1)SNoCutP 0 x0 (proof)
Theorem SNoCutP_0_0SNoCutP_0_0 : SNoCutP 0 0 (proof)
Param SNoCutSNoCut : ιιι
Param SNoLevSNoLev : ιι
Param ordsuccordsucc : ιι
Param binunionbinunion : ιιι
Param SNoEq_SNoEq_ : ιιιο
Known SNoCutP_SNoCut_impredSNoCutP_SNoCut_impred : ∀ x0 x1 . SNoCutP x0 x1∀ x2 : ο . (SNo (SNoCut x0 x1)SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3))))(∀ x3 . x3x0SNoLt x3 (SNoCut x0 x1))(∀ x3 . x3x1SNoLt (SNoCut x0 x1) x3)(∀ x3 . SNo x3(∀ x4 . x4x0SNoLt x4 x3)(∀ x4 . x4x1SNoLt x3 x4)and (SNoLev (SNoCut x0 x1)SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3))x2)x2
Known binunion_idlbinunion_idl : ∀ x0 . binunion 0 x0 = x0
Known SNo_eqSNo_eq : ∀ x0 x1 . SNo x0SNo x1SNoLev x0 = SNoLev x1SNoEq_ (SNoLev x0) x0 x1x0 = x1
Known SNo_0SNo_0 : SNo 0
Known SNoLev_0SNoLev_0 : SNoLev 0 = 0
Param iffiff : οοο
Known SNoEq_ISNoEq_I : ∀ x0 x1 x2 . (∀ x3 . x3x0iff (x3x1) (x3x2))SNoEq_ x0 x1 x2
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Theorem SNoCut_0_0SNoCut_0_0 : SNoCut 0 0 = 0 (proof)
Param SNoLSNoL : ιι
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Known SNo_1SNo_1 : SNo 1
Param ordinalordinal : ιο
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
Param nat_pnat_p : ιο
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known nat_1nat_1 : nat_p 1
Known In_0_1In_0_1 : 01
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Theorem SNoL_1SNoL_1 : SNoL 1 = 1 (proof)
Param SNoRSNoR : ιι
Known ordinal_SNoRordinal_SNoR : ∀ x0 . ordinal x0SNoR x0 = 0
Theorem SNoR_1SNoR_1 : SNoR 1 = 0 (proof)
Param add_SNoadd_SNo : ιιι
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Theorem SNo_add_SNo_3SNo_add_SNo_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (add_SNo x0 (add_SNo x1 x2)) (proof)
Param minus_SNominus_SNo : ιι
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Theorem SNo_add_SNo_3cSNo_add_SNo_3c : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (proof)
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)
Theorem minus_add_SNo_distr_3minus_add_SNo_distr_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2minus_SNo (add_SNo x0 (add_SNo x1 x2)) = add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (minus_SNo x2)) (proof)
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_Lt1add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)
Theorem add_SNo_3_3_3_Lt1add_SNo_3_3_3_Lt1 : ∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4SNoLt (add_SNo x0 x1) (add_SNo x2 x3)SNoLt (add_SNo x0 (add_SNo x1 x4)) (add_SNo x2 (add_SNo x3 x4)) (proof)
Known add_SNo_rotate_3_1add_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Theorem add_SNo_3_2_3_Lt1add_SNo_3_2_3_Lt1 : ∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4SNoLt (add_SNo x1 x0) (add_SNo x2 x3)SNoLt (add_SNo x0 (add_SNo x4 x1)) (add_SNo x2 (add_SNo x3 x4)) (proof)
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 add_SNo_minus_SNo_linvadd_SNo_minus_SNo_linv : ∀ x0 . SNo x0add_SNo (minus_SNo x0) x0 = 0
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Theorem add_SNo_minus_Lt1badd_SNo_minus_Lt1b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 (add_SNo x2 x1)SNoLt (add_SNo x0 (minus_SNo x1)) x2 (proof)
Theorem add_SNo_minus_Lt2badd_SNo_minus_Lt2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x2 x1) x0SNoLt x2 (add_SNo x0 (minus_SNo x1)) (proof)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Theorem add_SNo_minus_Lt12b3add_SNo_minus_Lt12b3 : ∀ x0 x1 x2 x3 x4 x5 . SNo x0SNo x1SNo x2SNo x3SNo x4SNo x5SNoLt (add_SNo x0 (add_SNo x1 x5)) (add_SNo x3 (add_SNo x4 x2))SNoLt (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (add_SNo x3 (add_SNo x4 (minus_SNo x5))) (proof)
Param mul_SNomul_SNo : ιιι
Known mul_SNo_prop_1mul_SNo_prop_1 : ∀ x0 . SNo x0∀ x1 . SNo x1∀ x2 : ο . (SNo (mul_SNo x0 x1)(∀ x3 . x3SNoL x0∀ x4 . x4SNoL x1SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)))(∀ x3 . x3SNoR x0∀ x4 . x4SNoR x1SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)))(∀ x3 . x3SNoL x0∀ x4 . x4SNoR x1SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)))(∀ x3 . x3SNoR x0∀ x4 . x4SNoL x1SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)))x2)x2
Theorem SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1) (proof)
Theorem SNo_mul_SNo_lemSNo_mul_SNo_lem : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNo (add_SNo (mul_SNo x2 x1) (add_SNo (mul_SNo x0 x3) (minus_SNo (mul_SNo x2 x3)))) (proof)
Known mul_SNo_eq_2mul_SNo_eq_2 : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (∀ 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 SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Theorem 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 (proof)
Theorem mul_SNo_Subq_lemmul_SNo_Subq_lem : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . x8x6∀ x9 : ο . (∀ x10 . x10x2∀ x11 . x11x3x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11)))x9)(∀ x10 . x10x4∀ x11 . x11x5x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11)))x9)x9)(∀ x8 . x8x2∀ x9 . x9x3add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9)))x7)(∀ x8 . x8x4∀ x9 . x9x5add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9)))x7)x6x7 (proof)
Known SNoR_0SNoR_0 : SNoR 0 = 0
Known SNoL_0SNoL_0 : SNoL 0 = 0
Theorem mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0 (proof)
Param SNoS_SNoS_ : ιι
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Known SNo_etaSNo_eta : ∀ x0 . SNo x0x0 = SNoCut (SNoL x0) (SNoR x0)
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 SNoCutP_SNoL_SNoRSNoCutP_SNoL_SNoR : ∀ x0 . SNo x0SNoCutP (SNoL x0) (SNoR x0)
Known SNoCutP_SNoCut_LSNoCutP_SNoCut_L : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2x0SNoLt x2 (SNoCut x0 x1)
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known SNoL_SNoSSNoL_SNoS : ∀ x0 . SNo x0∀ x1 . x1SNoL x0x1SNoS_ (SNoLev x0)
Known SNoCutP_SNoCut_RSNoCutP_SNoCut_R : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2x1SNoLt (SNoCut x0 x1) x2
Known SNoR_SNoSSNoR_SNoS : ∀ x0 . SNo x0∀ x1 . x1SNoR x0x1SNoS_ (SNoLev x0)
Theorem mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0 (proof)
Known SNoLev_ind2SNoLev_ind2 : ∀ x0 : ι → ι → ο . (∀ x1 x2 . SNo x1SNo x2(∀ x3 . x3SNoS_ (SNoLev x1)x0 x3 x2)(∀ x3 . x3SNoS_ (SNoLev x2)x0 x1 x3)(∀ x3 . x3SNoS_ (SNoLev x1)∀ x4 . x4SNoS_ (SNoLev x2)x0 x3 x4)x0 x1 x2)∀ x1 x2 . SNo x1SNo x2x0 x1 x2
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)
Theorem mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0 (proof)
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Known minus_SNo_Levminus_SNo_Lev : ∀ x0 . SNo x0SNoLev (minus_SNo x0) = SNoLev x0
Known minus_SNo_Lt_contra2minus_SNo_Lt_contra2 : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 (minus_SNo x1)SNoLt x1 (minus_SNo x0)
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known minus_SNo_Lt_contraminus_SNo_Lt_contra : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1SNoLt (minus_SNo x1) (minus_SNo x0)
Known minus_SNoCut_eqminus_SNoCut_eq : ∀ x0 x1 . SNoCutP x0 x1minus_SNo (SNoCut x0 x1) = SNoCut (prim5 x1 minus_SNo) (prim5 x0 minus_SNo)
Theorem mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1) (proof)