Proofgold Address

Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition ChurchNum_ii_6 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 x1)))))
Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . x0 (x0 x1)
Known f3785.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_6 ChurchNum2 x0 x2)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
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_3^nat_3 : nat_p 3
Theorem 5b6f8.. : nat_p 99 (proof)
Param add_nat^add_nat : ι → ι → ι
Definition ChurchNum_ii_3 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 x1))
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 add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_9^nat_9 : nat_p 9
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_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 9280e.. : add_nat 99 41 = 140 (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 61d53.. : nat_p 41
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_7_99 : TwoRamseyProp 4 7 99
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known TwoRamseyProp_3_8_41 : TwoRamseyProp 3 8 41
Theorem TwoRamseyProp_4_8_141 : TwoRamseyProp 4 8 141 (proof)
Definition ChurchNum_ii_8 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))
Definition ChurchNum_ii_4 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 x1)))
Known b8288.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_6 ChurchNum2 x0 x2)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
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)
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 1b77a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum2 x0 x2)
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 20b75.. : 141 ∈ ChurchNum_ii_8 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 bbc1b.. : exp_nat 2 8 = ChurchNum_ii_8 ChurchNum2 ordsucc 0
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 28496.. : nat_p 256
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_8^nat_8 : nat_p 8
Theorem TwoRamseyProp_4_8_Power_8^{TwoRamseyProp_4_8_Power_8} : TwoRamseyProp 4 8 (prim4 8) (proof)