---

Step * 2 of Lemma name-morph-extend-face-map


1. I : Cname List
2. K : Cname List
3. i : ℕ2
4. f : name-morph(I;K)
5. x : nameset(I+)
6. ¬(x = fresh-cname(I) ∈ Cname)
⊢ (uext(f) ((fresh-cname(I):=i) x)) = (uext((fresh-cname(K):=i)) (f x)) ∈ extd-nameset(K)
BY
{ (RepUR ``face-map`` 0⋅
   THEN (AutoSplit THEN Try ((Unfold `guard` -3 THEN Auto)))
   THEN Try ((HypSubst' (-1) (-2) THEN Auto))
   THEN RepUR ``uext`` 0
   THEN (Subst' isname(x) ~ tt 0 THENA (RepeatFor 2 (DVar `x') THEN RepUR ``isname`` 0 THEN Auto))
   THEN Reduce 0
   THEN Assert ⌜x ∈ nameset(I)⌝⋅) }

1
.....assertion..... 
1. I : Cname List
2. K : Cname List
3. i : ℕ2
4. f : name-morph(I;K)
5. x : nameset(I+)
6. x ≠ fresh-cname(I)
7. ¬(x = fresh-cname(I) ∈ Cname)
⊢ x ∈ nameset(I)

2
1. I : Cname List
2. K : Cname List
3. i : ℕ2
4. f : name-morph(I;K)
5. x : nameset(I+)
6. x ≠ fresh-cname(I)
7. ¬(x = fresh-cname(I) ∈ Cname)
8. x ∈ nameset(I)
⊢ (f x) = if isname(f x) then if (f x =z fresh-cname(K)) then i else f x fi  else f x fi  ∈ extd-nameset(K)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  K  :  Cname  List
3.  i  :  \mBbbN{}2
4.  f  :  name-morph(I;K)
5.  x  :  nameset(I+)
6.  \mneg{}(x  =  fresh-cname(I))
\mvdash{}  (uext(f)  ((fresh-cname(I):=i)  x))  =  (uext((fresh-cname(K):=i))  (f  x))


By

---

Latex:
(RepUR  ``face-map``  0\mcdot{}
  THEN  (AutoSplit  THEN  Try  ((Unfold  `guard`  -3  THEN  Auto)))
  THEN  Try  ((HypSubst'  (-1)  (-2)  THEN  Auto))
  THEN  RepUR  ``uext``  0
  THEN  (Subst'  isname(x)  \msim{}  tt  0  THENA  (RepeatFor  2  (DVar  `x')  THEN  RepUR  ``isname``  0  THEN  Auto))
  THEN  Reduce  0
  THEN  Assert  \mkleeneopen{}x  \mmember{}  nameset(I)\mkleeneclose{}\mcdot{})

---

Home Index