---

Step * 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-edge(lg-append(g1;g2);a;b)@i
9. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
⊢ a < b
BY
{ ((RWO "lg-edge-append" (-2) THENM D -2) THEN Auto) }

1
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

---

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-edge(lg-append(g1;g2);a;b)@i
9.  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))
\mvdash{}  a  <  b


By

---

Latex:
((RWO  "lg-edge-append"  (-2)  THENM  D  -2)  THEN  Auto)

---

Home Index