Search for blocks/addresses/...

Proofgold Address

address
PUi5EKXdfg9nX8u7o5MKkEuCLR4SepLxmgL
total
0
mg
-
conjpub
-
current assets
b4bef../d6466.. bday: 4962 doc published by Pr6Pc..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param SepSep : ι(ιο) → ι
Param SNoS_SNoS_ : ιι
Param SNoLevSNoLev : ιι
Param SNoLtSNoLt : ιιο
Definition SNoLSNoL := λ x0 . {x1 ∈ SNoS_ (SNoLev x0)|SNoLt x1 x0}
Known Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0
Known SNoL_SNoS_SNoL_SNoS_ : ∀ x0 . SNoL x0SNoS_ (SNoLev x0)
Definition SNoRSNoR := λ x0 . Sep (SNoS_ (SNoLev x0)) (SNoLt x0)
Known SNoR_SNoS_SNoR_SNoS_ : ∀ x0 . SNoR x0SNoS_ (SNoLev x0)
Param SNoSNo : ιο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param add_SNoadd_SNo : ιιι
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Param binunionbinunion : ιιι
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
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Definition ordinalordinal := λ x0 . and (TransSet x0) (∀ x1 . x1x0TransSet x1)
Param SNoCutSNoCut : ιιι
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known add_SNo_eqadd_SNo_eq : ∀ x0 . SNo x0∀ x1 . SNo x1add_SNo x0 x1 = SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x3 x1|x3 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0)))
Known and5Iand5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (and (and (and x0 x1) x2) x3) x4
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Known SNoCutP_SNoCut_LSNoCutP_SNoCut_L : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2x0SNoLt x2 (SNoCut x0 x1)
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known SNoCutP_SNoCut_RSNoCutP_SNoCut_R : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2x1SNoLt (SNoCut x0 x1) x2
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SNoCutP_SNo_SNoCutSNoCutP_SNo_SNoCut : ∀ x0 x1 . SNoCutP x0 x1SNo (SNoCut x0 x1)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
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
Param binintersectbinintersect : ιιι
Param SNoEq_SNoEq_ : ιιιο
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known SNoLtESNoLtE : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1∀ x2 : ο . (∀ x3 . SNo x3SNoLev x3binintersect (SNoLev x0) (SNoLev x1)SNoEq_ (SNoLev x3) x3 x0SNoEq_ (SNoLev x3) x3 x1SNoLt x0 x3SNoLt x3 x1nIn (SNoLev x3) x0SNoLev x3x1x2)(SNoLev x0SNoLev x1SNoEq_ (SNoLev x0) x0 x1SNoLev x0x1x2)(SNoLev x1SNoLev x0SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0x2)x2
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known SNoS_I2SNoS_I2 : ∀ x0 x1 . SNo x0SNo x1SNoLev x0SNoLev x1x0SNoS_ (SNoLev x1)
Known ordinal_TransSetordinal_TransSet : ∀ x0 . ordinal x0TransSet x0
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Theorem add_SNo_prop1add_SNo_prop1 : ∀ x0 x1 . SNo x0SNo x1and (and (and (and (and (SNo (add_SNo x0 x1)) (∀ x2 . x2SNoL x0SNoLt (add_SNo x2 x1) (add_SNo x0 x1))) (∀ x2 . x2SNoR x0SNoLt (add_SNo x0 x1) (add_SNo x2 x1))) (∀ x2 . x2SNoL x1SNoLt (add_SNo x0 x2) (add_SNo x0 x1))) (∀ x2 . x2SNoR x1SNoLt (add_SNo x0 x1) (add_SNo x0 x2))) (SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0)))) (proof)
Theorem SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1) (proof)
Theorem add_SNo_Lt1add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1) (proof)
Param SNoLeSNoLe : ιιο
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Theorem add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1) (proof)
Theorem add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2) (proof)
Theorem add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2) (proof)
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Theorem add_SNo_Lt3aadd_SNo_Lt3a : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x0 x2SNoLe x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3) (proof)
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Theorem add_SNo_Lt3badd_SNo_Lt3b : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3) (proof)
Theorem add_SNo_Lt3add_SNo_Lt3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3) (proof)
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Theorem add_SNo_Le3add_SNo_Le3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x0 x2SNoLe x1 x3SNoLe (add_SNo x0 x1) (add_SNo x2 x3) (proof)
Theorem add_SNo_SNoCutPadd_SNo_SNoCutP : ∀ x0 x1 . SNo x0SNo x1SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0))) (proof)
Theorem add_SNo_SNoCutP_genadd_SNo_SNoCutP_gen : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3SNoCutP (binunion {add_SNo x4 (SNoCut x2 x3)|x4 ∈ x0} (prim5 x2 (add_SNo (SNoCut x0 x1)))) (binunion {add_SNo x4 (SNoCut x2 x3)|x4 ∈ x1} (prim5 x3 (add_SNo (SNoCut x0 x1)))) (proof)
Known binunion_combinunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known ReplEq_extReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1 = prim5 x0 x2
Theorem add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0 (proof)
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Known SNo_0SNo_0 : SNo 0
Known SNo_etaSNo_eta : ∀ x0 . SNo x0x0 = SNoCut (SNoL x0) (SNoR x0)
Known SNoR_0SNoR_0 : SNoR 0 = 0
Known Repl_EmptyRepl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known binunion_idlbinunion_idl : ∀ x0 . binunion 0 x0 = x0
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known SNoL_0SNoL_0 : SNoL 0 = 0
Theorem add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0 (proof)
Theorem add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0 (proof)
Param minus_SNominus_SNo : ιι
Known SNo_eqSNo_eq : ∀ x0 x1 . SNo x0SNo x1SNoLev x0 = SNoLev x1SNoEq_ (SNoLev x0) x0 x1x0 = x1
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
Known ordinal_Emptyordinal_Empty : ordinal 0
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Known SNoCutP_SNoCut_fstSNoCutP_SNoCut_fst : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . SNo x2(∀ x3 . x3x0SNoLt x3 x2)(∀ x3 . x3x1SNoLt x2 x3)and (SNoLev (SNoCut x0 x1)SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known minus_SNo_Lt_contraminus_SNo_Lt_contra : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1SNoLt (minus_SNo x1) (minus_SNo x0)
Known minus_SNo_Levminus_SNo_Lev : ∀ x0 . SNo x0SNoLev (minus_SNo x0) = SNoLev x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Theorem add_SNo_minus_SNo_linvadd_SNo_minus_SNo_linv : ∀ x0 . SNo x0add_SNo (minus_SNo x0) x0 = 0 (proof)
Theorem add_SNo_minus_SNo_rinvadd_SNo_minus_SNo_rinv : ∀ x0 . SNo x0add_SNo x0 (minus_SNo x0) = 0 (proof)
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 ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem add_SNo_ordinal_SNoCutPadd_SNo_ordinal_SNoCutP : ∀ x0 . ordinal x0∀ x1 . ordinal x1SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoS_ x0} (prim5 (SNoS_ x1) (add_SNo x0))) 0 (proof)
Known ordinal_SNoLordinal_SNoL : ∀ x0 . ordinal x0SNoL x0 = SNoS_ x0
Known ordinal_SNoRordinal_SNoR : ∀ x0 . ordinal x0SNoR x0 = 0
Theorem add_SNo_ordinal_eqadd_SNo_ordinal_eq : ∀ x0 . ordinal x0∀ x1 . ordinal x1add_SNo x0 x1 = SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ x0} (prim5 (SNoS_ x1) (add_SNo x0))) 0 (proof)
Known SNo_max_ordinalSNo_max_ordinal : ∀ x0 . SNo x0(∀ x1 . x1SNoS_ (SNoLev x0)SNoLt x1 x0)ordinal x0
Known SNoLt_trichotomy_orSNoLt_trichotomy_or : ∀ x0 x1 . SNo x0SNo x1or (or (SNoLt x0 x1) (x0 = x1)) (SNoLt x1 x0)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Param ordsuccordsucc : ιι
Param famunionfamunion : ι(ιι) → ι
Known SNoCutP_SNoCutSNoCutP_SNoCut : ∀ x0 x1 . SNoCutP x0 x1and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2x0SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2x1SNoLt (SNoCut x0 x1) x2)) (∀ x2 . SNo x2(∀ x3 . x3x0SNoLt x3 x2)(∀ x3 . x3x1SNoLt x2 x3)and (SNoLev (SNoCut x0 x1)SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2))
Theorem add_SNo_ordinal_ordinaladd_SNo_ordinal_ordinal : ∀ x0 . ordinal x0∀ x1 . ordinal x1ordinal (add_SNo x0 x1) (proof)
Known ordinal_indordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . ordinal x1x0 x1
Known ordinal_ordsucc_In_eqordinal_ordsucc_In_eq : ∀ x0 x1 . ordinal x0x1x0or (ordsucc x1x0) (x0 = ordsucc x1)
Known ordinal_SNoLev_max_2ordinal_SNoLev_max_2 : ∀ x0 . ordinal x0∀ x1 . SNo x1SNoLev x1ordsucc x0SNoLe x1 x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known ordinal_Subq_SNoLeordinal_Subq_SNoLe : ∀ x0 x1 . ordinal x0ordinal x1x0x1SNoLe x0 x1
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0)
Known SNoS_ISNoS_I : ∀ x0 . ordinal x0∀ x1 x2 . x2x0SNo_ x2 x1x1SNoS_ x0
Known ordinal_SNo_ordinal_SNo_ : ∀ x0 . ordinal x0SNo_ x0 x0
Theorem add_SNo_ordinal_SLadd_SNo_ordinal_SL : ∀ x0 . ordinal x0∀ x1 . ordinal x1add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1) (proof)
Theorem add_SNo_ordinal_SRadd_SNo_ordinal_SR : ∀ x0 . ordinal x0∀ x1 . ordinal x1add_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1) (proof)
Known ordinal_Heredordinal_Hered : ∀ x0 . ordinal x0∀ x1 . x1x0ordinal x1
Theorem add_SNo_ordinal_InLadd_SNo_ordinal_InL : ∀ x0 . ordinal x0∀ x1 . ordinal x1∀ x2 . x2x0add_SNo x2 x1add_SNo x0 x1 (proof)
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoCut_LeSNoCut_Le : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3(∀ x4 . x4x0SNoLt x4 (SNoCut x2 x3))(∀ x4 . x4x3SNoLt (SNoCut x0 x1) x4)SNoLe (SNoCut x0 x1) (SNoCut x2 x3)
Known SNoCutP_SNoL_SNoRSNoCutP_SNoL_SNoR : ∀ x0 . SNo x0SNoCutP (SNoL x0) (SNoR x0)
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Theorem add_SNo_SNoL_interpolateadd_SNo_SNoL_interpolate : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoL (add_SNo x0 x1)or (∀ x3 : ο . (∀ x4 . and (x4SNoL x0) (SNoLe x2 (add_SNo x4 x1))x3)x3) (∀ x3 : ο . (∀ x4 . and (x4SNoL x1) (SNoLe x2 (add_SNo x0 x4))x3)x3) (proof)
Theorem add_SNo_SNoR_interpolateadd_SNo_SNoR_interpolate : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoR (add_SNo x0 x1)or (∀ x3 : ο . (∀ x4 . and (x4SNoR x0) (SNoLe (add_SNo x4 x1) x2)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4SNoR x1) (SNoLe (add_SNo x0 x4) x2)x3)x3) (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
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
Theorem 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 (proof)
Theorem add_SNo_cancel_Ladd_SNo_cancel_L : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 x1 = add_SNo x0 x2x1 = x2 (proof)
Theorem minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0 (proof)
Theorem 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) (proof)
Param If_iIf_i : οιιι
Param mul_SNomul_SNo : ιιι
Definition div_SNodiv_SNo := λ x0 x1 . If_i (x1 = 0) 0 (prim0 (λ x2 . and (SNo x2) (mul_SNo x2 x1 = x0)))
Param SNo_pairSNo_pair : ιιι
Param CSNo_ReCSNo_Re : ιι
Param CSNo_ImCSNo_Im : ιι
Definition minus_CSNominus_CSNo := λ x0 . SNo_pair (minus_SNo (CSNo_Re x0)) (minus_SNo (CSNo_Im x0))
Param CSNoCSNo : ιο
Known CSNo_ICSNo_I : ∀ x0 x1 . SNo x0SNo x1CSNo (SNo_pair x0 x1)
Known CSNo_ReRCSNo_ReR : ∀ x0 . CSNo x0SNo (CSNo_Re x0)
Known CSNo_ImRCSNo_ImR : ∀ x0 . CSNo x0SNo (CSNo_Im x0)
Theorem CSNo_minus_CSNoCSNo_minus_CSNo : ∀ x0 . CSNo x0CSNo (minus_CSNo x0) (proof)
Known SNo_pair_0SNo_pair_0 : ∀ x0 . SNo_pair x0 0 = x0
Known CSNo_Re2CSNo_Re2 : ∀ x0 x1 . SNo x0SNo x1CSNo_Re (SNo_pair x0 x1) = x0
Theorem SNo_ReSNo_Re : ∀ x0 . SNo x0CSNo_Re x0 = x0 (proof)
Known CSNo_Im2CSNo_Im2 : ∀ x0 x1 . SNo x0SNo x1CSNo_Im (SNo_pair x0 x1) = x1
Theorem SNo_ImSNo_Im : ∀ x0 . SNo x0CSNo_Im x0 = 0 (proof)
Theorem Re_0Re_0 : CSNo_Re 0 = 0 (proof)
Theorem Im_0Im_0 : CSNo_Im 0 = 0 (proof)
Known SNo_1SNo_1 : SNo 1
Theorem Re_1Re_1 : CSNo_Re 1 = 1 (proof)
Theorem Im_1Im_1 : CSNo_Im 1 = 0 (proof)
Definition Complex_iComplex_i := SNo_pair 0 1
Theorem Re_iRe_i : CSNo_Re Complex_i = 0 (proof)
Theorem Im_iIm_i : CSNo_Im Complex_i = 1 (proof)
Definition add_CSNoadd_CSNo := λ x0 x1 . SNo_pair (add_SNo (CSNo_Re x0) (CSNo_Re x1)) (add_SNo (CSNo_Im x0) (CSNo_Im x1))
Theorem add_SNo_add_CSNoadd_SNo_add_CSNo : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_CSNo x0 x1 (proof)
Theorem CSNo_add_CSNoCSNo_add_CSNo : ∀ x0 x1 . CSNo x0CSNo x1CSNo (add_CSNo x0 x1) (proof)
Known CSNo_ReImCSNo_ReIm : ∀ x0 . CSNo x0x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0)
Theorem add_CSNo_0Ladd_CSNo_0L : ∀ x0 . CSNo x0add_CSNo 0 x0 = x0 (proof)
Theorem add_CSNo_0Radd_CSNo_0R : ∀ x0 . CSNo x0add_CSNo x0 0 = x0 (proof)
Theorem add_CSNo_minus_CSNo_linvadd_CSNo_minus_CSNo_linv : ∀ x0 . CSNo x0add_CSNo (minus_CSNo x0) x0 = 0 (proof)
Theorem add_CSNo_minus_CSNo_rinvadd_CSNo_minus_CSNo_rinv : ∀ x0 . CSNo x0add_CSNo x0 (minus_CSNo x0) = 0 (proof)
Theorem minus_SNo_minus_CSNominus_SNo_minus_CSNo : ∀ x0 . SNo x0minus_SNo x0 = minus_CSNo x0 (proof)
Param mul_CSNomul_CSNo : ιιι
Definition div_CSNodiv_CSNo := λ x0 x1 . If_i (x1 = 0) 0 (prim0 (λ x2 . and (CSNo x2) (mul_CSNo x2 x1 = x0)))

previous assets