---

Step * 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∈vs.var-num(t;y) ≤ i)
⊢ ¬(if i <z 0 then a else <t, i> fi  = v ∈ varname())
BY
{ ((RWO "l_all_iff" (-1) THENA Auto) THEN (InstHyp [⌜v⌝] (-1)⋅ 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;v) ≤ i
⊢ ¬(if i <z 0 then a else <t, i> fi  = v ∈ varname())

---

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\mmember{}vs.var-num(t;y)  \mleq{}  i)
\mvdash{}  \mneg{}(if  i  <z  0  then  a  else  <t,  i>  fi    =  v)


By

---

Latex:
((RWO  "l\_all\_iff"  (-1)  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index