Proofgold Asset

Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition ChurchNum_ii_5 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 x1))))
Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . 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_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known nat_9^nat_9 : nat_p 9
Theorem 61d53.. : nat_p 41 (proof)
Param add_nat^add_nat : ι → ι → ι
Definition ChurchNum_ii_3 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 x1))
Definition ChurchNum_ii_4 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 x1)))
Known 218e1.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_4 ChurchNum2 x0 x3) = ChurchNum_ii_4 ChurchNum2 x0 (x2 x3)
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_8^nat_8 : nat_p 8
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_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem f6a7c.. : add_nat 41 24 = 65 (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))
Known 73189.. : nat_p 24
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_4_5_41 : TwoRamseyProp 4 5 41
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known TwoRamseyProp_3_6_24 : TwoRamseyProp 3 6 24
Theorem TwoRamseyProp_4_6_66 : TwoRamseyProp 4 6 66 (proof)
Definition ChurchNum_ii_7 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))
Definition ChurchNum_ii_2 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 x1)
Known 80fa6.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_5 ChurchNum2 x0 x2)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 8c01a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_4 ChurchNum2 x0 x2)
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)
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 ecfd3.. : 66 ∈ ChurchNum_ii_7 ChurchNum2 ordsucc 0 (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 cc1c2.. : exp_nat 2 7 = ChurchNum_ii_7 ChurchNum2 ordsucc 0
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 5eca6.. : nat_p 128
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_7^nat_7 : nat_p 7
Theorem TwoRamseyProp_4_6_Power_7^{TwoRamseyProp_4_6_Power_7} : TwoRamseyProp 4 6 (prim4 7) (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_4_6_Power_8^{TwoRamseyProp_4_6_Power_8} : TwoRamseyProp 4 6 (prim4 8) (proof)
Known 93d19.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_5 ChurchNum2 x0 x3) = ChurchNum_ii_5 ChurchNum2 x0 (x2 x3)
Known nat_1^nat_1 : nat_p 1
Theorem f99bf.. : add_nat 41 41 = 82 (proof)
Known 42643.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp_atleastp x1 x0 x2
Theorem TwoRamseyProp_5_5_83 : TwoRamseyProp 5 5 83 (proof)
Theorem 694f0.. : 83 ∈ ChurchNum_ii_7 ChurchNum2 ordsucc 0 (proof)
Theorem TwoRamseyProp_5_5_Power_7^{TwoRamseyProp_5_5_Power_7} : TwoRamseyProp 5 5 (prim4 7) (proof)
Theorem TwoRamseyProp_5_5_Power_8^{TwoRamseyProp_5_5_Power_8} : TwoRamseyProp 5 5 (prim4 8) (proof)
Theorem cbfd5.. : add_nat 66 32 = 98 (proof)
Known 3ae46.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_4 ChurchNum2 x0 x2)
Known 078b0.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_3 ChurchNum2 x0 x2)
Known nat_10^nat_10 : nat_p 10
Theorem ad171.. : nat_p 66 (proof)
Known 1f846.. : nat_p 32
Known TwoRamseyProp_3_7_32 : TwoRamseyProp 3 7 32
Theorem TwoRamseyProp_4_7_99 : TwoRamseyProp 4 7 99 (proof)
Theorem 06f74.. : 99 ∈ ChurchNum_ii_7 ChurchNum2 ordsucc 0 (proof)
Theorem TwoRamseyProp_4_7_Power_7^{TwoRamseyProp_4_7_Power_7} : TwoRamseyProp 4 7 (prim4 7) (proof)
Theorem TwoRamseyProp_4_7_Power_8^{TwoRamseyProp_4_7_Power_8} : TwoRamseyProp 4 7 (prim4 8) (proof)