Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0Church13_p x1Church13_p x2Church13_p x3Church13_p x4(x0 = x1∀ x5 : ο . x5)(x0 = x2∀ x5 : ο . x5)(x0 = x3∀ x5 : ο . x5)(x0 = x4∀ x5 : ο . x5)(x1 = x2∀ x5 : ο . x5)(x1 = x3∀ x5 : ο . x5)(x1 = x4∀ x5 : ο . x5)(x2 = x3∀ x5 : ο . x5)(x2 = x4∀ x5 : ο . x5)(x3 = x4∀ x5 : ο . x5)(TwoRamseyGraph_3_5_Church13 x0 x1 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x0 x2 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x0 x3 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x0 x4 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x1 x2 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x1 x3 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x1 x4 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x2 x3 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x2 x4 = λ x6 x7 . x7)(TwoRamseyGraph_3_5_Church13 x3 x4 = λ x6 x7 . x7)False
as obj
-
as prop
4a8a6..
theory
HotG
stx
3c3e7..
address
TMXvV..