Nuprl Lemma : red-black-example-ext

`∀[A,D:Type]. ∀[Red,Black:D ⟶ ℙ]. ∀[R:D ⟶ D ⟶ ℙ].`
`  ((∀x:D. (Red[x] ∨ Black[x]))`
`  `` (∀x,y,z:D.  (R[x;y] `` R[y;z] `` R[x;z]))`
`  `` (∀x:D. (R[x;x] `` A))`
`  `` (∀x:D. (Red[x] `` (∃y:D. (Black[y] ∧ R[x;y]))))`
`  `` (∀x:D. (Black[x] `` (∃y:D. (Red[y] ∧ R[x;y]))))`
`  `` (∃m:D. ((∀x:D. (Red[x] `` R[x;m])) ∨ (∀x:D. (Black[x] `` R[x;m]))))`
`  `` A)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` spreadn: spread3 red-black-example
Lemmas referenced :  red-black-example
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A,D:Type].  \mforall{}[Red,Black:D  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x:D.  (Red[x]  \mvee{}  Black[x]))
{}\mRightarrow{}  (\mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  R[y;z]  {}\mRightarrow{}  R[x;z]))
{}\mRightarrow{}  (\mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A))
{}\mRightarrow{}  (\mforall{}x:D.  (Red[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Black[y]  \mwedge{}  R[x;y]))))
{}\mRightarrow{}  (\mforall{}x:D.  (Black[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Red[y]  \mwedge{}  R[x;y]))))
{}\mRightarrow{}  (\mexists{}m:D.  ((\mforall{}x:D.  (Red[x]  {}\mRightarrow{}  R[x;m]))  \mvee{}  (\mforall{}x:D.  (Black[x]  {}\mRightarrow{}  R[x;m]))))
{}\mRightarrow{}  A)

Date html generated: 2018_05_21-PM-08_55_37
Last ObjectModification: 2018_05_19-PM-05_07_58

Theory : general

Home Index