---

Step * 1 1 1 2 2 1 1 of Lemma mccarthy91_wf1


1. w : {92..102-}
⊢ mccarthy91(w) = 91 ∈ ℤ
BY
{ xxx(IntSegCases 1 THEN RW (AddrC [2] (TagC (mk_tag_term 1000))) 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  w  :  \{92..102\msupminus{}\}
\mvdash{}  mccarthy91(w)  =  91


By

---

Latex:
xxx(IntSegCases  1  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1000)))  0  THEN  Auto)xxx

---

Home Index