---

Step * of 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)
BY
{ xxxNormalizeExtractTo (ioid Obid: red-black-example)⌜λD,T,I,RB,BR,mx. let m,MxRorB = mx 
                                                                        in case MxRorB
                                                                            of inl(MxR) =>
                                                                            case D m
                                                                             of inl(rdm) =>
                                                                             I m (MxR m rdm)
                                                                             | inr(blm) =>
                                                                             let y,rdy,ygtr = BR m blm in 
                                                                             I m (T m y m ygtr (MxR y rdy))
                                                                            | inr(MxB) =>
                                                                            case D m
                                                                             of inl(rdm) =>
                                                                             let y,bly,ygtr = RB m rdm in 
                                                                             I m (T m y m ygtr (MxB y bly))
                                                                             | inr(blm) =>
                                                                             I m (MxB m blm)⌝ 1000 []⋅xxx }

---

Latex:

---

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)


By

---

Latex:
xxxNormalizeExtractTo  (ioid  Obid:  red-black-example)\mkleeneopen{}\mlambda{}D,T,I,RB,BR,mx.  let  m,MxRorB  =  mx 
                                                                                                                                            in  case  MxRorB
                                                                                                                                                    of  inl(MxR)  =>
                                                                                                                                                    case  D  m
                                                                                                                                                      of  inl(rdm)  =>
                                                                                                                                                      I  m  (MxR  m  rdm)
                                                                                                                                                      |  inr(blm)  =>
                                                                                                                                                      let  y,rdy,ygtr  =  BR  m 
                                                                                                                                                                                        blm  in 
                                                                                                                                                      I  m 
                                                                                                                                                      (T  m  y  m  ygtr 
                                                                                                                                                        (MxR  y  rdy))
                                                                                                                                                    |  inr(MxB)  =>
                                                                                                                                                    case  D  m
                                                                                                                                                      of  inl(rdm)  =>
                                                                                                                                                      let  y,bly,ygtr  =  RB  m 
                                                                                                                                                                                        rdm  in 
                                                                                                                                                      I  m 
                                                                                                                                                      (T  m  y  m  ygtr 
                                                                                                                                                        (MxB  y  bly))
                                                                                                                                                      |  inr(blm)  =>
                                                                                                                                                      I  m  (MxB  m  blm)\mkleeneclose{}  1000  []\mcdot{}\000Cxxx

---

Home Index