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:  Q or: P ∨ Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  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