---

Step * 1 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. if i <z 0 then a else <t, i> fi  = nullvar() ∈ varname()
⊢ a = nullvar() ∈ varname()
BY
{ (SplitOnHypITE -1  THEN Auto) }

1
.....falsecase..... 
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
⊢ a = nullvar() ∈ varname()

---

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.  if  i  <z  0  then  a  else  <t,  i>  fi    =  nullvar()
\mvdash{}  a  =  nullvar()


By

---

Latex:
(SplitOnHypITE  -1    THEN  Auto)

---

Home Index