Definition. We define TwoRamseyProp to be λM N V ⇒ ∀R : set → set → prop, (∀x y, R x y → R y x) → ((∃X ⊆ V, equip M X ∧ (∀x y ∈ X, x ≠ y → R x y)) ∨ (∃Y ⊆ V, equip N Y ∧ (∀x y ∈ Y, x ≠ y → ¬ R x y))) of type set → set → set → prop.

In Proofgold the corresponding term root is c5d86c... and object id is faf73f...

Theorem. (not_TwoRamseyProp_3_7_22)

¬ TwoRamseyProp 3 7 22

In Proofgold the corresponding term root is 781928... and proposition id is 9e7335...

Proof:
Proof not loaded.

L12

Theorem. (not_TwoRamseyProp_3_8_27)

¬ TwoRamseyProp 3 8 27

In Proofgold the corresponding term root is a70f2e... and proposition id is 828bca...

Proof:
Proof not loaded.

L16

Theorem. (not_TwoRamseyProp_3_9_35)

¬ TwoRamseyProp 3 9 35

In Proofgold the corresponding term root is d13ea9... and proposition id is ad1c84...

Proof:
Proof not loaded.

L20

Theorem. (not_TwoRamseyProp_3_10_39)

¬ TwoRamseyProp 3 10 39

In Proofgold the corresponding term root is f07e7a... and proposition id is cbbd38...

Proof:
Proof not loaded.

L24

Theorem. (not_TwoRamseyProp_4_7_48)

¬ TwoRamseyProp 4 7 48

In Proofgold the corresponding term root is 6fa829... and proposition id is 7db35f...

Proof:
Proof not loaded.

L28

Theorem. (not_TwoRamseyProp_4_8_58)

¬ TwoRamseyProp 4 8 58

In Proofgold the corresponding term root is 902a09... and proposition id is 2044fd...

Proof:
Proof not loaded.

L32

Theorem. (not_TwoRamseyProp_4_9_72)

¬ TwoRamseyProp 4 9 72

In Proofgold the corresponding term root is e27002... and proposition id is cecb1a...

Proof:
Proof not loaded.

L36

Theorem. (not_TwoRamseyProp_5_5_42)

¬ TwoRamseyProp 5 5 42

In Proofgold the corresponding term root is 719f58... and proposition id is c7463a...

Proof:
Proof not loaded.

L40

Theorem. (not_TwoRamseyProp_5_6_57)

¬ TwoRamseyProp 5 6 57

In Proofgold the corresponding term root is 845185... and proposition id is 580f9d...

Proof:
Proof not loaded.

L44

Theorem. (not_TwoRamseyProp_5_7_79)

¬ TwoRamseyProp 5 7 79

In Proofgold the corresponding term root is 527b93... and proposition id is 6a8180...

Proof:
Proof not loaded.

L48

Theorem. (not_TwoRamseyProp_5_8_100)

¬ TwoRamseyProp 5 8 100

In Proofgold the corresponding term root is 482b10... and proposition id is 10514b...

Proof:
Proof not loaded.

L52

Theorem. (not_TwoRamseyProp_6_6_101)

¬ TwoRamseyProp 6 6 101

In Proofgold the corresponding term root is 9ca7da... and proposition id is ccd3e7...

Proof:
Proof not loaded.

L56

Theorem. (not_TwoRamseyProp_6_7_114)

¬ TwoRamseyProp 6 7 114

In Proofgold the corresponding term root is d69655... and proposition id is d6f6b1...

Proof:
Proof not loaded.

L60

Theorem. (TwoRamseyProp_3_6_18)

TwoRamseyProp 3 6 18

In Proofgold the corresponding term root is 81b8e4... and proposition id is ab81a1...

Proof:
Proof not loaded.

L64

Theorem. (TwoRamseyProp_3_7_23)

TwoRamseyProp 3 7 23

In Proofgold the corresponding term root is c400bb... and proposition id is 2265c1...

Proof:
Proof not loaded.

L68

Theorem. (TwoRamseyProp_3_8_28)

