Proofgold Address

Param ordsucc^ordsucc : ι → ι
Definition ChurchNum_ii_6 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 x1)))))
Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . x0 (x0 x1)
Definition ChurchNum_ii_2 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 x1)
Definition ChurchNum_ii_3 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 x1))
Known 9ba2f.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_3 ChurchNum2 x0 x2)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 7df32.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_2 ChurchNum2 x0 x2)
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem ac394.. : 51 ∈ ChurchNum_ii_6 ChurchNum2 ordsucc 0 (proof)
Param add_nat^add_nat : ι → ι → ι
Param nat_p^nat_p : ι → ο
Known 69b84.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_3 ChurchNum2 x0 x3) = ChurchNum_ii_3 ChurchNum2 x0 (x2 x3)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_1^nat_1 : nat_p 1
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem d3ec1.. : add_nat 41 9 = 50 (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
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))
Definition ChurchNum_ii_5 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 x1))))
Known 9821b.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_5 ChurchNum2 x0 x2)
Known nat_9^nat_9 : nat_p 9
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_8_41 : TwoRamseyProp 3 8 41
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem TwoRamseyProp_3_9_51 : TwoRamseyProp 3 9 51 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Param exp_nat^exp_nat : ι → ι → ι
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known b3a97.. : exp_nat 2 6 = ChurchNum_ii_6 ChurchNum2 ordsucc 0
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 5a366.. : nat_p 64
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
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Known nat_6^nat_6 : nat_p 6
Theorem TwoRamseyProp_3_9_Power_6^{TwoRamseyProp_3_9_Power_6} : TwoRamseyProp 3 9 (prim4 6) (proof)
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_9_Power_7^{TwoRamseyProp_3_9_Power_7} : TwoRamseyProp 3 9 (prim4 7) (proof)
Theorem TwoRamseyProp_3_9_Power_8^{TwoRamseyProp_3_9_Power_8} : TwoRamseyProp 3 9 (prim4 8) (proof)
Definition ChurchNum_ii_4 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 x1)))
Known 3ae46.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_4 ChurchNum2 x0 x2)
Known nat_3^nat_3 : nat_p 3
Theorem 81538.. : nat_p 51 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem ccce4.. : add_nat 51 10 = 61 (proof)
Theorem a1a2d.. : 62 ∈ ChurchNum_ii_6 ChurchNum2 ordsucc 0 (proof)
Known nat_10^nat_10 : nat_p 10
Theorem TwoRamseyProp_3_10_62 : TwoRamseyProp 3 10 62 (proof)
Theorem TwoRamseyProp_3_10_Power_6^{TwoRamseyProp_3_10_Power_6} : TwoRamseyProp 3 10 (prim4 6) (proof)
Theorem TwoRamseyProp_3_10_Power_7^{TwoRamseyProp_3_10_Power_7} : TwoRamseyProp 3 10 (prim4 7) (proof)
Theorem TwoRamseyProp_3_10_Power_8^{TwoRamseyProp_3_10_Power_8} : TwoRamseyProp 3 10 (prim4 8) (proof)