---

Step * of Lemma name-morph-flip_wf

∀[I:Cname List]. ∀[y:nameset(I)]. ∀[f:name-morph(I;[])].  (flip(f;y) ∈ name-morph(I;[]))
BY
{ ProveWfLemma }

1
1. I : Cname List
2. y : nameset(I)
3. f : name-morph(I;[])
⊢ λn.if eq-cname(n;y) then 1 - f n else f n fi  ∈ name-morph(I;[])

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[y:nameset(I)].  \mforall{}[f:name-morph(I;[])].    (flip(f;y)  \mmember{}  name-morph(I;[]))


By

---

Latex:
ProveWfLemma

---

Home Index