TwoRamseyProp 3 8 28

In Proofgold the corresponding term root is afae62... and proposition id is a89eaa...

Proof:
Proof not loaded.

L72

Theorem. (TwoRamseyProp_3_9_36)

TwoRamseyProp 3 9 36

In Proofgold the corresponding term root is cc11e3... and proposition id is 5b30ba...

Proof:
Proof not loaded.

L76

Theorem. (TwoRamseyProp_3_10_42)

TwoRamseyProp 3 10 42

In Proofgold the corresponding term root is ff9a0d... and proposition id is 6f9cfa...

Proof:
Proof not loaded.

L80

Theorem. (TwoRamseyProp_4_5_25)

TwoRamseyProp 4 5 25

In Proofgold the corresponding term root is 73be68... and proposition id is cc7495...

Proof:
Proof not loaded.

L84

Theorem. (TwoRamseyProp_4_6_41)

TwoRamseyProp 4 6 41

In Proofgold the corresponding term root is bb42d4... and proposition id is 8ecff7...

Proof:
Proof not loaded.

L88

Theorem. (TwoRamseyProp_4_7_61)

TwoRamseyProp 4 7 61

In Proofgold the corresponding term root is 5ef5f1... and proposition id is 019f14...

Proof:
Proof not loaded.

L92

Theorem. (TwoRamseyProp_4_8_84)

TwoRamseyProp 4 8 84

In Proofgold the corresponding term root is 8709c0... and proposition id is ae49e3...

Proof:
Proof not loaded.

L96

Theorem. (TwoRamseyProp_4_9_115)

TwoRamseyProp 4 9 115

In Proofgold the corresponding term root is 5a92ff... and proposition id is 0df9d6...

Proof:
Proof not loaded.

L100

Theorem. (TwoRamseyProp_5_5_48)

TwoRamseyProp 5 5 48

In Proofgold the corresponding term root is abf150... and proposition id is 4c7566...

Proof:
Proof not loaded.

L104

Theorem. (TwoRamseyProp_5_6_87)

TwoRamseyProp 5 6 87

In Proofgold the corresponding term root is 43db24... and proposition id is bfcef2...

Proof:
Proof not loaded.

L108

Theorem. (TwoRamseyProp_5_7_143)

TwoRamseyProp 5 7 143

In Proofgold the corresponding term root is 656f91... and proposition id is 67a94c...

Proof:
Proof not loaded.

L112

Theorem. (TwoRamseyProp_5_8_216)

TwoRamseyProp 5 8 216

In Proofgold the corresponding term root is 516a20... and proposition id is f57af5...

Proof:
Proof not loaded.

L116

Theorem. (TwoRamseyProp_6_6_165)

TwoRamseyProp 6 6 165

In Proofgold the corresponding term root is 10e700... and proposition id is 184bf0...

Proof:
Proof not loaded.

L120

Theorem. (TwoRamseyProp_6_7_298)

TwoRamseyProp 6 7 298

In Proofgold the corresponding term root is ea7d2e... and proposition id is 6bc284...

Proof:
Proof not loaded.

L124

Theorem. (not_TwoRamseyProp_3_9_Power_5)

¬ TwoRamseyProp 3 9 (𝒫 5)

In Proofgold the corresponding term root is f978c0... and proposition id is 976d22...

Proof:
Proof not loaded.

L128

Theorem. (not_TwoRamseyProp_3_10_Power_5)

¬ TwoRamseyProp 3 10 (𝒫 5)

In Proofgold the corresponding term root is 1279fc... and proposition id is 0c824e...

Proof:
Proof not loaded.

L132

Theorem. (not_TwoRamseyProp_4_9_Power_6)

¬ TwoRamseyProp 4 9 (𝒫 6)

In Proofgold the corresponding term root is ab00f3... and proposition id is aaf471...

Proof:
Proof not loaded.

L136

Theorem. (not_TwoRamseyProp_5_5_Power_5)

¬ TwoRamseyProp 5 5 (𝒫 5)

