---

Step * of Lemma closure-well-founded-total

No Annotations
∀[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)))
  ⇒ (∀a,b:T.  (((R^*) a b) ∨ ((R^*) b a))) supposing 
        ((∀y,z:T.  ((∀x:T. ((¬(R x y)) ∧ (¬(R x z)))) ⇒ (y = z ∈ T))) and 
        one-one(T;T;R)))
BY
{ TACTIC:(Auto
          THEN ((InstLemma `wellfounded-minimal-field` [⌜T⌝; ⌜R⌝; ⌜a⌝])⋅ THENA Auto)
          THEN D -1
          THEN ((InstLemma `wellfounded-minimal-field` [⌜T⌝; ⌜R⌝; ⌜b⌝])⋅ THENA Auto)
          THEN D -1
          THEN ((Subst ⌜x1 = x ∈ T⌝ (-1))⋅ THENA (Auto THEN BackThruSomeHyp THEN Auto))
          THEN (Thin (-2))
          THEN Auto
          THEN (Thin (-1))
          THEN RenameTo `m' `x') }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.R x y)
4. ∀x,y:T.  Dec(R x y)
5. ∀y:T. ∃L:T List. ∀x:T. ((R x y) ⇒ (x ∈ L))
6. one-one(T;T;R)
7. ∀y,z:T.  ((∀x:T. ((¬(R x y)) ∧ (¬(R x z)))) ⇒ (y = z ∈ T))
8. a : T@i
9. b : T@i
10. m : T
11. (R^*) m a
12. ∀z:T. (¬(R z m))
13. (R^*) m b
⊢ ((R^*) a b) ∨ ((R^*) b a)

---

Latex:

---

Latex:
No  Annotations
\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{}a,b:T.    ((rel\_star(T;  R)  a  b)  \mvee{}  (rel\_star(T;  R)  b  a)))  supposing 
                ((\mforall{}y,z:T.    ((\mforall{}x:T.  ((\mneg{}(R  x  y))  \mwedge{}  (\mneg{}(R  x  z))))  {}\mRightarrow{}  (y  =  z)))  and 
                one-one(T;T;R)))


By

---

Latex:
TACTIC:(Auto
                THEN  ((InstLemma  `wellfounded-minimal-field`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}])\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  ((InstLemma  `wellfounded-minimal-field`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  ((Subst  \mkleeneopen{}x1  =  x\mkleeneclose{}  (-1))\mcdot{}  THENA  (Auto  THEN  BackThruSomeHyp  THEN  Auto))
                THEN  (Thin  (-2))
                THEN  Auto
                THEN  (Thin  (-1))
                THEN  RenameTo  `m'  `x')

---

Home Index