---

Step * 1 1 of Lemma bag-reduce_wf


1. T : Type
2. zero : T
3. f : T ⟶ T ⟶ T
4. ∀[x,y:T].  (f[x;y] = f[y;x] ∈ T)
5. ∀[x,y,z:T].  (f[x;f[y;z]] = f[f[x;y];z] ∈ T)
6. as : T List
7. bs : T List
8. permutation(T;as;bs)
9. a1 : T List
10. a : T
⊢ reduce(λx,y. f[x;y];zero;a1 @ [a]) = reduce(λx,y. f[x;y];zero;[a / a1]) ∈ T
BY
{ (MoveToConcl 2
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "-3" 0 THENM Reduce 0)
   THEN Auto
   THEN (Reduce 0⋅ THEN RWO "4" 0 THEN Auto THEN RepeatFor 2 ((EqCD THEN Auto)))⋅)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  zero  :  T
3.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  \mforall{}[x,y:T].    (f[x;y]  =  f[y;x])
5.  \mforall{}[x,y,z:T].    (f[x;f[y;z]]  =  f[f[x;y];z])
6.  as  :  T  List
7.  bs  :  T  List
8.  permutation(T;as;bs)
9.  a1  :  T  List
10.  a  :  T
\mvdash{}  reduce(\mlambda{}x,y.  f[x;y];zero;a1  @  [a])  =  reduce(\mlambda{}x,y.  f[x;y];zero;[a  /  a1])


By

---

Latex:
(MoveToConcl  2
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "-3"  0  THENM  Reduce  0)
  THEN  Auto
  THEN  (Reduce  0\mcdot{}  THEN  RWO  "4"  0  THEN  Auto  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))\mcdot{})\mcdot{}

---

Home Index