---

Step * 1 1 of Lemma maybe_new_var-is-null

.....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()
BY
{ ApFunToHypEquands `Z' ⌜if Z is an atom then 0 otherwise 1⌝ ⌜ℤ⌝ (-2)⋅ }

1
.....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 ∈ ℤ

2
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()

---

Latex:

---

Latex:
.....falsecase..... 
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
\mvdash{}  a  =  nullvar()


By

---

Latex:
ApFunToHypEquands  `Z'  \mkleeneopen{}if  Z  is  an  atom  then  0  otherwise  1\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-2)\mcdot{}

---

Home Index