Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../315bb..
PURP9../ceebc..
vout
PrCit../c9a62.. 6.20 bars
TMcQa../6248d.. negprop ownership controlledby Pr4zB.. upto 0
TMVvu../48bba.. negprop ownership controlledby Pr4zB.. upto 0
TMbbq../c678c.. negprop ownership controlledby Pr4zB.. upto 0
TMKNm../0d1c4.. negprop ownership controlledby Pr4zB.. upto 0
TMcPX../31986.. negprop ownership controlledby Pr4zB.. upto 0
TMaVn../51174.. negprop ownership controlledby Pr4zB.. upto 0
TMcHx../c7cc9.. negprop ownership controlledby Pr4zB.. upto 0
TMZjp../288d9.. negprop ownership controlledby Pr4zB.. upto 0
TMdo5../76aa0.. negprop ownership controlledby Pr4zB.. upto 0
TMKSZ../80e3c.. negprop ownership controlledby Pr4zB.. upto 0
TMEgA../f2929.. negprop ownership controlledby Pr4zB.. upto 0
TMcUC../18ee2.. negprop ownership controlledby Pr4zB.. upto 0
TMUvX../0fef5.. negprop ownership controlledby Pr4zB.. upto 0
TMTVq../3704f.. negprop ownership controlledby Pr4zB.. upto 0
TMEvC../106bc.. negprop ownership controlledby Pr4zB.. upto 0
TMaZ4../fb156.. ownership of c642e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdkM../c70b2.. ownership of 045e6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYNo../f788c.. ownership of 3ce96.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMS2J../e4ca2.. ownership of 1e8ea.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcca../6564d.. ownership of f4df6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZK1../32664.. ownership of 3b881.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHp7../9282e.. ownership of c6b25.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRaM../fe2f1.. ownership of 9229f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFbY../79f4b.. ownership of c0836.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTHg../0e69e.. ownership of 5bd10.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMahh../6f169.. ownership of 5914c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNBn../37791.. ownership of 63021.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQtV../01852.. ownership of fa29b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJuK../dcfe4.. ownership of 219cd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMReA../bd157.. ownership of a1968.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLEA../70f2d.. ownership of d0d0d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGsp../f70e1.. ownership of f5ebc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHqt../0b8f6.. ownership of 27738.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFWh../b0104.. ownership of a1e0f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXnW../4937a.. ownership of c5022.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUYs../7693f.. ownership of f990b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNqD../cc928.. ownership of a44fd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEzz../c9ba7.. ownership of b6366.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPwa../7b162.. ownership of 7c4c3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRgs../2c1df.. ownership of 1d99f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRCn../093c4.. ownership of 0b06f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLyv../5cee3.. ownership of 4618e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa12../a4658.. ownership of 47c91.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcUH../78480.. ownership of 50032.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQ62../b2bbb.. ownership of a8735.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUd6h../b26b4.. doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param atleastpatleastp : ιιο
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5x3 x5 x4)or (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x0 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)x3 x6 x7))x4)x4) (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x1 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)not (x3 x6 x7)))x4)x4)
Param ordsuccordsucc : ιι
Known f03aa.. : ∀ x0 . atleastp 3 x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0(x2 = x3∀ x5 : ο . x5)(x2 = x4∀ x5 : ο . x5)(x3 = x4∀ x5 : ο . x5)x1)x1
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Param invinv : ι(ιι) → ιι
Param nat_pnat_p : ιο
Known PigeonHole_natPigeonHole_nat : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2ordsucc x0x1 x2x0)not (∀ x2 . x2ordsucc x0∀ x3 . x3ordsucc x0x1 x2 = x1 x3x2 = x3)
Known nat_3nat_3 : nat_p 3
Known surj_inv_injsurj_inv_inj : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)inj x1 x0 (inv x0 x2)
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Definition nInnIn := λ x0 x1 . not (x0x1)
Known FalseEFalseE : False∀ x0 : ο . x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known In_2_3In_2_3 : 23
Known tuple_3_2_eqtuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Known In_1_3In_1_3 : 13
Known tuple_3_1_eqtuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known In_0_3In_0_3 : 03
Known tuple_3_0_eqtuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known In_0_4In_0_4 : 04
Param binunionbinunion : ιιι
Param SepSep : ι(ιο) → ι
Param setminussetminus : ιιι
Param SingSing : ιι
Param bijbij : ιι(ιι) → ο
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Known a6047.. : ∀ x0 . x0prim4 3∀ x1 . x1prim4 3(∀ x2 . x2x0∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x53) (∀ x6 : ο . (∀ x7 . and (x73) (and (and (x5 = x7∀ x8 : ο . x8) (x5x2 = x5x3)) (x7x2 = x7x3))x6)x6)x4)x4)∀ x2 : ο . (atleastp x0 1x2)(atleastp x1 1x2)(equip 2 x0equip 2 x1x2)x2
Known 89205.. : ∀ x0 x1 . (∀ x2 . x2x0nIn x2 x1)atleastp 6 (binunion x0 x1)atleastp x0 1atleastp x1 (prim4 2)False
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known binunion_combinunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Known nat_5nat_5 : nat_p 5
Param setsumsetsum : ιιι
Known 385ef.. : ∀ x0 x1 x2 x3 . atleastp x0 x2atleastp x1 x3(∀ x4 . x4x0nIn x4 x1)atleastp (binunion x0 x1) (setsum x2 x3)
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known 5b991.. : equip 4 (setsum 2 2)
Known nat_In_atleastp : ∀ x0 . nat_p x0∀ x1 . x1x0atleastp x1 x0
Known In_4_5In_4_5 : 45
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Known bijIbijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x1)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)(∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)bij x0 x1 x2
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known dfb49.. : ∀ x0 x1 . x1prim4 (ordsucc x0)(∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)∀ x4 : ο . (∀ x5 . and (x5ordsucc x0) (x5x2 = x5x3)x4)x4)atleastp x1 (prim4 x0)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
Known SingISingI : ∀ x0 . x0Sing x0
Known Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Theorem not_TwoRamseyProp_atleast_3_6_Power_4 : not (TwoRamseyProp_atleastp 3 6 (prim4 4)) (proof)
Param TwoRamseyPropTwoRamseyProp : ιιιο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4atleastp x1 x0atleastp x3 x2TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem 4618e..not_TwoRamseyProp_3_6_Power_4 : not (TwoRamseyProp 3 6 (prim4 4)) (proof)
Known nat_7nat_7 : nat_p 7
Known In_6_7In_6_7 : 67
Theorem 1d99f..not_TwoRamseyProp_3_7_Power_4 : not (TwoRamseyProp 3 7 (prim4 4)) (proof)
Known nat_8nat_8 : nat_p 8
Known In_6_8In_6_8 : 68
Theorem b6366..not_TwoRamseyProp_3_8_Power_4 : not (TwoRamseyProp 3 8 (prim4 4)) (proof)
Known nat_9nat_9 : nat_p 9
Known In_6_9In_6_9 : 69
Theorem f990b..not_TwoRamseyProp_3_9_Power_4 : not (TwoRamseyProp 3 9 (prim4 4)) (proof)
Known nat_10nat_10 : nat_p 10
Known 1beb5.. : 610
Theorem a1e0f..not_TwoRamseyProp_3_10_Power_4 : not (TwoRamseyProp 3 10 (prim4 4)) (proof)
Known nat_4nat_4 : nat_p 4
Known In_3_4In_3_4 : 34
Theorem f5ebc..not_TwoRamseyProp_4_6_Power_4 : not (TwoRamseyProp 4 6 (prim4 4)) (proof)
Theorem a1968..not_TwoRamseyProp_4_7_Power_4 : not (TwoRamseyProp 4 7 (prim4 4)) (proof)
Theorem fa29b..not_TwoRamseyProp_4_8_Power_4 : not (TwoRamseyProp 4 8 (prim4 4)) (proof)
Theorem 5914c..not_TwoRamseyProp_4_9_Power_4 : not (TwoRamseyProp 4 9 (prim4 4)) (proof)
Known In_3_5In_3_5 : 35
Theorem c0836..not_TwoRamseyProp_5_6_Power_4 : not (TwoRamseyProp 5 6 (prim4 4)) (proof)
Theorem c6b25..not_TwoRamseyProp_5_7_Power_4 : not (TwoRamseyProp 5 7 (prim4 4)) (proof)
Theorem f4df6..not_TwoRamseyProp_5_8_Power_4 : not (TwoRamseyProp 5 8 (prim4 4)) (proof)
Known nat_6nat_6 : nat_p 6
Known In_3_6In_3_6 : 36
Theorem 3ce96..not_TwoRamseyProp_6_6_Power_4 : not (TwoRamseyProp 6 6 (prim4 4)) (proof)
Theorem c642e..not_TwoRamseyProp_6_7_Power_4 : not (TwoRamseyProp 6 7 (prim4 4)) (proof)