---

Step * 1 of Lemma name-morph-flip-face-map1


1. I : Cname List
2. y : nameset(I)
3. ∀v:nameset(I). ((¬(v = y ∈ Cname)) ⇒ (v ∈ nameset(I-[y])))
4. a : ℕ2
5. f : name-morph(I-[y];[])
6. v : nameset(I)
7. ¬(v = y ∈ Cname)
8. x : nameset(I)
⊢ (flip(((y:=a) o f);v) x) = (((y:=a) o flip(f;v)) x) ∈ extd-nameset([])
BY
{ (RepUR ``name-comp face-map compose name-morph-flip uext`` 0
   THEN (BoolCase ⌜(x =z y)⌝⋅ THENA Auto)
   THEN (Subst' isname(a) ~ ff 0 THENA (OnVar `a' IntSegCases THEN RepUR ``isname`` 0 THEN Auto))
   THEN Reduce 0
   THEN (BoolCase ⌜eq-cname(x;v)⌝⋅ THENA Auto)
   THEN Try ((RWO  "isname-name" 0 THENM Reduce 0))
   THEN Auto
   THEN (GenConcl ⌜(f x) = z ∈ ℕ2⌝⋅ THENA Auto)
   THEN SubsumeC ⌜ℕ2⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  y  :  nameset(I)
3.  \mforall{}v:nameset(I).  ((\mneg{}(v  =  y))  {}\mRightarrow{}  (v  \mmember{}  nameset(I-[y])))
4.  a  :  \mBbbN{}2
5.  f  :  name-morph(I-[y];[])
6.  v  :  nameset(I)
7.  \mneg{}(v  =  y)
8.  x  :  nameset(I)
\mvdash{}  (flip(((y:=a)  o  f);v)  x)  =  (((y:=a)  o  flip(f;v))  x)


By

---

Latex:
(RepUR  ``name-comp  face-map  compose  name-morph-flip  uext``  0
  THEN  (BoolCase  \mkleeneopen{}(x  =\msubz{}  y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Subst'  isname(a)  \msim{}  ff  0  THENA  (OnVar  `a'  IntSegCases  THEN  RepUR  ``isname``  0  THEN  Auto))
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x;v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((RWO    "isname-name"  0  THENM  Reduce  0))
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}(f  x)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\mBbbN{}2\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index