---

Step * 1 of Lemma bag-reduce_wf


1. T : Type
2. zero : T
3. f : T ⟶ T ⟶ T
4. Comm(T;λx,y. f[x;y])
5. Assoc(T;λx,y. f[x;y])
6. as : T List
7. bs : T List
8. permutation(T;as;bs)
⊢ reduce(λx,y. f[x;y];zero;as) = reduce(λx,y. f[x;y];zero;bs) ∈ T
BY
{ ((UnfoldTopAb 5 THEN Reduce 5 THEN UnfoldTopAb 4 THEN Reduce 4)
   THEN ((InstLemma `permutation-invariant` [⌜T⌝;⌜λ2as.reduce(λx,y. f[x;y];zero;as) = reduce(λx,y. f[x;y];zero;bs) ∈ T⌝]\000C⋅
          THENA Auto
          )
         THEN Try (((InstHyp [⌜as⌝;⌜bs⌝] (-1)⋅ THENA Auto) THEN BHyp -1  THEN Auto))
         THEN NthHypEq (-1)
         THEN EqCD
         THEN Auto
         THEN Thin (-1)
         THEN Try ((Reduce 0 THEN RWO "5" 0 THEN Auto THEN RepeatFor 2 ((EqCD THEN Auto)))))⋅
   ) }

1
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  zero  :  T
3.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  Comm(T;\mlambda{}x,y.  f[x;y])
5.  Assoc(T;\mlambda{}x,y.  f[x;y])
6.  as  :  T  List
7.  bs  :  T  List
8.  permutation(T;as;bs)
\mvdash{}  reduce(\mlambda{}x,y.  f[x;y];zero;as)  =  reduce(\mlambda{}x,y.  f[x;y];zero;bs)


By

---

Latex:
((UnfoldTopAb  5  THEN  Reduce  5  THEN  UnfoldTopAb  4  THEN  Reduce  4)
  THEN  ((InstLemma  `permutation-invariant`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}as.reduce(\mlambda{}x,y.  f[x;y];zero;as)
                                                                                                =  reduce(\mlambda{}x,y.  f[x;y];zero;bs)\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  Try  (((InstHyp  [\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto))
              THEN  NthHypEq  (-1)
              THEN  EqCD
              THEN  Auto
              THEN  Thin  (-1)
              THEN  Try  ((Reduce  0  THEN  RWO  "5"  0  THEN  Auto  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))))\mcdot{}
  )

---

Home Index