---

Step * 2 2 of Lemma lg-acyclic-well-founded


1. T : Type
2. ∀n:ℕ. ∀g:LabeledGraph(T).  (lg-size(g) < n ⇒ lg-acyclic(g) ⇒ SWellFounded(lg-edge(g;a;b)))
3. g : LabeledGraph(T)@i
4. SWellFounded(lg-edge(g;a;b))@i
⊢ lg-acyclic(g)
BY
{ ((InstLemma `rel_plus_strongwellfounded` [⌜ℕlg-size(g)⌝;⌜λa,b. lg-edge(g;a;b)⌝]⋅ THENA Auto)
   THEN Fold `lg-connected` (-1)
   THEN D -1
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. T : Type
2. ∀n:ℕ. ∀g:LabeledGraph(T).  (lg-size(g) < n ⇒ lg-acyclic(g) ⇒ SWellFounded(lg-edge(g;a;b)))
3. g : LabeledGraph(T)@i
4. SWellFounded(lg-edge(g;a;b))@i
5. f : ℕlg-size(g) ⟶ ℕ
6. ∀x,y:ℕlg-size(g).  (lg-connected(g;x;y) ⇒ f x < f y)
7. a : ℕlg-size(g)@i
8. lg-connected(g;a;a)@i
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}n:\mBbbN{}.  \mforall{}g:LabeledGraph(T).    (lg-size(g)  <  n  {}\mRightarrow{}  lg-acyclic(g)  {}\mRightarrow{}  SWellFounded(lg-edge(g;a;b)))
3.  g  :  LabeledGraph(T)@i
4.  SWellFounded(lg-edge(g;a;b))@i
\mvdash{}  lg-acyclic(g)


By

---

Latex:
((InstLemma  `rel\_plus\_strongwellfounded`  [\mkleeneopen{}\mBbbN{}lg-size(g)\mkleeneclose{};\mkleeneopen{}\mlambda{}a,b.  lg-edge(g;a;b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `lg-connected`  (-1)
  THEN  D  -1
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index