---

Step * of Lemma face-maps-commute

No Annotations
∀I:Cname List. ∀x:nameset(I). ∀i:ℕ2. ∀y:nameset(I). ∀j:ℕ2.
  ((¬(x = y ∈ Cname)) ⇒ (((x:=i) o (y:=j)) = ((y:=j) o (x:=i)) ∈ name-morph(I;I-[x; y])))
BY
{ (Auto
   THEN (Assert (y:=j) ∈ name-morph(I-[x];I-[x; y]) BY
               (SubsumeC ⌜name-morph(I-[x];I-[x]-[y])⌝⋅ THEN Auto THEN RWO "list-diff2" 0 THEN Auto))
   ) }

1
1. I : Cname List
2. x : nameset(I)
3. i : ℕ2
4. y : nameset(I)
5. j : ℕ2
6. ¬(x = y ∈ Cname)
7. (y:=j) ∈ name-morph(I-[x];I-[x; y])
⊢ ((x:=i) o (y:=j)) = ((y:=j) o (x:=i)) ∈ name-morph(I;I-[x; y])

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Cname  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}y:nameset(I).  \mforall{}j:\mBbbN{}2.
    ((\mneg{}(x  =  y))  {}\mRightarrow{}  (((x:=i)  o  (y:=j))  =  ((y:=j)  o  (x:=i))))


By

---

Latex:
(Auto
  THEN  (Assert  (y:=j)  \mmember{}  name-morph(I-[x];I-[x;  y])  BY
                          (SubsumeC  \mkleeneopen{}name-morph(I-[x];I-[x]-[y])\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  RWO  "list-diff2"  0  THEN  Auto))
  )

---

Home Index