---

Step * of Lemma infinite-domain-example-ext

∀[A,D:Type]. ∀[R,Eq:D ⟶ D ⟶ ℙ].
  ((∀x,y,z:D.  (R[x;y] ⇒ (R[y;z] ∨ Eq[y;z]) ⇒ R[x;z]))
  ⇒ (∀x:D. (R[x;x] ⇒ A))
  ⇒ (∀x:D. ∃y:D. R[x;y])
  ⇒ (∃m:D. ∀x:D. ((Eq[x;m] ⇒ A) ⇒ R[x;m]))
  ⇒ A)
BY
{ xxxNormalizeExtractTo (ioid Obid: infinite-domain-example)  
⌜λTrans,Irr,Unbdd,MxEx. let m,bounds = MxEx 
                        in let y,ygtr = Unbdd m 
                           in Irr m (Trans m y m ygtr (inl (bounds y (λeq.(Irr m (Trans m y m ygtr (inr eq )))))))⌝
 1000 []⋅xxx }

---

Latex:

---

Latex:
\mforall{}[A,D:Type].  \mforall{}[R,Eq:D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  (R[y;z]  \mvee{}  Eq[y;z])  {}\mRightarrow{}  R[x;z]))
    {}\mRightarrow{}  (\mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A))
    {}\mRightarrow{}  (\mforall{}x:D.  \mexists{}y:D.  R[x;y])
    {}\mRightarrow{}  (\mexists{}m:D.  \mforall{}x:D.  ((Eq[x;m]  {}\mRightarrow{}  A)  {}\mRightarrow{}  R[x;m]))
    {}\mRightarrow{}  A)


By

---

Latex:
xxxNormalizeExtractTo  (ioid  Obid:  infinite-domain-example)   
\mkleeneopen{}\mlambda{}Trans,Irr,Unbdd,MxEx.  let  m,bounds  =  MxEx 
                                                in  let  y,ygtr  =  Unbdd  m 
                                                      in  Irr  m 
                                                            (Trans  m  y  m  ygtr 
                                                              (inl  (bounds  y  (\mlambda{}eq.(Irr  m  (Trans  m  y  m  ygtr  (inr  eq  )))))))\mkleeneclose{}
  1000  []\mcdot{}xxx

---

Home Index