---

Step * 1 1 1 of Lemma is-dag-append


1. T : Type
2. g1 : LabeledGraph(T)
3. g2 : LabeledGraph(T)
4. ∀a,b:ℕlg-size(g1).  (lg-edge(g1;a;b) ⇒ a < b)
5. ∀a,b:ℕlg-size(g2).  (lg-edge(g2;a;b) ⇒ a < b)
6. a : ℕlg-size(lg-append(g1;g2))@i
7. b : ℕlg-size(lg-append(g1;g2))@i
8. lg-size(g1) ≤ a
9. lg-size(g1) ≤ b
10. lg-edge(g2;a - lg-size(g1);b - lg-size(g1))
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
⊢ a < b
BY
{ (FHyp 5 [-2] THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g1  :  LabeledGraph(T)
3.  g2  :  LabeledGraph(T)
4.  \mforall{}a,b:\mBbbN{}lg-size(g1).    (lg-edge(g1;a;b)  {}\mRightarrow{}  a  <  b)
5.  \mforall{}a,b:\mBbbN{}lg-size(g2).    (lg-edge(g2;a;b)  {}\mRightarrow{}  a  <  b)
6.  a  :  \mBbbN{}lg-size(lg-append(g1;g2))@i
7.  b  :  \mBbbN{}lg-size(lg-append(g1;g2))@i
8.  lg-size(g1)  \mleq{}  a
9.  lg-size(g1)  \mleq{}  b
10.  lg-edge(g2;a  -  lg-size(g1);b  -  lg-size(g1))
11.  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))
\mvdash{}  a  <  b


By

---

Latex:
(FHyp  5  [-2]  THEN  Auto')

---

Home Index