---

Step * of Lemma oal_neg_keys_invar

∀a:PosetSig. ∀b:GrpSig. ∀ps:(|a| × |b|) List.  (map(λz.(fst(z));--ps) = map(λz.(fst(z));ps) ∈ (|a| List))
BY
{ ((RepD THENM Unfold `oal_neg` 0) THENA Auto) }

1
1. a : PosetSig@i'
2. b : GrpSig@i'
3. ps : (|a| × |b|) List@i
⊢ map(λz.(fst(z));map(λkv.<fst(kv), ~ (snd(kv))>;ps)) = map(λz.(fst(z));ps) ∈ (|a| List)

---

Latex:

---

Latex:
\mforall{}a:PosetSig.  \mforall{}b:GrpSig.  \mforall{}ps:(|a|  \mtimes{}  |b|)  List.    (map(\mlambda{}z.(fst(z));--ps)  =  map(\mlambda{}z.(fst(z));ps))


By

---

Latex:
((RepD  THENM  Unfold  `oal\_neg`  0)  THENA  Auto)

---

Home Index