Step
*
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;v) ≤ i
⊢ ¬(if i <z 0 then a else <t, i> fi  = v ∈ varname())
BY
{ ((D 0 THENA Auto) THEN (RWO "-1<" (-2) THENA Auto)) }
1
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
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;v)  \mleq{}  i
\mvdash{}  \mneg{}(if  i  <z  0  then  a  else  <t,  i>  fi    =  v)
By
Latex:
((D  0  THENA  Auto)  THEN  (RWO  "-1<"  (-2)  THENA  Auto))
Home
Index