Proofgold Address

Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param add_nat^add_nat : ι → ι → ι
Known 8b5c1.. : add_nat 32 8 = 40
Param nat_p^nat_p : ι → ο
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 1f846.. : nat_p 32
Known nat_8^nat_8 : nat_p 8
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_7_32 : TwoRamseyProp 3 7 32
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem TwoRamseyProp_3_8_41 : TwoRamseyProp 3 8 41 (proof)
Param exp_nat^exp_nat : ι → ι → ι
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Known nat_2^nat_2 : nat_p 2
Known nat_6^nat_6 : nat_p 6
Param Sigma_nat : ι → (ι → ι) → ι
Param mul_nat^mul_nat : ι → ι → ι
Known 0c734.. : Sigma_nat 6 (λ x1 . mul_nat (ap (lam 6 (λ x2 . If_i (x2 = 0) 1 (If_i (x2 = 1) 0 (If_i (x2 = 2) 0 (If_i (x2 = 3) 1 (If_i (x2 = 4) 0 1)))))) x1) (exp_nat 2 x1)) = 41
Known bdfcb.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ 2) ⟶ Sigma_nat x0 (λ x2 . mul_nat (x1 x2) (exp_nat 2 x2)) ∈ exp_nat 2 x0
Known cases_6^cases_6 : ∀ x0 . x0 ∈ 6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 x0
Known tuple_6_0_eq^tuple_6_0_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 0 = x0
Known In_1_2^In_1_2 : 1 ∈ 2
Known tuple_6_1_eq^tuple_6_1_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 1 = x1
Known In_0_2^In_0_2 : 0 ∈ 2
Known tuple_6_2_eq^tuple_6_2_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 2 = x2
Known tuple_6_3_eq^tuple_6_3_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 3 = x3
Known tuple_6_4_eq^tuple_6_4_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 4 = x4
Known tuple_6_5_eq^tuple_6_5_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 5 = x5
Theorem 89af8.. : atleastp 41 (exp_nat 2 6) (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
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)
Theorem TwoRamseyProp_3_8_Power_6^{TwoRamseyProp_3_8_Power_6} : TwoRamseyProp 3 8 (prim4 6) (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_8_Power_7^{TwoRamseyProp_3_8_Power_7} : TwoRamseyProp 3 8 (prim4 7) (proof)
Theorem TwoRamseyProp_3_8_Power_8^{TwoRamseyProp_3_8_Power_8} : TwoRamseyProp 3 8 (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 2e090.. : add_nat 23 8 = 31
Theorem 02d84.. : add_nat 23 9 = 32 (proof)
Known nat_9^nat_9 : nat_p 9
Theorem 1db04.. : add_nat 23 10 = 33 (proof)
Known nat_10^nat_10 : nat_p 10
Theorem 829e3.. : add_nat 23 11 = 34 (proof)
Known nat_11^nat_11 : nat_p 11
Theorem 25750.. : add_nat 23 12 = 35 (proof)
Known nat_12^nat_12 : nat_p 12
Theorem 4bf38.. : add_nat 23 13 = 36 (proof)
Known nat_13^nat_13 : nat_p 13
Theorem fb7b7.. : add_nat 23 14 = 37 (proof)
Known nat_14^nat_14 : nat_p 14
Theorem b9812.. : add_nat 23 15 = 38 (proof)
Known nat_15^nat_15 : nat_p 15
Theorem 97994.. : add_nat 23 16 = 39 (proof)
Known nat_16^nat_16 : nat_p 16
Theorem 5973b.. : add_nat 23 17 = 40 (proof)
Known 90194.. : add_nat 11 12 = 23
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Theorem b73b8.. : nat_p 23 (proof)
Known nat_17^nat_17 : nat_p 17
Known TwoRamseyProp_4_4_23 : TwoRamseyProp 4 4 23
Known TwoRamseyProp_3_5_17 : TwoRamseyProp 3 5 17
Theorem TwoRamseyProp_4_5_41 : TwoRamseyProp 4 5 41 (proof)
Theorem TwoRamseyProp_4_5_Power_6^{TwoRamseyProp_4_5_Power_6} : TwoRamseyProp 4 5 (prim4 6) (proof)
Theorem TwoRamseyProp_4_5_Power_7^{TwoRamseyProp_4_5_Power_7} : TwoRamseyProp 4 5 (prim4 7) (proof)
Theorem TwoRamseyProp_4_5_Power_8^{TwoRamseyProp_4_5_Power_8} : TwoRamseyProp 4 5 (prim4 8) (proof)