Step * 1 1 1 of Lemma oal_neg_non_id_vals


1. LOSet
2. AbDGrp
3. ps (|a| × |b|) List
4. ¬↑(e ∈b map(λx.(snd(x));ps))
⊢ ¬↑(e ∈b map((λx.(snd(x))) kv.<fst(kv), (snd(kv))>);ps))
BY
Eval ``compose`` }

1
1. LOSet
2. AbDGrp
3. ps (|a| × |b|) List
4. ¬↑(e ∈b map(λx.(snd(x));ps))
⊢ ¬↑(e ∈b map(λx.(~ (snd(x)));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))
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map((\mlambda{}x.(snd(x)))  o  (\mlambda{}kv.<fst(kv),  \msim{}  (snd(kv))>);ps))


By


Latex:
Eval  ``compose``  0




Home Index