---

Step * 1 1 of Lemma face-map_wf

.....subterm..... T:t
1:n
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : nameset([x / L])
⊢ if (z =z x) then p else z fi  ∈ extd-nameset(L)
BY
{ (D -1 THEN (BoolCase ⌜(z =z x)⌝⋅ THENA Auto)) }

1
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : Cname
5. (z ∈ [x / L])
6. z = x ∈ ℤ
⊢ p ∈ extd-nameset(L)

2
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : Cname
5. z ≠ x
6. (z ∈ [x / L])
⊢ z ∈ extd-nameset(L)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  z  :  nameset([x  /  L])
\mvdash{}  if  (z  =\msubz{}  x)  then  p  else  z  fi    \mmember{}  extd-nameset(L)


By

---

Latex:
(D  -1  THEN  (BoolCase  \mkleeneopen{}(z  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index