---

Step * of 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)
BY
{ (EvidenceTac ⌜λD,T,I,RB,BR,mx. let m = fst(mx) in
                                  let Im = I m in
                                  let mRorB = D m in
                                  let RorBFinite = snd(mx) in
                                  let RIsFinite = isl(RorBFinite) in
                                  let mBoundsRed = outl(RorBFinite) in
                                  let mBoundsBlack = outr(RorBFinite) in
                                  let mIsRed = isl(mRorB) in
                                  let mRed = outl(mRorB) in
                                  let mBlack = outr(mRorB) in
                                  let loop = λy.(T m y m) in
                                  if RIsFinite
                                    then if hd([mIsRed])
                                         then Im (mBoundsRed m mRed)
                                         else let y,rdy,ygtr = BR m mBlack in 
                                              Im (loop y ygtr (mBoundsRed y rdy))
                                         fi 
                                  if mIsRed then let y,bly,ygtr = RB m mRed in Im (loop y ygtr (mBoundsBlack y bly))
                                  else Im (mBoundsBlack m mBlack)
                                  fi ⌝⋅
   THENA Auto
   )⋅ }

---

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:
(EvidenceTac  \mkleeneopen{}\mlambda{}D,T,I,RB,BR,mx.  let  m  =  fst(mx)  in
                                                                let  Im  =  I  m  in
                                                                let  mRorB  =  D  m  in
                                                                let  RorBFinite  =  snd(mx)  in
                                                                let  RIsFinite  =  isl(RorBFinite)  in
                                                                let  mBoundsRed  =  outl(RorBFinite)  in
                                                                let  mBoundsBlack  =  outr(RorBFinite)  in
                                                                let  mIsRed  =  isl(mRorB)  in
                                                                let  mRed  =  outl(mRorB)  in
                                                                let  mBlack  =  outr(mRorB)  in
                                                                let  loop  =  \mlambda{}y.(T  m  y  m)  in
                                                                if  RIsFinite
                                                                    then  if  hd([mIsRed])
                                                                              then  Im  (mBoundsRed  m  mRed)
                                                                              else  let  y,rdy,ygtr  =  BR  m  mBlack  in 
                                                                                        Im  (loop  y  ygtr  (mBoundsRed  y  rdy))
                                                                              fi 
                                                                if  mIsRed
                                                                    then  let  y,bly,ygtr  =  RB  m  mRed  in 
                                                                              Im  (loop  y  ygtr  (mBoundsBlack  y  bly))
                                                                else  Im  (mBoundsBlack  m  mBlack)
                                                                fi  \mkleeneclose{}\mcdot{}
  THENA  Auto
  )\mcdot{}

---

Home Index