---

Step * of Lemma decidable__wellfound-bounded-exists

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
  ((∀x,y:T.  Dec(R x y))
  ⇒ (∀x:T. Dec(P[x]))
  ⇒ (∀y:T. ∃L:T List. ∀x:T. ((R x y) ⇒ (x ∈ L)))
  ⇒ WellFnd{i}(T;x,y.R x y)
  ⇒ (∀y:T. Dec(∃x:T. ((R+ x y) ∧ P[x]))))
BY
{ (RepeatFor 7 ((D 0 THENA Auto))
   THEN BackThruSomeHyp'
   THEN Auto
   THEN RenameTo `z' `j'
   THEN ((InstHyp [⌜z⌝] (-4))⋅ THENA Auto)
   THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [P] : T ⟶ ℙ
4. ∀x,y:T.  Dec(R x y)@i
5. ∀x:T. Dec(P[x])@i
6. ∀y:T. ∃L:T List. ∀x:T. ((R x y) ⇒ (x ∈ L))@i
7. ∀[P:T ⟶ ℙ]. ((∀j:T. ((∀k:T. ((R k j) ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T. P[n]})@i'
8. z : T@i
9. ∀k:T. ((R k z) ⇒ Dec(∃x:T. ((R+ x k) ∧ P[x])))@i
10. L : T List
11. ∀x:T. ((R x z) ⇒ (x ∈ L))
⊢ Dec(∃x:T. ((R+ x z) ∧ P[x]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:T.    Dec(R  x  y))
    {}\mRightarrow{}  (\mforall{}x:T.  Dec(P[x]))
    {}\mRightarrow{}  (\mforall{}y:T.  \mexists{}L:T  List.  \mforall{}x:T.  ((R  x  y)  {}\mRightarrow{}  (x  \mmember{}  L)))
    {}\mRightarrow{}  WellFnd\{i\}(T;x,y.R  x  y)
    {}\mRightarrow{}  (\mforall{}y:T.  Dec(\mexists{}x:T.  ((R\msupplus{}  x  y)  \mwedge{}  P[x]))))


By

---

Latex:
(RepeatFor  7  ((D  0  THENA  Auto))
  THEN  BackThruSomeHyp'
  THEN  Auto
  THEN  RenameTo  `z'  `j'
  THEN  ((InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  (-4))\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index