---

Step * 1 of Lemma lg-append_assoc


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)
BY
{ (Thin (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN EqCD
   THEN Try (Trivial)
   THEN DVar `u'
   THEN DVar `u2'
   THEN Reduce 0
   THEN RepeatFor 2 (EqCD)
   THEN All Thin
   THEN ListInd (-1)
   THEN Reduce 0
   THEN EqCD
   THEN Try (Trivial)
   THEN Unfold `lg-size` 0
   THEN RWW "length-append length-map-sq" 0
   THEN Auto
   THEN Using [`A',⌈Top⌉] Auto⋅
   THEN (RepeatFor 2 (DVar `a') THEN Trivial)⋅)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  LabeledGraph(T)
3.  b  :  LabeledGraph(T)
4.  c  :  LabeledGraph(T)
5.  L  :  (T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List@i
6.  c  =  L@i
\mvdash{}  map(\mlambda{}x.let  lbl,in,out  =  let  lbl,in,out  =  x  in 
                  <lbl,  map(\mlambda{}x.(x  +  lg-size(b));in),  map(\mlambda{}x.(x  +  lg-size(b));out)>  in 
                  <lbl,  map(\mlambda{}x.(x  +  lg-size(a));in),  map(\mlambda{}x.(x  +  lg-size(a));out)>L) 
\msim{}  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                    <lbl
                    ,  map(\mlambda{}x.(x
                                      +  lg-size(a
                                          @  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                                                              <lbl,  map(\mlambda{}x.(x  +  lg-size(a));in),  map(\mlambda{}x.(x  +  lg-size(a));out)>
                                                      b)));in)
                    ,  map(\mlambda{}x.(x
                                      +  lg-size(a
                                          @  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                                                              <lbl,  map(\mlambda{}x.(x  +  lg-size(a));in),  map(\mlambda{}x.(x  +  lg-size(a));out)>
                                                      b)));out)>L)


By

---

Latex:
(Thin  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  DVar  `u'
  THEN  DVar  `u2'
  THEN  Reduce  0
  THEN  RepeatFor  2  (EqCD)
  THEN  All  Thin
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  Unfold  `lg-size`  0
  THEN  RWW  "length-append  length-map-sq"  0
  THEN  Auto
  THEN  Using  [`A',\mkleeneopen{}Top\mkleeneclose{}]  Auto\mcdot{}
  THEN  (RepeatFor  2  (DVar  `a')  THEN  Trivial)\mcdot{})\mcdot{}

---

Home Index