---

Step * 1 of Lemma is-dag-remove


1. T : Type
2. g : LabeledGraph(T)
3. x : ℕlg-size(g)
4. ∀a,b:ℕlg-size(g).  (lg-edge(g;a;b) ⇒ a < b)
5. a : ℕlg-size(lg-remove(g;x))@i
6. b : ℕlg-size(lg-remove(g;x))@i
7. lg-edge(g;if a <z x then a else a + 1 fi ;if b <z x then b else b + 1 fi )
8. lg-size(lg-remove(g;x)) = (lg-size(g) - 1) ∈ ℤ
9. if a <z x then a else a + 1 fi  < if b <z x then b else b + 1 fi 
⊢ a < b
BY
{ ((SplitOnHypITE -1  THEN Auto) THEN SplitOnHypITE -2  THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  x  :  \mBbbN{}lg-size(g)
4.  \mforall{}a,b:\mBbbN{}lg-size(g).    (lg-edge(g;a;b)  {}\mRightarrow{}  a  <  b)
5.  a  :  \mBbbN{}lg-size(lg-remove(g;x))@i
6.  b  :  \mBbbN{}lg-size(lg-remove(g;x))@i
7.  lg-edge(g;if  a  <z  x  then  a  else  a  +  1  fi  ;if  b  <z  x  then  b  else  b  +  1  fi  )
8.  lg-size(lg-remove(g;x))  =  (lg-size(g)  -  1)
9.  if  a  <z  x  then  a  else  a  +  1  fi    <  if  b  <z  x  then  b  else  b  +  1  fi 
\mvdash{}  a  <  b


By

---

Latex:
((SplitOnHypITE  -1    THEN  Auto)  THEN  SplitOnHypITE  -2    THEN  Auto)\mcdot{}

---

Home Index