Search for blocks/addresses/...

Proofgold Asset

asset id
481edc0d6b5a7bbd3f1f7d77f5c9cb0ef50a8e31550fec7186fe06b1cbcea91b
asset hash
634804cc88bc60d22ee988001c5cc789c5437e0c5b502a50936a4992c1c69476
bday / block
19279
tx
e68a5..
preasset
doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param TwoRamseyPropTwoRamseyProp : ιιιο
Param ordsuccordsucc : ιι
Known not_TwoRamseyProp_4_4_17not_TwoRamseyProp_4_4_17 : not (TwoRamseyProp 4 4 17)
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 u16 := ordsucc u15
Definition u17 := ordsucc u16
Param atleastpatleastp : ιιο
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3TwoRamseyProp x0 x1 x2TwoRamseyProp x0 x1 x3
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Param equipequip : ιιο
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Param exp_natexp_nat : ιιι
Known db1de.. : exp_nat 2 4 = 16
Param nat_pnat_p : ιο
Known 293d3.. : ∀ x0 . nat_p x0equip (prim4 x0) (exp_nat 2 x0)
Known nat_4nat_4 : nat_p 4
Known nat_In_atleastp : ∀ x0 . nat_p x0∀ x1 . x1x0atleastp x1 x0
Known nat_17nat_17 : nat_p 17
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Theorem 485cd..not_TwoRamseyProp_4_4_Power_4 : not (TwoRamseyProp 4 4 (prim4 4)) (proof)
Param TwoRamseyProp_atleastp : ιιιο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2TwoRamseyProp x0 x1 x2
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
Known nat_5nat_5 : nat_p 5
Known In_4_5In_4_5 : 45
Theorem 5b30a..not_TwoRamseyProp_4_5_Power_4 : not (TwoRamseyProp 4 5 (prim4 4)) (proof)