Proofgold Asset

Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Param add_nat^add_nat : ι → ι → ι
Known 816bd.. : add_nat 16 8 = 24
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known nat_16^nat_16 : nat_p 16
Known nat_8^nat_8 : nat_p 8
Theorem 73189.. : nat_p 24 (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known 6ba1d.. : add_nat 24 7 = 31
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_7^nat_7 : nat_p 7
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 TwoRamseyProp_3_6_24 : TwoRamseyProp 3 6 24
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem TwoRamseyProp_3_7_32 : TwoRamseyProp 3 7 32 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
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 e089c.. : exp_nat 2 5 = 32
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Known nat_5^nat_5 : nat_p 5
Theorem TwoRamseyProp_3_7_Power_5^{TwoRamseyProp_3_7_Power_5} : TwoRamseyProp 3 7 (prim4 5) (proof)
Param Subq^Subq : ι → ι → ο
Known 697c6.. : ∀ x0 x1 x2 x3 . x2 ⊆ x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known 78a3e.. : ∀ x0 . prim4 x0 ⊆ prim4 (ordsucc x0)
Theorem TwoRamseyProp_3_7_Power_6^{TwoRamseyProp_3_7_Power_6} : TwoRamseyProp 3 7 (prim4 6) (proof)
Theorem TwoRamseyProp_3_7_Power_7^{TwoRamseyProp_3_7_Power_7} : TwoRamseyProp 3 7 (prim4 7) (proof)
Theorem TwoRamseyProp_3_7_Power_8^{TwoRamseyProp_3_7_Power_8} : TwoRamseyProp 3 7 (prim4 8) (proof)