---

Step * 1 1 1 of Lemma oal_dom_neg


1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
⊢ map(λz.(fst(z));ps) = map(λz.(fst(z));--ps) ∈ (|a| List)
BY
{ ((RWW "oal_neg_keys_invar" 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDGrp
3.  ps  :  |oal(a;b)|
\mvdash{}  map(\mlambda{}z.(fst(z));ps)  =  map(\mlambda{}z.(fst(z));--ps)


By

---

Latex:
((RWW  "oal\_neg\_keys\_invar"  0)  THEN  Auto)

---

Home Index