---

Step * 2 of Lemma extend-name-morph_wf

.....set predicate..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
⊢ ∀i,j:nameset([z1 / I]).
    ((↑isname((λx.if eq-cname(x;z1) then z2 else f x fi ) i))
    ⇒ (↑isname((λx.if eq-cname(x;z1) then z2 else f x fi ) j))
    ⇒ (((λx.if eq-cname(x;z1) then z2 else f x fi ) i)
       = ((λx.if eq-cname(x;z1) then z2 else f x fi ) j)
       ∈ extd-nameset([z2 / J]))
    ⇒ (i = j ∈ nameset([z1 / I])))
BY
{ ((Assert nameset(J) ⊆r extd-nameset([z2 / J]) BY
          (UseTrans ⌜nameset([z2 / J])⌝⋅ THEN Auto))
   THEN Reduce 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (BoolCase ⌜eq-cname(i;z1)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜eq-cname(j;z1)⌝⋅ THENA Auto)
   THEN (Subst' isname(z2) ~ tt 0 THENA (DVar `z2' THEN RepUR ``isname`` 0 THEN Auto))
   THEN (Subst' isname(z1) ~ tt 0 THENA (DVar `z1' THEN RepUR ``isname`` 0 THEN Auto))
   THEN Reduce 0
   THEN Try ((Assert j ∈ nameset(I) BY
                    OnVar `j' (\h. (D h THEN (RW ListC (h+1) THENA Auto) THEN D h+1 THEN Complete (Auto)))⋅))
   THEN Try ((Assert i ∈ nameset(I) BY
                    OnVar `i' (\h. (D h THEN (RW ListC (h+1) THENA Auto) THEN D h+1 THEN Complete (Auto)))⋅))
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN Try ((FLemma `assert-isname` [-1] THENA Auto))))
   THEN (Assert z2 ∈ extd-nameset([z2 / J]) BY
               (SubsumeC ⌜nameset([z2 / J])⌝⋅ THEN Auto))
   THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
7. nameset(J) ⊆r extd-nameset([z2 / J])
8. i : nameset([z1 / I])
9. j : nameset([z1 / I])
10. ¬(j = z1 ∈ Cname)
11. i = z1 ∈ Cname
12. j ∈ nameset(I)
13. True
14. ↑isname(f j)
15. f j ∈ nameset(J)
16. z2 ∈ extd-nameset([z2 / J])
17. z2 = (f j) ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])

2
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
7. nameset(J) ⊆r extd-nameset([z2 / J])
8. i : nameset([z1 / I])
9. ¬(i = z1 ∈ Cname)
10. j : nameset([z1 / I])
11. j = z1 ∈ Cname
12. i ∈ nameset(I)
13. ↑isname(f i)
14. f i ∈ nameset(J)
15. True
16. z2 ∈ extd-nameset([z2 / J])
17. (f i) = z2 ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])

3
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
7. nameset(J) ⊆r extd-nameset([z2 / J])
8. i : nameset([z1 / I])
9. ¬(i = z1 ∈ Cname)
10. j : nameset([z1 / I])
11. ¬(j = z1 ∈ Cname)
12. j ∈ nameset(I)
13. i ∈ nameset(I)
14. ↑isname(f i)
15. f i ∈ nameset(J)
16. ↑isname(f j)
17. f j ∈ nameset(J)
18. z2 ∈ extd-nameset([z2 / J])
19. (f i) = (f j) ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])

---

Latex:

---

Latex:
.....set  predicate..... 
1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  z1  :  Cname
5.  z2  :  Cname
6.  \mneg{}(z2  \mmember{}  J)
\mvdash{}  \mforall{}i,j:nameset([z1  /  I]).
        ((\muparrow{}isname((\mlambda{}x.if  eq-cname(x;z1)  then  z2  else  f  x  fi  )  i))
        {}\mRightarrow{}  (\muparrow{}isname((\mlambda{}x.if  eq-cname(x;z1)  then  z2  else  f  x  fi  )  j))
        {}\mRightarrow{}  (((\mlambda{}x.if  eq-cname(x;z1)  then  z2  else  f  x  fi  )  i)
              =  ((\mlambda{}x.if  eq-cname(x;z1)  then  z2  else  f  x  fi  )  j))
        {}\mRightarrow{}  (i  =  j))


By

---

Latex:
((Assert  nameset(J)  \msubseteq{}r  extd-nameset([z2  /  J])  BY
                (UseTrans  \mkleeneopen{}nameset([z2  /  J])\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Reduce  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (BoolCase  \mkleeneopen{}eq-cname(i;z1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}eq-cname(j;z1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Subst'  isname(z2)  \msim{}  tt  0  THENA  (DVar  `z2'  THEN  RepUR  ``isname``  0  THEN  Auto))
  THEN  (Subst'  isname(z1)  \msim{}  tt  0  THENA  (DVar  `z1'  THEN  RepUR  ``isname``  0  THEN  Auto))
  THEN  Reduce  0
  THEN  Try  ((Assert  j  \mmember{}  nameset(I)  BY
                                    OnVar  `j'  (\mbackslash{}h.  (D  h
                                                                    THEN  (RW  ListC  (h+1)  THENA  Auto)
                                                                    THEN  D  h+1
                                                                    THEN  Complete  (Auto)))\mcdot{}))
  THEN  Try  ((Assert  i  \mmember{}  nameset(I)  BY
                                    OnVar  `i'  (\mbackslash{}h.  (D  h
                                                                    THEN  (RW  ListC  (h+1)  THENA  Auto)
                                                                    THEN  D  h+1
                                                                    THEN  Complete  (Auto)))\mcdot{}))
  THEN  RepeatFor  2  (((D  0  THENA  Auto)  THEN  Try  ((FLemma  `assert-isname`  [-1]  THENA  Auto))))
  THEN  (Assert  z2  \mmember{}  extd-nameset([z2  /  J])  BY
                          (SubsumeC  \mkleeneopen{}nameset([z2  /  J])\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Auto)

---

Home Index