Proofgold Address

Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Known TwoRamseyProp_3_4_9^{TwoRamseyProp_3_4_9} : TwoRamseyProp 3 4 9
Param add_nat^add_nat : ι → ι → ι
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
Param nat_p^nat_p : ι → ο
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 6b0ad.. : add_nat u9 u1 = u10 (proof)
Definition u11 := ordsucc u10
Known nat_1^nat_1 : nat_p 1
Theorem f731c.. : add_nat u9 u2 = u11 (proof)
Definition u12 := ordsucc u11
Known nat_2^nat_2 : nat_p 2
Theorem 79b65.. : add_nat u9 u3 = u12 (proof)
Definition u13 := ordsucc u12
Known nat_3^nat_3 : nat_p 3
Theorem d9e97.. : add_nat u9 u4 = u13 (proof)
Definition u14 := ordsucc u13
Known nat_4^nat_4 : nat_p 4
Theorem 8ae56.. : add_nat u9 u5 = u14 (proof)
Definition u15 := ordsucc u14
Param TwoRamseyProp_atleastp : ι → ι → ι → ο
Known 97c7e.. : ∀ x0 x1 x2 x3 . nat_p x2 ⟶ nat_p x3 ⟶ TwoRamseyProp_atleastp (ordsucc x0) x1 x2 ⟶ TwoRamseyProp_atleastp x0 (ordsucc x1) x3 ⟶ TwoRamseyProp (ordsucc x0) (ordsucc x1) (ordsucc (add_nat x2 x3))
Known nat_9^nat_9 : nat_p 9
Known nat_5^nat_5 : nat_p 5
Param atleastp^atleastp : ι → ι → ο
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 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem TwoRamseyProp_u3_u5_u15 : TwoRamseyProp u3 u5 u15 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Definition u16 := ordsucc u15
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Param Subq^Subq : ι → ι → ο
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Param exp_nat^exp_nat : ι → ι → ι
Known db1de.. : exp_nat 2 4 = 16
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Theorem TwoRamseyProp_3_5_Power_4^{TwoRamseyProp_3_5_Power_4} : TwoRamseyProp 3 5 (prim4 4) (proof)