---

Step * 1 of Lemma oal_neg_non_id_vals


1. a : LOSet
2. b : AbDGrp
3. ps : (|a| × |b|) List
4. ¬↑(e ∈b map(λx.(snd(x));ps))
5. map(λkv.<fst(kv), ~ (snd(kv))>;ps) ∈ (|a| × |b|) List
⊢ ¬↑(e ∈b map(λx.(snd(x));map(λkv.<fst(kv), ~ (snd(kv))>;ps)))
BY
{ TACTIC:(RWO "map_map" 0 THENA Auto) }

1
1. a : LOSet
2. b : AbDGrp
3. ps : (|a| × |b|) List
4. ¬↑(e ∈b map(λx.(snd(x));ps))
5. map(λkv.<fst(kv), ~ (snd(kv))>;ps) ∈ (|a| × |b|) List
⊢ ¬↑(e ∈b map((λx.(snd(x))) o (λkv.<fst(kv), ~ (snd(kv))>);ps))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDGrp
3.  ps  :  (|a|  \mtimes{}  |b|)  List
4.  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps))
5.  map(\mlambda{}kv.<fst(kv),  \msim{}  (snd(kv))>ps)  \mmember{}  (|a|  \mtimes{}  |b|)  List
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));map(\mlambda{}kv.<fst(kv),  \msim{}  (snd(kv))>ps)))


By

---

Latex:
TACTIC:(RWO  "map\_map"  0  THENA  Auto)

---

Home Index