---

Step * 1 1 1 of Lemma maybe_new_var-distinct


1. a : varname()
2. vs : varname() List
3. ¬(vs = [] ∈ (varname() List))
4. a ∈ Base
5. v : varname()
6. (v ∈ vs)
7. t : Atom
8. if a is an atom then a otherwise fst(a) = t ∈ Atom
9. i : ℤ
10. v2 : {b:varname()| var-num(t;b) = i ∈ ℤ} 
11. (v2 ∈ vs)
12. var-num(t;v2) = i ∈ ℤ
13. ∀y:varname(). ((y ∈ vs) ⇒ (var-num(t;y) ≤ i))
14. var-num(t;if i <z 0 then a else <t, i> fi ) ≤ i
15. if i <z 0 then a else <t, i> fi  = v ∈ varname()
⊢ False
BY
{ (D 1
   THEN Try (D 1)
   THEN (All Reduce THENA Auto)
   THEN (HypSubst' 9 (-2) ORELSE HypSubst' 8 (-2))
   THEN MoveToConcl (-2)
   THEN AutoSplit
   THEN RepUR ``var-num`` 0
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  1
  THEN  Try  (D  1)
  THEN  (All  Reduce  THENA  Auto)
  THEN  (HypSubst'  9  (-2)  ORELSE  HypSubst'  8  (-2))
  THEN  MoveToConcl  (-2)
  THEN  AutoSplit
  THEN  RepUR  ``var-num``  0
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index