In Proofgold the corresponding term root is ce5e33... and proposition id is 181da7...

Proof:
Proof not loaded.

L140

Theorem. (not_TwoRamseyProp_5_7_Power_6)

¬ TwoRamseyProp 5 7 (𝒫 6)

In Proofgold the corresponding term root is 63d422... and proposition id is 5b9e15...

Proof:
Proof not loaded.

L144

Theorem. (not_TwoRamseyProp_5_8_Power_6)

¬ TwoRamseyProp 5 8 (𝒫 6)

In Proofgold the corresponding term root is 659e09... and proposition id is cd9fa7...

Proof:
Proof not loaded.

L148

Theorem. (not_TwoRamseyProp_6_6_Power_6)

¬ TwoRamseyProp 6 6 (𝒫 6)

In Proofgold the corresponding term root is 7369ec... and proposition id is 129ce3...

Proof:
Proof not loaded.

L152

Theorem. (not_TwoRamseyProp_6_7_Power_6)

¬ TwoRamseyProp 6 7 (𝒫 6)

In Proofgold the corresponding term root is 77aa69... and proposition id is 65eeb0...

Proof:
Proof not loaded.

L156

Theorem. (TwoRamseyProp_3_8_Power_5)

TwoRamseyProp 3 8 (𝒫 5)

In Proofgold the corresponding term root is d27407... and proposition id is 736840...

Proof:
Proof not loaded.

L160

Theorem. (TwoRamseyProp_4_6_Power_6)

TwoRamseyProp 4 6 (𝒫 6)

In Proofgold the corresponding term root is a518e8... and proposition id is 1e5e44...

Proof:
Proof not loaded.

L164

Theorem. (TwoRamseyProp_4_7_Power_6)

TwoRamseyProp 4 7 (𝒫 6)

In Proofgold the corresponding term root is bc5303... and proposition id is 0ea3e8...

Proof:
Proof not loaded.

L168

Theorem. (TwoRamseyProp_4_9_Power_7)

TwoRamseyProp 4 9 (𝒫 7)

In Proofgold the corresponding term root is e4ef51... and proposition id is 75d1df...

Proof:
Proof not loaded.

L172

Theorem. (TwoRamseyProp_5_6_Power_7)

TwoRamseyProp 5 6 (𝒫 7)

In Proofgold the corresponding term root is 2d548a... and proposition id is 4005bf...

Proof:
Proof not loaded.

L176

Theorem. (TwoRamseyProp_5_7_Power_8)

TwoRamseyProp 5 7 (𝒫 8)

In Proofgold the corresponding term root is e2647f... and proposition id is c6e221...

Proof:
Proof not loaded.

L180

Theorem. (TwoRamseyProp_5_8_Power_8)

TwoRamseyProp 5 8 (𝒫 8)

In Proofgold the corresponding term root is 384300... and proposition id is 31b50b...

Proof:
Proof not loaded.

L184

Theorem. (TwoRamseyProp_6_6_Power_8)

TwoRamseyProp 6 6 (𝒫 8)

In Proofgold the corresponding term root is 447712... and proposition id is c30d48...

Proof:
Proof not loaded.

L188

Theorem. (TwoRamseyProp_3_10_40)

TwoRamseyProp 3 10 40

In Proofgold the corresponding term root is 819cb8... and proposition id is f3e4ef...

Proof:
Proof not loaded.

L192

Theorem. (TwoRamseyProp_3_10_41)

TwoRamseyProp 3 10 41

In Proofgold the corresponding term root is 2f991f... and proposition id is 47305a...

Proof:
Proof not loaded.

L196

Theorem. (TwoRamseyProp_4_6_36)

TwoRamseyProp 4 6 36

In Proofgold the corresponding term root is ecf55c... and proposition id is 9cb5e1...

Proof:
Proof not loaded.

L200

Theorem. (TwoRamseyProp_4_6_40)

TwoRamseyProp 4 6 40

In Proofgold the corresponding term root is cca9c8... and proposition id is 130f84...

Proof:
Proof not loaded.

