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