---

Step * of Lemma maybe-new_wf

∀[s:Name]. ∀[avoid:Name List].  (maybe-new(s;avoid) ∈ {s':Name| ¬(s' ∈ avoid)} )
BY
{ ProveWfLemma }

1
1. s : Name
2. avoid : Name List
3. (s ∈ avoid)
⊢ s @ nat-to-str(mu(λn.(¬bs @ nat-to-str(n) ∈b avoid))) ∈ {s':Name| ¬(s' ∈ avoid)} 

---

Latex:

---

Latex:
\mforall{}[s:Name].  \mforall{}[avoid:Name  List].    (maybe-new(s;avoid)  \mmember{}  \{s':Name|  \mneg{}(s'  \mmember{}  avoid)\}  )


By

---

Latex:
ProveWfLemma

---

Home Index