---

Step * 2 of Lemma lookup_oal_neg


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|
BY
{ ((D 4 THEN Reduce 0 
THEN SplitOnConclITE) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  DSet
2.  b  :  IGroup
3.  k  :  |a|
4.  p  :  |a|  \mtimes{}  |b|
5.  ps  :  (|a|  \mtimes{}  |b|)  List
6.  ((--ps)[k])  =  (\msim{}  (ps[k]))
\mvdash{}  ((--[p  /  ps])[k])  =  (\msim{}  ([p  /  ps][k]))


By

---

Latex:
((D  4  THEN  Reduce  0 
THEN  SplitOnConclITE)  THEN  Auto)

---

Home Index