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 m
                                                                             of inl(rdm) =>
                                                                             (MxR rdm)
                                                                             inr(blm) =>
                                                                             let y,rdy,ygtr BR blm in 
                                                                             (T ygtr (MxR rdy))
                                                                            inr(MxB) =>
                                                                            case m
                                                                             of inl(rdm) =>
                                                                             let y,bly,ygtr RB rdm in 
                                                                             (T ygtr (MxB bly))
                                                                             inr(blm) =>
                                                                             (MxB 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