---

Step * of Lemma lg-append_assoc

∀[T:Type]. ∀[a,b,c:LabeledGraph(T)].  (lg-append(a;lg-append(b;c)) ~ lg-append(lg-append(a;b);c))
BY
{ ((UnivCD THENA Auto)
   THEN (RepUR ``lg-append`` 0
         THEN (RWW "map_append_sq append_assoc_sq map-map" 0 THENA Auto)⋅
         THEN RepeatFor 2 (EqCD)
         THEN Try (Trivial))
   THEN RepUR ``compose`` 0⋅
   THEN (GenConcl ⌜c = L ∈ ((T × ℤ List × (ℤ List)) List)⌝⋅
         THENA (DVar `c' THEN DoSubsume THEN Try (Trivial) THEN Thin (-1) THEN Auto)⋅
         )⋅) }

1
1. T : Type
2. a : LabeledGraph(T)
3. b : LabeledGraph(T)
4. c : LabeledGraph(T)
5. L : (T × ℤ List × (ℤ List)) List@i
6. c = L ∈ ((T × ℤ List × (ℤ List)) List)@i
⊢ map(λx.let lbl,in,out = let lbl,in,out = x in 
         <lbl, map(λx.(x + lg-size(b));in), map(λx.(x + lg-size(b));out)> in 
         <lbl, map(λx.(x + lg-size(a));in), map(λx.(x + lg-size(a));out)>;L) 
~ map(λtr.let lbl,in,out = tr in 
          <lbl
          , map(λx.(x
                   + lg-size(a
                     @ map(λtr.let lbl,in,out = tr in 
                               <lbl, map(λx.(x + lg-size(a));in), map(λx.(x + lg-size(a));out)>;b)));in)
          , map(λx.(x
                   + lg-size(a
                     @ map(λtr.let lbl,in,out = tr in 
                               <lbl, map(λx.(x + lg-size(a));in), map(λx.(x + lg-size(a));out)>;b)));out)>;L)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b,c:LabeledGraph(T)].    (lg-append(a;lg-append(b;c))  \msim{}  lg-append(lg-append(a;b);c))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepUR  ``lg-append``  0
              THEN  (RWW  "map\_append\_sq  append\_assoc\_sq  map-map"  0  THENA  Auto)\mcdot{}
              THEN  RepeatFor  2  (EqCD)
              THEN  Try  (Trivial))
  THEN  RepUR  ``compose``  0\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}c  =  L\mkleeneclose{}\mcdot{}
              THENA  (DVar  `c'  THEN  DoSubsume  THEN  Try  (Trivial)  THEN  Thin  (-1)  THEN  Auto)\mcdot{}
              )\mcdot{})

---

Home Index