Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Known not_TwoRamseyProp_4_5_24^{not_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 atleastp^atleastp : ι → ι → ο
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Param exp_nat^exp_nat : ι → ι → ι
Known db1de.. : exp_nat 2 4 = 16
Param nat_p^nat_p : ι → ο
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Known nat_4^nat_4 : nat_p 4
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 73189.. : nat_p u24
Param add_nat^add_nat : ι → ι → ι
Known 07f4e.. : add_nat 16 7 = 23
Known d8085.. : ∀ x0 x1 . nat_p x1 ⟶ x0 ∈ ordsucc (add_nat x0 x1)
Known nat_7^nat_7 : nat_p 7
Param TwoRamseyProp_atleastp : ι → ι → ι → ο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x2
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4 ⟶ atleastp x1 x0 ⟶ atleastp x3 x2 ⟶ TwoRamseyProp_atleastp x1 x3 x4
Known nat_5^nat_5 : nat_p 5
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_5_5_Power_4^{not_TwoRamseyProp_5_5_Power_4} : not (TwoRamseyProp 5 5 (prim4 4)) (proof)