---

Step * of Lemma rename-one-extend-name-morph

No Annotations
∀I,K:Cname List. ∀f:name-morph(I;K). ∀x,y,z:Cname.
  ((¬(x ∈ I)) ⇒ (¬(z ∈ K)) ⇒ (¬(y ∈ K)) ⇒ ((f[x:=y] o rename-one-name(y;z)) = f[x:=z] ∈ name-morph([x / I];[z / K])))
BY
{ (Auto
   THEN (BLemma `name-morphs-equal` THEN Auto)
   THEN (FunExt  THENA Auto)
   THEN RepUR ``name-comp extend-name-morph rename-one-name uext`` 0
   THEN (BoolCase ⌜eq-cname(x1;x)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. x : Cname
5. y : Cname
6. z : Cname
7. ¬(x ∈ I)
8. ¬(z ∈ K)
9. ¬(y ∈ K)
10. x1 : nameset([x / I])
11. x1 = x ∈ Cname
⊢ if isname(y) then if eq-cname(y;y) then z else y fi  else y fi  = z ∈ extd-nameset([z / K])

2
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. x : Cname
5. y : Cname
6. z : Cname
7. ¬(x ∈ I)
8. ¬(z ∈ K)
9. ¬(y ∈ K)
10. x1 : nameset([x / I])
11. ¬(x1 = x ∈ Cname)
⊢ if isname(f x1) then if eq-cname(f x1;y) then z else f x1 fi  else f x1 fi  = (f x1) ∈ extd-nameset([z / K])

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}x,y,z:Cname.
    ((\mneg{}(x  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(z  \mmember{}  K))  {}\mRightarrow{}  (\mneg{}(y  \mmember{}  K))  {}\mRightarrow{}  ((f[x:=y]  o  rename-one-name(y;z))  =  f[x:=z]))


By

---

Latex:
(Auto
  THEN  (BLemma  `name-morphs-equal`  THEN  Auto)
  THEN  (FunExt    THENA  Auto)
  THEN  RepUR  ``name-comp  extend-name-morph  rename-one-name  uext``  0
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x1;x)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index