### Nuprl Lemma : 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` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` so_apply: `x[s1;s2]` and: `P ∧ Q` guard: `{T}`
Lemmas referenced :  subtype_rel_self istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt sqequalHypSubstitution productElimination thin unionElimination cut hypothesis dependent_functionElimination hypothesisEquality sqequalRule productIsType universeIsType unionIsType functionIsType because_Cache applyEquality instantiate introduction extract_by_obid isectElimination universeEquality inhabitedIsType independent_functionElimination

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: 2020_05_20-AM-08_19_34
Last ObjectModification: 2020_02_01-AM-11_42_37

Theory : general

Home Index