---

Step * of Lemma test-infinite-domain-example

∀[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
{ (EvidenceTac ⌜λTrans,Irr,Unbdd,MxEx. let m = fst(MxEx) in
                                        let bounds = snd(MxEx) in
                                        let y,ygtr = Unbdd m 
                                        in let loop = Trans m y m ygtr in
                                            let F = λx.(Irr m (loop x)) in
                                            F (inl (bounds y (λeq.(F (inr eq )))))⌝⋅
   THENA Auto
   ) }

---

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:
(EvidenceTac  \mkleeneopen{}\mlambda{}Trans,Irr,Unbdd,MxEx.  let  m  =  fst(MxEx)  in
                                                                            let  bounds  =  snd(MxEx)  in
                                                                            let  y,ygtr  =  Unbdd  m 
                                                                            in  let  loop  =  Trans  m  y  m  ygtr  in
                                                                                    let  F  =  \mlambda{}x.(Irr  m  (loop  x))  in
                                                                                    F  (inl  (bounds  y  (\mlambda{}eq.(F  (inr  eq  )))))\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index