---

Step * 1 of Lemma lg-contains_antisymmetry


1. T : Type
2. g1 : LabeledGraph(T)
3. g2 : LabeledGraph(T)
4. g3 : LabeledGraph(T)
5. g4 : LabeledGraph(T)
6. g2 = lg-append(g3;lg-append(g1;g4)) ∈ LabeledGraph(T)
7. ga : LabeledGraph(T)
8. gb : LabeledGraph(T)
9. g1 = lg-append(ga;lg-append(g2;gb)) ∈ LabeledGraph(T)
10. (lg-size(ga) = 0 ∈ ℤ) ∧ (lg-size(gb) = 0 ∈ ℤ)
⊢ g1 = g2 ∈ LabeledGraph(T)
BY
{ ((Assert g1 = lg-append(lg-nil();lg-append(g2;lg-nil())) ∈ LabeledGraph(T) BY
          (RWO "lg-size-nil" (-1) THEN Auto))
   THEN RWW "lg-append-nil lg-nil-append" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g1  :  LabeledGraph(T)
3.  g2  :  LabeledGraph(T)
4.  g3  :  LabeledGraph(T)
5.  g4  :  LabeledGraph(T)
6.  g2  =  lg-append(g3;lg-append(g1;g4))
7.  ga  :  LabeledGraph(T)
8.  gb  :  LabeledGraph(T)
9.  g1  =  lg-append(ga;lg-append(g2;gb))
10.  (lg-size(ga)  =  0)  \mwedge{}  (lg-size(gb)  =  0)
\mvdash{}  g1  =  g2


By

---

Latex:
((Assert  g1  =  lg-append(lg-nil();lg-append(g2;lg-nil()))  BY
                (RWO  "lg-size-nil"  (-1)  THEN  Auto))
  THEN  RWW  "lg-append-nil  lg-nil-append"  (-1)
  THEN  Auto)

---

Home Index