### Nuprl Lemma : test-red-black-example

`∀[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 :  uall: `∀[x:A]. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` or: `P ∨ Q` all: `∀x:A. B[x]` member: `t ∈ T` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_apply: `x[s1;s2]`
Lemmas referenced :  exists_wf or_wf all_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation rename sqequalHypSubstitution productElimination thin unionElimination cut hypothesis dependent_functionElimination hypothesisEquality because_Cache independent_functionElimination lemma_by_obid isectElimination sqequalRule lambdaEquality functionEquality applyEquality cumulativity universeEquality

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: 2016_05_15-PM-03_19_16
Last ObjectModification: 2015_12_27-PM-01_03_39

Theory : general

Home Index