---

Step * of Lemma lg-all-append

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀g1,g2:LabeledGraph(T).  (∀x∈lg-append(g1;g2).P[x] ⇐⇒ ∀x∈g1.P[x] ∧ ∀x∈g2.P[x])
BY
{ (Unfold `lg-all` 0
   THEN (UnivCD THENA Auto)
   THEN Dlg (-2)
   THEN Dlg (-1)
   THEN (Assert lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ BY
               (RepUR ``lg-size lg-append`` 0
                THEN RWW "length-append length-map-sq" 0
                THEN Try (Fold `lg-size` 0)
                THEN Auto))) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. g1 : LabeledGraph(T)
4. lg-size(g1) ∈ ℕ
5. g1 ∈ Top List
6. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
7. g2 : LabeledGraph(T)
8. lg-size(g2) ∈ ℕ
9. g2 ∈ Top List
10. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
⊢ ∀n:ℕlg-size(lg-append(g1;g2)). P[lg-label(lg-append(g1;g2);n)]
⇐⇒ (∀n:ℕlg-size(g1). P[lg-label(g1;n)]) ∧ (∀n:ℕlg-size(g2). P[lg-label(g2;n)])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}g1,g2:LabeledGraph(T).    (\mforall{}x\mmember{}lg-append(g1;g2).P[x]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x\mmember{}g1.P[x]  \mwedge{}  \mforall{}x\mmember{}g2.P[x])


By

---

Latex:
(Unfold  `lg-all`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Dlg  (-2)
  THEN  Dlg  (-1)
  THEN  (Assert  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))  BY
                          (RepUR  ``lg-size  lg-append``  0
                            THEN  RWW  "length-append  length-map-sq"  0
                            THEN  Try  (Fold  `lg-size`  0)
                            THEN  Auto)))

---

Home Index