---

Step * of Lemma lg-acyclic-has-source

∀[T:Type]. ∀g:LabeledGraph(T). (∃i:ℕlg-size(g). (↑lg-is-source(g;i))) supposing (lg-acyclic(g) and 0 < lg-size(g))
BY
{ (Auto
   THEN SupposeNot
   THEN (Assert ∀i:ℕlg-size(g). ∃j:ℕlg-size(g). lg-edge(g;j;i) BY
               (Auto
                THEN SupposeNot
                THEN D -3
                THEN With ⌜i⌝ (D 0)⋅
                THEN Auto
                THEN RepUR ``lg-is-source`` 0
                THEN AutoSplit
                THEN MoveToConcl (-2)
                THEN Unfold `lg-edge` 0
                THEN GenConclAtAddr [2;1;1]
                THEN D -2
                THEN Reduce 0
                THEN Auto))) }

1
1. [T] : Type
2. g : LabeledGraph(T)@i
3. 0 < lg-size(g)
4. lg-acyclic(g)
5. ¬(∃i:ℕlg-size(g). (↑lg-is-source(g;i)))
6. ∀i:ℕlg-size(g). ∃j:ℕlg-size(g). lg-edge(g;j;i)
⊢ ∃i:ℕlg-size(g). (↑lg-is-source(g;i))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}g:LabeledGraph(T)
        (\mexists{}i:\mBbbN{}lg-size(g).  (\muparrow{}lg-is-source(g;i)))  supposing  (lg-acyclic(g)  and  0  <  lg-size(g))


By

---

Latex:
(Auto
  THEN  SupposeNot
  THEN  (Assert  \mforall{}i:\mBbbN{}lg-size(g).  \mexists{}j:\mBbbN{}lg-size(g).  lg-edge(g;j;i)  BY
                          (Auto
                            THEN  SupposeNot
                            THEN  D  -3
                            THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto
                            THEN  RepUR  ``lg-is-source``  0
                            THEN  AutoSplit
                            THEN  MoveToConcl  (-2)
                            THEN  Unfold  `lg-edge`  0
                            THEN  GenConclAtAddr  [2;1;1]
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto)))

---

Home Index