---

Step * 1 1 1 1 1 1 2 1 1 of Lemma local-class-single-valued-class-except


1. f : Name ─→ Type
2. L : Message(f) List@i
3. m : Message(f)@i
4. v : ℕ@i
⊢ if v <z v then L[v] else [m][v - v] fi  ~ m
BY
{ (AutoSplit THEN Subst' v - v ~ 0 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  L  :  Message(f)  List@i
3.  m  :  Message(f)@i
4.  v  :  \mBbbN{}@i
\mvdash{}  if  v  <z  v  then  L[v]  else  [m][v  -  v]  fi    \msim{}  m


By

---

Latex:
(AutoSplit  THEN  Subst'  v  -  v  \msim{}  0  0  THEN  Reduce  0  THEN  Auto)

---

Home Index