Search for blocks/addresses/...

Proofgold Asset

asset id
bf6bbac14c828f2a370c53d821179a58905af236cc4fd4ee30c9c64909ced72a
asset hash
60b152f8aceacf81064f801add4e4602f539c06b9a87199989ad17e276f25d3b
bday / block
21756
tx
6b79c..
preasset
doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param TwoRamseyPropTwoRamseyProp : ιιιο
Param ordsuccordsucc : ιι
Known not_TwoRamseyProp_4_5_24not_TwoRamseyProp_4_5_24 : not (TwoRamseyProp 4 5 24)
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
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
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 73189.. : nat_p u24
Param add_natadd_nat : ιιι
Known 07f4e.. : add_nat 16 7 = 23
Known d8085.. : ∀ x0 x1 . nat_p x1x0ordsucc (add_nat x0 x1)
Known nat_7nat_7 : nat_p 7
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 nat_5nat_5 : nat_p 5
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_5_5_Power_4not_TwoRamseyProp_5_5_Power_4 : not (TwoRamseyProp 5 5 (prim4 4)) (proof)