---

Step * 1 1 of Lemma fresh-cname_wf


1. I : Cname List
2. [1 / I] ∈ {1...} List
3. v : i:ℤ × {x:{1...}| x = i ∈ ℤ} 
4. list-max(x.x;[1 / I]) = v ∈ (i:ℤ × {x:{1...}| x = i ∈ ℤ} )
⊢ let n,x = v in (x ∈ [1 / I]) ∧ (x = n ∈ ℤ) ∧ (∀y∈[1 / I].y ≤ n) ⇒ ((fst(v)) + 1 ∈ {x:Cname| ¬(x ∈ I)} )
BY
{ ((D -2 THEN Reduce 0) THEN Auto) }

1
1. I : Cname List
2. [1 / I] ∈ {1...} List
3. i : ℤ
4. v1 : {x:{1...}| x = i ∈ ℤ} 
5. list-max(x.x;[1 / I]) = <i, v1> ∈ (i:ℤ × {x:{1...}| x = i ∈ ℤ} )
6. (v1 ∈ [1 / I])
7. v1 = i ∈ ℤ
8. (∀y∈[1 / I].y ≤ i)
⊢ i + 1 ∈ {x:Cname| ¬(x ∈ I)} 

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  [1  /  I]  \mmember{}  \{1...\}  List
3.  v  :  i:\mBbbZ{}  \mtimes{}  \{x:\{1...\}|  x  =  i\} 
4.  list-max(x.x;[1  /  I])  =  v
\mvdash{}  let  n,x  =  v 
    in  (x  \mmember{}  [1  /  I])  \mwedge{}  (x  =  n)  \mwedge{}  (\mforall{}y\mmember{}[1  /  I].y  \mleq{}  n)
{}\mRightarrow{}  ((fst(v))  +  1  \mmember{}  \{x:Cname|  \mneg{}(x  \mmember{}  I)\}  )


By

---

Latex:
((D  -2  THEN  Reduce  0)  THEN  Auto)

---

Home Index