---

Step * 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
⊢ a < b
BY
{ (InstLemma `lg-size-append` [⌈T⌉;⌈g1⌉;⌈g2⌉]⋅ 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-edge(lg-append(g1;g2);a;b)@i
9. 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
\mvdash{}  a  <  b


By

---

Latex:
(InstLemma  `lg-size-append`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}g1\mkleeneclose{};\mkleeneopen{}g2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index