---

Step * 1 1 2 of Lemma maybe_new_var-is-null


1. a : varname()
2. vs : varname() List
3. ¬(vs = [] ∈ (varname() List))
4. a ∈ Base
5. t : Atom
6. if a is an atom then a otherwise fst(a) = t ∈ Atom
7. i : ℤ
8. v1 : {b:varname()| var-num(t;b) = i ∈ ℤ} 
9. (v1 ∈ vs)
10. var-num(t;v1) = i ∈ ℤ
11. (∀y∈vs.var-num(t;y) ≤ i)
12. <t, i> = nullvar() ∈ varname()
13. ¬i < 0
14. if <t, i> is an atom then 0 otherwise 1 = if nullvar() is an atom then 0 otherwise 1 ∈ ℤ
⊢ a = nullvar() ∈ varname()
BY
{ (RepUR ``nullvar`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  varname()
2.  vs  :  varname()  List
3.  \mneg{}(vs  =  [])
4.  a  \mmember{}  Base
5.  t  :  Atom
6.  if  a  is  an  atom  then  a  otherwise  fst(a)  =  t
7.  i  :  \mBbbZ{}
8.  v1  :  \{b:varname()|  var-num(t;b)  =  i\} 
9.  (v1  \mmember{}  vs)
10.  var-num(t;v1)  =  i
11.  (\mforall{}y\mmember{}vs.var-num(t;y)  \mleq{}  i)
12.  <t,  i>  =  nullvar()
13.  \mneg{}i  <  0
14.  if  <t,  i>  is  an  atom  then  0  otherwise  1  =  if  nullvar()  is  an  atom  then  0  otherwise  1
\mvdash{}  a  =  nullvar()


By

---

Latex:
(RepUR  ``nullvar``  -1  THEN  Auto)

---

Home Index