Search for blocks/addresses/...

Proofgold Address

address
PUYvD7FxdYJQdXj9WdZtFSQrNEmszzSWm5m
total
0
mg
-
conjpub
-
current assets
7f67c../2c9d7.. bday: 19045 doc published by Pr4zB..
Param ordsuccordsucc : ιι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
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
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition u16 := ordsucc u15
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param binintersectbinintersect : ιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param add_natadd_nat : ιιι
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Param nat_pnat_p : ιο
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Known nat_5nat_5 : nat_p 5
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Definition nInnIn := λ x0 x1 . not (x0x1)
Param If_iIf_i : οιιι
Known In_3_5In_3_5 : 35
Known In_4_5In_4_5 : 45
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_11nat_11 : nat_p 11
Known add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Known nat_4nat_4 : nat_p 4
Known 62dd3.. : add_nat 11 4 = 15
Known nat_3nat_3 : nat_p 3
Known 336f0.. : add_nat 11 3 = 14
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Known binintersectIbinintersectI : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1
Known In_0_5In_0_5 : 05
Known add_nat_0Ladd_nat_0L : ∀ x0 . nat_p x0add_nat 0 x0 = x0
Known nat_12nat_12 : nat_p 12
Known In_1_5In_1_5 : 15
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known nat_0nat_0 : nat_p 0
Known In_2_5In_2_5 : 25
Known nat_1nat_1 : nat_p 1
Known nat_2nat_2 : nat_p 2
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known cases_9cases_9 : ∀ x0 . x09∀ x1 : ι → ο . x1 0x1 1x1 2x1 3x1 4x1 5x1 6x1 7x1 8x1 x0
Theorem 1c7b4.. : ∀ x0 : ι → ι → ο . x0 0 u2x0 u4 u6x0 u1 u12x0 u5 u12x0 u8 u12x0 u9 u12x0 u3 u13x0 u7 u13x0 u10 u13x0 u2 u14x0 u6 u14x0 u11 u14x0 0 u15x0 u4 u15∀ x1 . x1u16atleastp u6 x1u12x1u13x1u14x1(∀ x2 . x2x1∀ x3 . x3x1not (x0 x2 x3))False (proof)

previous assets