L204

Theorem. (TwoRamseyProp_4_7_49)

TwoRamseyProp 4 7 49

In Proofgold the corresponding term root is 339a49... and proposition id is 9a8e3c...

Proof:
Proof not loaded.

L208

Theorem. (TwoRamseyProp_4_7_60)

TwoRamseyProp 4 7 60

In Proofgold the corresponding term root is b0a10d... and proposition id is 937b9a...

Proof:
Proof not loaded.

L212

Theorem. (TwoRamseyProp_4_8_59)

TwoRamseyProp 4 8 59

In Proofgold the corresponding term root is a4013a... and proposition id is 750bb8...

Proof:
Proof not loaded.

L216

Theorem. (TwoRamseyProp_4_8_83)

TwoRamseyProp 4 8 83

In Proofgold the corresponding term root is ef7fe9... and proposition id is faf2bb...

Proof:
Proof not loaded.

L220

Theorem. (TwoRamseyProp_4_9_73)

TwoRamseyProp 4 9 73

In Proofgold the corresponding term root is eb38e5... and proposition id is 0b30c5...

Proof:
Proof not loaded.

L224

Theorem. (TwoRamseyProp_4_9_114)

TwoRamseyProp 4 9 114

In Proofgold the corresponding term root is 875b53... and proposition id is beb3ce...

Proof:
Proof not loaded.

L228

Theorem. (TwoRamseyProp_5_5_43)

TwoRamseyProp 5 5 43

In Proofgold the corresponding term root is fa1f88... and proposition id is e5b639...

Proof:
Proof not loaded.

L232

Theorem. (TwoRamseyProp_5_5_47)

TwoRamseyProp 5 5 47

In Proofgold the corresponding term root is e26c1c... and proposition id is e11650...

Proof:
Proof not loaded.

L236

Theorem. (TwoRamseyProp_5_6_58)

TwoRamseyProp 5 6 58

In Proofgold the corresponding term root is c460b3... and proposition id is b51440...

Proof:
Proof not loaded.

L240

Theorem. (TwoRamseyProp_5_6_86)

TwoRamseyProp 5 6 86

In Proofgold the corresponding term root is 9d293f... and proposition id is dba4bd...

Proof:
Proof not loaded.

L244

Theorem. (TwoRamseyProp_5_7_80)

TwoRamseyProp 5 7 80

In Proofgold the corresponding term root is 6ec438... and proposition id is c8d15a...

Proof:
Proof not loaded.

L248

Theorem. (TwoRamseyProp_5_7_142)

TwoRamseyProp 5 7 142

In Proofgold the corresponding term root is cb2ea4... and proposition id is 89daf3...

Proof:
Proof not loaded.

L252

Theorem. (TwoRamseyProp_5_8_101)

TwoRamseyProp 5 8 101

In Proofgold the corresponding term root is 83ea87... and proposition id is 11f946...

Proof:
Proof not loaded.

L256

Theorem. (TwoRamseyProp_5_8_215)

TwoRamseyProp 5 8 215

In Proofgold the corresponding term root is 5d1e89... and proposition id is 3f0856...

Proof:
Proof not loaded.

L260

Theorem. (TwoRamseyProp_6_6_102)

TwoRamseyProp 6 6 102

In Proofgold the corresponding term root is d70e2c... and proposition id is 13553e...

Proof:
Proof not loaded.

L264

Theorem. (TwoRamseyProp_6_6_164)

TwoRamseyProp 6 6 164

In Proofgold the corresponding term root is 1db0b3... and proposition id is 54fb46...

Proof:
Proof not loaded.

L268

Theorem. (TwoRamseyProp_6_7_115)

TwoRamseyProp 6 7 115

In Proofgold the corresponding term root is 814a85... and proposition id is 9c5ae9...

Proof:
Proof not loaded.

L272

Theorem. (TwoRamseyProp_6_7_297)

TwoRamseyProp 6 7 297

In Proofgold the corresponding term root is 33269e... and proposition id is bb403e...

Proof:
Proof not loaded.