---

Step * of Lemma wellfounded-minimal-field

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (WellFnd{i}(T;x,y.R x y)
  ⇒ (∀x,y:T.  Dec(R x y))
  ⇒ (∀y:T. ∃L:T List. ∀x:T. ((R x y) ⇒ (x ∈ L)))
  ⇒ (∀y:T. ∃x:T. (((R^*) x y) ∧ (∀z:T. (¬(R z x))))))
BY
{ (Auto
   THEN ((InstLemma `wellfounded-minimal` [⌜T⌝; ⌜R⌝; ⌜λx.True⌝; ⌜y⌝])⋅ THENA Auto)
   THEN All Reduce
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.R x y)@i'
4. ∀x,y:T.  Dec(R x y)@i
5. ∀y:T. ∃L:T List. ∀x:T. ((R x y) ⇒ (x ∈ L))@i
6. y : T@i
7. y@0 : T
8. True
9. (R^*) y@0 y
10. ∀x:T. ((R+ x y@0) ⇒ (¬True))
11. (R^*) y@0 y
12. z : T@i
⊢ ¬(R z y@0)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((InstLemma  `wellfounded-minimal`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.True\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index