Step
*
1
1
1
of Lemma
maybe_new_var-is-null
.....fun wf..... 
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. Z : varname()
⊢ if Z is an atom then 0 otherwise 1 = if Z is an atom then 0 otherwise 1 ∈ ℤ
BY
{ RepeatFor 2 (((D -1 THEN Reduce 0) THEN Auto)) }
Latex:
Latex:
.....fun  wf..... 
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.  Z  :  varname()
\mvdash{}  if  Z  is  an  atom  then  0  otherwise  1  =  if  Z  is  an  atom  then  0  otherwise  1
By
Latex:
RepeatFor  2  (((D  -1  THEN  Reduce  0)  THEN  Auto))
Home
Index