Proofgold Address

Param nat_p^nat_p : ι → ο
Param TwoRamseyProp_atleastp : ι → ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param add_nat^add_nat : ι → ι → ι
Known 1f164.. : ∀ x0 x1 x2 x3 . nat_p x2 ⟶ nat_p x3 ⟶ TwoRamseyProp_atleastp (ordsucc x0) x1 (ordsucc x2) ⟶ TwoRamseyProp_atleastp x0 (ordsucc x1) (ordsucc x3) ⟶ TwoRamseyProp_atleastp (ordsucc x0) (ordsucc x1) (ordsucc (ordsucc (add_nat x2 x3)))
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x2
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 atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem 164da..^{TwoRamseyProp_bd} : ∀ x0 x1 x2 x3 . nat_p x2 ⟶ nat_p x3 ⟶ TwoRamseyProp (ordsucc x0) x1 (ordsucc x2) ⟶ TwoRamseyProp x0 (ordsucc x1) (ordsucc x3) ⟶ TwoRamseyProp (ordsucc x0) (ordsucc x1) (ordsucc (ordsucc (add_nat x2 x3))) (proof)
Known 95eb4.. : ∀ x0 . TwoRamseyProp_atleastp 2 x0 x0
Theorem f0d6f..^{TwoRamseyProp_2} : ∀ x0 . TwoRamseyProp 2 x0 x0 (proof)
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Known 69b67..^add_nat_8_4 : add_nat 8 4 = 12
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Known nat_8^nat_8 : nat_p 8
Known nat_4^nat_4 : nat_p 4
Known TwoRamseyProp_3_4_9^{TwoRamseyProp_3_4_9} : TwoRamseyProp 3 4 9
Theorem TwoRamseyProp_3_5_14^{TwoRamseyProp_3_5_14} : TwoRamseyProp 3 5 14 (proof)
Known TwoRamseyProp_4_4_18^{TwoRamseyProp_4_4_18} : TwoRamseyProp 4 4 18
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_6^nat_6 : nat_p 6
Known eec07.. : add_nat 17 6 = 23
Theorem e7d46.. : add_nat u17 u7 = u24 (proof)
Definition u25 := ordsucc u24
Known nat_7^nat_7 : nat_p 7
Theorem 8609e.. : add_nat u17 u8 = u25 (proof)
Definition u26 := ordsucc u25
Theorem d04d9.. : add_nat u17 u9 = u26 (proof)
Definition u27 := ordsucc u26
Known nat_9^nat_9 : nat_p 9
Theorem 5782f.. : add_nat u17 u10 = u27 (proof)
Definition u28 := ordsucc u27
Known nat_10^nat_10 : nat_p 10
Theorem 37f74.. : add_nat u17 u11 = u28 (proof)
Definition u29 := ordsucc u28
Known nat_11^nat_11 : nat_p 11
Theorem 9f043.. : add_nat u17 u12 = u29 (proof)
Definition u30 := ordsucc u29
Known nat_12^nat_12 : nat_p 12
Theorem 8d18d.. : add_nat u17 u13 = u30 (proof)
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Known nat_17^nat_17 : nat_p 17
Known nat_13^nat_13 : nat_p 13
Theorem TwoRamseyProp_u4_u5_u32 : TwoRamseyProp u4 u5 u32 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Param exp_nat^exp_nat : ι → ι → ι
Known e089c.. : exp_nat 2 5 = 32
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_5^nat_5 : nat_p 5
Theorem TwoRamseyProp_4_5_Power_5^{TwoRamseyProp_4_5_Power_5} : TwoRamseyProp 4 5 (prim4 5) (proof)
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
Definition u36 := ordsucc u35
Definition u37 := ordsucc u36
Definition u38 := ordsucc u37
Definition u39 := ordsucc u38
Definition u40 := ordsucc u39
Definition u41 := ordsucc u40
Definition u42 := ordsucc u41
Definition u43 := ordsucc u42
Definition u44 := ordsucc u43
Definition u45 := ordsucc u44
Definition u46 := ordsucc u45
Definition u47 := ordsucc u46
Definition u48 := ordsucc u47
Definition u49 := ordsucc u48
Definition u50 := ordsucc u49
Definition u51 := ordsucc u50
Definition u52 := ordsucc u51
Definition u53 := ordsucc u52
Definition u54 := ordsucc u53
Definition u55 := ordsucc u54
Definition u56 := ordsucc u55
Definition u57 := ordsucc u56
Definition u58 := ordsucc u57
Definition u59 := ordsucc u58
Definition u60 := ordsucc u59
Definition u61 := ordsucc u60
Definition u62 := ordsucc u61
Definition u63 := ordsucc u62
Definition u64 := ordsucc u63
Definition u65 := ordsucc u64
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 10cab.. : add_nat u31 u1 = u32 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem f92a1.. : add_nat u31 u2 = u33 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem 511f7.. : add_nat u31 u3 = u34 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem d826c.. : add_nat u31 u4 = u35 (proof)
Theorem 2fe22.. : add_nat u31 u5 = u36 (proof)
Theorem f4e1a.. : add_nat u31 u6 = u37 (proof)
Theorem bf403.. : add_nat u31 u7 = u38 (proof)
Theorem b109e.. : add_nat u31 u8 = u39 (proof)
Theorem 701cc.. : add_nat u31 u9 = u40 (proof)
Theorem 5bff0.. : add_nat u31 u10 = u41 (proof)
Theorem c4ffa.. : add_nat u31 u11 = u42 (proof)
Theorem d9ac1.. : add_nat u31 u12 = u43 (proof)
Theorem 33bf0.. : add_nat u31 u13 = u44 (proof)
Theorem acfb0.. : add_nat u31 u14 = u45 (proof)
Known nat_14^nat_14 : nat_p 14
Theorem e721a.. : add_nat u31 u15 = u46 (proof)
Known nat_15^nat_15 : nat_p 15
Theorem 54b8d.. : add_nat u31 u16 = u47 (proof)
Known nat_16^nat_16 : nat_p 16
Theorem 0e651.. : add_nat u31 u17 = u48 (proof)
Theorem 5af7c.. : add_nat u31 u18 = u49 (proof)
Known 86c65.. : nat_p u18
Theorem 20c1f.. : add_nat u31 u19 = u50 (proof)
Known d9e2e.. : nat_p u19
Theorem a3ba7.. : add_nat u31 u20 = u51 (proof)
Known 2669c.. : nat_p u20
Theorem b4a35.. : add_nat u31 u21 = u52 (proof)
Known e8a0a.. : nat_p u21
Theorem 64359.. : add_nat u31 u22 = u53 (proof)
Known daa33.. : nat_p u22
Theorem 1d45f.. : add_nat u31 u23 = u54 (proof)
Known b73b8.. : nat_p u23
Theorem 82374.. : add_nat u31 u24 = u55 (proof)
Known 73189.. : nat_p u24
Theorem 28932.. : add_nat u31 u25 = u56 (proof)
Known d5180.. : nat_p u25
Theorem 259e4.. : add_nat u31 u26 = u57 (proof)
Known 24234.. : nat_p u26
Theorem bf663.. : add_nat u31 u27 = u58 (proof)
Known e06fe.. : nat_p u27
Theorem 3c2af.. : add_nat u31 u28 = u59 (proof)
Known 5c78e.. : nat_p u28
Theorem 3301d.. : add_nat u31 u29 = u60 (proof)
Known 7e1a8.. : nat_p u29
Theorem 510c8.. : add_nat u31 u30 = u61 (proof)
Known a9ae2.. : nat_p u30
Theorem 6cf36.. : add_nat u31 u31 = u62 (proof)
Known 74918.. : nat_p u31
Known 0d7c6.. : ∀ x0 x1 x2 . TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x1 x0 x2
Theorem TwoRamseyProp_u5_u5_u64 : TwoRamseyProp u5 u5 u64 (proof)
Theorem 73823.. : add_nat u31 u32 = u63 (proof)
Known add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known 1f846.. : nat_p u32
Theorem 304b9.. : add_nat u32 u32 = u64 (proof)
Param mul_nat^mul_nat : ι → ι → ι
Known add_nat_1_1_2^{add_nat_1_1_2} : add_nat 1 1 = 2
Known mul_add_nat_distrR^{mul_add_nat_distrR} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2)
Known f11bb.. : ∀ x0 . nat_p x0 ⟶ mul_nat 1 x0 = x0
Theorem 6cce6.. : ∀ x0 . nat_p x0 ⟶ mul_nat u2 x0 = add_nat x0 x0 (proof)
Known caaf4..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ exp_nat x0 (ordsucc x1) = mul_nat x0 (exp_nat x0 x1)
Theorem 337ce.. : exp_nat u2 u6 = u64 (proof)
Theorem TwoRamseyProp_5_5_Power_6^{TwoRamseyProp_5_5_Power_6} : TwoRamseyProp 5 5 (prim4 6) (proof)