---

Step * of Lemma lg-acyclic-remove

∀[T:Type]. ∀[g:LabeledGraph(T)].  ∀[i:ℕlg-size(g)]. lg-acyclic(lg-remove(g;i)) supposing lg-acyclic(g)
BY
{ ((Auto THEN RepeatFor 2 ((D 0 THEN Auto)))
   THEN Subst' lg-size(lg-remove(g;i)) = (lg-size(g) - 1) ∈ ℤ -2
   THEN RWW "lg-size-remove" 0
   THEN Auto
   THEN ((With ⌈if a <z i then a else a + 1 fi ⌉ (D 3)⋅ THENM D -1) THENA Auto)
   THEN BLemma `lg-connected-remove`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].
    \mforall{}[i:\mBbbN{}lg-size(g)].  lg-acyclic(lg-remove(g;i))  supposing  lg-acyclic(g)


By

---

Latex:
((Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))
  THEN  Subst'  lg-size(lg-remove(g;i))  =  (lg-size(g)  -  1)  -2
  THEN  RWW  "lg-size-remove"  0
  THEN  Auto
  THEN  ((With  \mkleeneopen{}if  a  <z  i  then  a  else  a  +  1  fi  \mkleeneclose{}  (D  3)\mcdot{}  THENM  D  -1)  THENA  Auto)
  THEN  BLemma  `lg-connected-remove`
  THEN  Auto)

---

Home Index