Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Known not_TwoRamseyProp_4_4_17^{not_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 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 nat_17^nat_17 : nat_p 17
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc 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 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 atleastp_ref : ∀ x0 . atleastp x0 x0
Known nat_5^nat_5 : nat_p 5
Known In_4_5^In_4_5 : 4 ∈ 5
Theorem 5b30a..^{not_TwoRamseyProp_4_5_Power_4} : not (TwoRamseyProp 4 5 (prim4 4)) (proof)