---

Step * 1 of Lemma context-lookup-stable1


1. Gamma : mFOL() List
2. more : mFOL() List
3. x : ℕ||Gamma||
⊢ if (||more|| + ||Gamma||) - x + 1 <z ||more||
then more[(||more|| + ||Gamma||) - x + 1]
else Gamma[(||more|| + ||Gamma||) - x + 1 - ||more||]
fi  ~ Gamma[||Gamma|| - x + 1]
BY
{ AutoSplit }

---

Latex:

---

Latex:

1.  Gamma  :  mFOL()  List
2.  more  :  mFOL()  List
3.  x  :  \mBbbN{}||Gamma||
\mvdash{}  if  (||more||  +  ||Gamma||)  -  x  +  1  <z  ||more||
then  more[(||more||  +  ||Gamma||)  -  x  +  1]
else  Gamma[(||more||  +  ||Gamma||)  -  x  +  1  -  ||more||]
fi    \msim{}  Gamma[||Gamma||  -  x  +  1]


By

---

Latex:
AutoSplit

---

Home Index