Search for blocks/addresses/...

Proofgold Address

address
PUdwfK2KyQMkBahEABSvvUUFtAbFA4h6SE9
total
0
mg
-
conjpub
-
current assets
c8961../48c9f.. bday: 31380 doc published by Pr4zB..
Param nat_pnat_p : ιο
Param equipequip : ιιο
Param ordsuccordsucc : ιι
Param ordinalordinal : ιο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param binunionbinunion : ιιι
Param SingSing : ιι
Param atleastpatleastp : ιιο
Known 2ec5a.. : ∀ x0 . nat_p x0∀ x1 . atleastp (ordsucc x0) x1(∀ x2 . x2x1ordinal x2)∀ x2 : ο . (∀ x3 x4 . equip x0 x3x4x1x3x1x3x4x2)x2
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param omegaomega : ι
Definition finitefinite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (equip x0 x2)x1)x1
Known 1b508.. : ∀ x0 x1 . finite x0atleastp x1 x0x0x1x0 = x1
Known adjoin_finiteadjoin_finite : ∀ x0 x1 . finite x0finite (binunion x0 (Sing x1))
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Param add_natadd_nat : ιιι
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0nat_0 : nat_p 0
Param setsumsetsum : ιιι
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3)
Known nat_1nat_1 : nat_p 1
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known d778e.. : ∀ x0 x1 x2 x3 . equip x0 x2equip x1 x3(∀ x4 . x4x0nIn x4 x1)equip (binunion x0 x1) (setsum x2 x3)
Definition u1 := 1
Known 5169f..equip_Sing_1 : ∀ x0 . equip (Sing x0) u1
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Theorem be1cd.. : ∀ x0 . nat_p x0∀ x1 . equip (ordsucc x0) x1(∀ x2 . x2x1ordinal x2)∀ x2 : ο . (∀ x3 x4 . equip x0 x3x4x1x3x1x3x4x1 = binunion x3 (Sing x4)x2)x2 (proof)
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Theorem 480b2.. : add_nat u3 u1 = u4 (proof)
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Param u13 : ι
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known nat_17nat_17 : nat_p u17
Known e57ea.. : u11u17
Theorem b4ae4.. : u11u17 (proof)
Known nat_8nat_8 : nat_p 8
Known In_6_8In_6_8 : 68
Theorem bd770.. : u6u8 (proof)
Known In_7_8In_7_8 : 78
Theorem 021ac.. : u7u8 (proof)
Param setminussetminus : ιιι
Definition u12 := ordsucc u11
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known 660da.. : ∀ x0 . x0u16∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 u13x1 u14x1 u15x1 x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known 46814.. : 012
Known 2b77d.. : 112
Known 7c2ac.. : 212
Known 2f583.. : 312
Known e4fc0.. : 412
Known 04716.. : 512
Known fbe39.. : 612
Known 35d73.. : 712
Known 5196c.. : 812
Known 4fa36.. : 912
Known 42552.. : 1012
Known fee2e.. : 1112
Theorem ee881.. : ∀ x0 . x0setminus u16 u12∀ x1 : ι → ο . x1 u12x1 u13x1 u14x1 u15x1 x0 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Theorem 4fd0a.. : ∀ x0 . x0setminus u17 u12∀ x1 : ι → ο . x1 u12x1 u13x1 u14x1 u15x1 u16x1 x0 (proof)
Definition u18 := ordsucc u17
Theorem 7618f.. : ∀ x0 . x0setminus u18 u12∀ x1 : ι → ο . x1 u12x1 u13x1 u14x1 u15x1 u16x1 u17x1 x0 (proof)
Known 866c8.. : ∀ x0 . x0u12∀ x1 : ι → ο . x1 0x1 u1x1 u2x1 u3x1 u4x1 u5x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 x0
Known In_0_6In_0_6 : 06
Known In_1_6In_1_6 : 16
Known In_2_6In_2_6 : 26
Known In_3_6In_3_6 : 36
Known In_4_6In_4_6 : 46
Known In_5_6In_5_6 : 56
Theorem 49949.. : ∀ x0 . x0setminus u12 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 x0 (proof)
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Theorem 823c9.. : ∀ x0 . x0setminus u16 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 u13x1 u14x1 u15x1 x0 (proof)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem 0420f.. : ∀ x0 . x0setminus u15 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 u13x1 u14x1 x0 (proof)
Theorem a1137.. : ∀ x0 . x0setminus u14 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 u13x1 x0 (proof)
Theorem 5786d.. : ∀ x0 . x0setminus u13 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 u11x1 u12x1 x0 (proof)
Theorem 090fa.. : ∀ x0 . x0setminus u11 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 u10x1 x0 (proof)
Theorem 86222.. : ∀ x0 . x0setminus u10 u6∀ x1 : ι → ο . x1 u6x1 u7x1 u8x1 u9x1 x0 (proof)
Theorem 27661.. : ∀ x0 . x0setminus u12 u10∀ x1 : ι → ο . x1 u10x1 u11x1 x0 (proof)
Theorem 853d4.. : ∀ x0 . x0setminus u16 u10∀ x1 : ι → ο . x1 u10x1 u11x1 u12x1 u13x1 u14x1 u15x1 x0 (proof)
Theorem 332b1.. : ∀ x0 . x0setminus u15 u10∀ x1 : ι → ο . x1 u10x1 u11x1 u12x1 u13x1 u14x1 x0 (proof)
Theorem 98cac.. : ∀ x0 . x0setminus u14 u10∀ x1 : ι → ο . x1 u10x1 u11x1 u12x1 u13x1 x0 (proof)
Theorem fc2d4.. : ∀ x0 . x0setminus u13 u10∀ x1 : ι → ο . x1 u10x1 u11x1 u12x1 x0 (proof)
Known In_0_8In_0_8 : 08
Known In_1_8In_1_8 : 18
Known In_2_8In_2_8 : 28
Known In_3_8In_3_8 : 38
Known In_4_8In_4_8 : 48
Known In_5_8In_5_8 : 58
Theorem bf41f.. : ∀ x0 . x0setminus u12 u8∀ x1 : ι → ο . x1 u8x1 u9x1 u10x1 u11x1 x0 (proof)

previous assets