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 ((D 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 <then else fi ⌉ (D 3)⋅ THENM -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