---

Step * of Lemma lookup_oal_neg

∀a:DSet. ∀b:IGroup. ∀k:|a|. ∀ps:(|a| × |b|) List.  (((--ps)[k]) = (~ (ps[k])) ∈ |b|)
BY
{ (InductionOnListA THEN Reduce 0) }

1
1. a : DSet
2. b : IGroup
3. k : |a|
⊢ e = (~ e) ∈ |b|

2
1. a : DSet
2. b : IGroup
3. k : |a|
4. p : |a| × |b|
5. ps : (|a| × |b|) List
6. ((--ps)[k]) = (~ (ps[k])) ∈ |b|
⊢ ((--[p / ps])[k]) = (~ ([p / ps][k])) ∈ |b|

---

Latex:

---

Latex:
\mforall{}a:DSet.  \mforall{}b:IGroup.  \mforall{}k:|a|.  \mforall{}ps:(|a|  \mtimes{}  |b|)  List.    (((--ps)[k])  =  (\msim{}  (ps[k])))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0)

---

Home Index