---

Step * of Lemma lg-label-append

∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. ∀[x:ℕlg-size(lg-append(g1;g2))].
  (lg-label(lg-append(g1;g2);x) ~ if x <z lg-size(g1) then lg-label(g1;x) else lg-label(g2;x - lg-size(g1)) fi )
BY
{ ((UnivCD THENA Auto) THEN Dlg (-3) THEN Dlg (-2)) }

1
1. T : Type
2. g1 : LabeledGraph(T)
3. lg-size(g1) ∈ ℕ
4. g1 ∈ Top List
5. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
6. g2 : LabeledGraph(T)
7. lg-size(g2) ∈ ℕ
8. g2 ∈ Top List
9. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
10. x : ℕlg-size(lg-append(g1;g2))
⊢ lg-label(lg-append(g1;g2);x) ~ if x <z lg-size(g1) then lg-label(g1;x) else lg-label(g2;x - lg-size(g1)) fi 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g1,g2:LabeledGraph(T)].  \mforall{}[x:\mBbbN{}lg-size(lg-append(g1;g2))].
    (lg-label(lg-append(g1;g2);x)  \msim{}  if  x  <z  lg-size(g1)
    then  lg-label(g1;x)
    else  lg-label(g2;x  -  lg-size(g1))
    fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Dlg  (-3)  THEN  Dlg  (-2))

---

Home Index