---

Step * 1 of Lemma name-morph-flip_wf


1. I : Cname List
2. y : nameset(I)
3. f : name-morph(I;[])
⊢ λn.if eq-cname(n;y) then 1 - f n else f n fi  ∈ name-morph(I;[])
BY
{ ((GenConcl ⌜f = g ∈ (nameset(I) ⟶ ℕ2)⌝⋅ THENA Auto)
   THEN SubsumeC ⌜nameset(I) ⟶ ℕ2⌝⋅
   THEN InstLemma `name-morph-nil` [⌜I⌝]⋅
   THEN Auto) }

1
1. I : Cname List
2. y : nameset(I)
3. f : name-morph(I;[])
4. g : nameset(I) ⟶ ℕ2
5. f = g ∈ (nameset(I) ⟶ ℕ2)
6. name-morph(I;[]) ≡ nameset(I) ⟶ ℕ2
7. n : nameset(I)
8. eq-cname(n;y) ∈ 𝔹
9. n = y ∈ Cname
⊢ 1 - g n ∈ ℕ2

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  y  :  nameset(I)
3.  f  :  name-morph(I;[])
\mvdash{}  \mlambda{}n.if  eq-cname(n;y)  then  1  -  f  n  else  f  n  fi    \mmember{}  name-morph(I;[])


By

---

Latex:
((GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}nameset(I)  {}\mrightarrow{}  \mBbbN{}2\mkleeneclose{}\mcdot{}
  THEN  InstLemma  `name-morph-nil`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index