---

Step * of Lemma combine-list-append

∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[as,bs:A List].
     combine-list(x,y.f[x;y];as @ bs) = combine-list(x,y.f[x;y];bs @ as) ∈ A supposing 0 < ||as @ bs||) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))
BY
{ (Auto
   THEN DVar `as'
   THEN All Reduce
   THEN Try (((EqCD THEN Auto) THEN RWO "append_back_nil" 0 THEN Auto)⋅)
   THEN DVar `bs'
   THEN Try ((Reduce 0 THEN (RWO "append_back_nil" 0 THEN Auto')⋅)⋅)
   THEN Unfold `combine-list` 0
   THEN Reduce 0
   THEN (InstLemma `list_accum_permute` [⌜A⌝;⌜A⌝;⌜λx.x⌝;⌜f⌝]⋅ THENA Auto)
   THEN RepUR ``so_apply`` -1
   THEN (RWO "-1" 0 THENA Auto)
   THEN Reduce 0
   THEN Subst' (f u u1) = (f u1 u) ∈ A 0
   THEN Auto
   THEN BackThruSomeHyp'⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as,bs:A  List].
          combine-list(x,y.f[x;y];as  @  bs)  =  combine-list(x,y.f[x;y];bs  @  as) 
          supposing  0  <  ||as  @  bs||)  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(Auto
  THEN  DVar  `as'
  THEN  All  Reduce
  THEN  Try  (((EqCD  THEN  Auto)  THEN  RWO  "append\_back\_nil"  0  THEN  Auto)\mcdot{})
  THEN  DVar  `bs'
  THEN  Try  ((Reduce  0  THEN  (RWO  "append\_back\_nil"  0  THEN  Auto')\mcdot{})\mcdot{})
  THEN  Unfold  `combine-list`  0
  THEN  Reduce  0
  THEN  (InstLemma  `list\_accum\_permute`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``so\_apply``  -1
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Subst'  (f  u  u1)  =  (f  u1  u)  0
  THEN  Auto
  THEN  BackThruSomeHyp'\mcdot{})

---

Home Index