Proofgold Address

Param nat_p^nat_p : ι → ο
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Param ordsucc^ordsucc : ι → ι
Param add_nat^add_nat : ι → ι → ι
Param binunion^binunion : ι → ι → ι
Param Sep^Sep : ι → (ι → ο) → ι
Known 9da24.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . atleastp (add_nat x0 x1) (binunion x2 x3) ⟶ or (atleastp x0 x2) (atleastp x1 x3)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Param Sing^Sing : ι → ι
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known 1dc5a.. : ∀ x0 x1 x2 . nIn x2 x1 ⟶ atleastp x0 x1 ⟶ atleastp (ordsucc x0) (binunion x1 (Sing x2))
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem 610be.. : ∀ x0 x1 x2 x3 . nat_p x2 ⟶ nat_p x3 ⟶ TwoRamseyProp_atleastp (ordsucc x0) x1 x2 ⟶ TwoRamseyProp_atleastp x0 (ordsucc x1) x3 ⟶ TwoRamseyProp_atleastp (ordsucc x0) (ordsucc x1) (ordsucc (add_nat x2 x3)) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x2
Theorem 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)) (proof)
Known 2cf95.. : add_nat 6 4 = 10
Known nat_6^nat_6 : nat_p 6
Known nat_4^nat_4 : nat_p 4
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_3_6^{TwoRamseyProp_3_3_6} : TwoRamseyProp 3 3 6
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem TwoRamseyProp_3_4_11 : TwoRamseyProp 3 4 11 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known nat_16^nat_16 : nat_p 16
Known 2039c.. : 11 ∈ 16
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_4_Power_4^{TwoRamseyProp_3_4_Power_4} : TwoRamseyProp 3 4 (prim4 4) (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_4_Power_5^{TwoRamseyProp_3_4_Power_5} : TwoRamseyProp 3 4 (prim4 5) (proof)
Theorem TwoRamseyProp_3_4_Power_6^{TwoRamseyProp_3_4_Power_6} : TwoRamseyProp 3 4 (prim4 6) (proof)
Theorem TwoRamseyProp_3_4_Power_7^{TwoRamseyProp_3_4_Power_7} : TwoRamseyProp 3 4 (prim4 7) (proof)
Theorem TwoRamseyProp_3_4_Power_8^{TwoRamseyProp_3_4_Power_8} : TwoRamseyProp 3 4 (prim4 8) (proof)
Known 525d1.. : add_nat 11 5 = 16
Known nat_11^nat_11 : nat_p 11
Known nat_5^nat_5 : nat_p 5
Theorem TwoRamseyProp_3_5_17 : TwoRamseyProp 3 5 17 (proof)
Known 1f846.. : nat_p 32
Known 8ad73.. : 17 ∈ 32
Known e089c.. : exp_nat 2 5 = 32
Theorem TwoRamseyProp_3_5_Power_5^{TwoRamseyProp_3_5_Power_5} : TwoRamseyProp 3 5 (prim4 5) (proof)
Theorem TwoRamseyProp_3_5_Power_6^{TwoRamseyProp_3_5_Power_6} : TwoRamseyProp 3 5 (prim4 6) (proof)
Theorem TwoRamseyProp_3_5_Power_7^{TwoRamseyProp_3_5_Power_7} : TwoRamseyProp 3 5 (prim4 7) (proof)
Theorem TwoRamseyProp_3_5_Power_8^{TwoRamseyProp_3_5_Power_8} : TwoRamseyProp 3 5 (prim4 8) (proof)
Known d5f37.. : add_nat 11 11 = 22
Known 42643.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp_atleastp x1 x0 x2
Theorem TwoRamseyProp_4_4_23 : TwoRamseyProp 4 4 23 (proof)
Known e4564.. : 23 ∈ 32
Theorem TwoRamseyProp_4_4_Power_5^{TwoRamseyProp_4_4_Power_5} : TwoRamseyProp 4 4 (prim4 5) (proof)
Theorem TwoRamseyProp_4_4_Power_6^{TwoRamseyProp_4_4_Power_6} : TwoRamseyProp 4 4 (prim4 6) (proof)
Theorem TwoRamseyProp_4_4_Power_7^{TwoRamseyProp_4_4_Power_7} : TwoRamseyProp 4 4 (prim4 7) (proof)
Theorem TwoRamseyProp_4_4_Power_8^{TwoRamseyProp_4_4_Power_8} : TwoRamseyProp 4 4 (prim4 8) (proof)
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 f6732.. : add_nat 17 1 = 18 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem 87c30.. : add_nat 17 2 = 19 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem cd6de.. : add_nat 17 3 = 20 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 7246a.. : add_nat 17 4 = 21 (proof)
Theorem 6670f.. : add_nat 17 5 = 22 (proof)
Theorem eec07.. : add_nat 17 6 = 23 (proof)
Known nat_17^nat_17 : nat_p 17
Theorem TwoRamseyProp_3_6_24 : TwoRamseyProp 3 6 24 (proof)
Known be3fd.. : 24 ∈ 32
Theorem TwoRamseyProp_3_6_Power_5^{TwoRamseyProp_3_6_Power_5} : TwoRamseyProp 3 6 (prim4 5) (proof)
Theorem TwoRamseyProp_3_6_Power_6^{TwoRamseyProp_3_6_Power_6} : TwoRamseyProp 3 6 (prim4 6) (proof)
Theorem TwoRamseyProp_3_6_Power_7^{TwoRamseyProp_3_6_Power_7} : TwoRamseyProp 3 6 (prim4 7) (proof)
Theorem TwoRamseyProp_3_6_Power_8^{TwoRamseyProp_3_6_Power_8} : TwoRamseyProp 3 6 (prim4 8) (proof)