---

Step * 1 1 1 1 1 2 of Lemma fresh-cname_wf


1. I : Cname List
2. [1 / I] ∈ {1...} List
3. i : ℤ
4. v1 : {1...}
5. v1 = i ∈ ℤ
6. list-max(x.x;[1 / I]) = <i, v1> ∈ (i:ℤ × {x:{1...}| x = i ∈ ℤ} )
7. (v1 ∈ [1 / I])
8. v1 = i ∈ ℤ
9. j : ℕ
10. j < ||I|| c∧ ((i + 1) = I[j] ∈ Cname)
11. [1 / I][j + 1] ≤ i
⊢ False
BY
{ (RWO "select_cons_tl" (-1) THENA Auto) }

1
.....rewrite subgoal..... 
1. I : Cname List
2. [1 / I] ∈ {1...} List
3. i : ℤ
4. v1 : {1...}
5. v1 = i ∈ ℤ
6. list-max(x.x;[1 / I]) = <i, v1> ∈ (i:ℤ × {x:{1...}| x = i ∈ ℤ} )
7. (v1 ∈ [1 / I])
8. v1 = i ∈ ℤ
9. j : ℕ
10. j < ||I|| c∧ ((i + 1) = I[j] ∈ Cname)
11. [1 / I][j + 1] ≤ i
⊢ (j + 1) ≤ ||I||

2
1. I : Cname List
2. [1 / I] ∈ {1...} List
3. i : ℤ
4. v1 : {1...}
5. v1 = i ∈ ℤ
6. list-max(x.x;[1 / I]) = <i, v1> ∈ (i:ℤ × {x:{1...}| x = i ∈ ℤ} )
7. (v1 ∈ [1 / I])
8. v1 = i ∈ ℤ
9. j : ℕ
10. j < ||I|| c∧ ((i + 1) = I[j] ∈ Cname)
11. I[(j + 1) - 1] ≤ i
⊢ False

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  [1  /  I]  \mmember{}  \{1...\}  List
3.  i  :  \mBbbZ{}
4.  v1  :  \{1...\}
5.  v1  =  i
6.  list-max(x.x;[1  /  I])  =  <i,  v1>
7.  (v1  \mmember{}  [1  /  I])
8.  v1  =  i
9.  j  :  \mBbbN{}
10.  j  <  ||I||  c\mwedge{}  ((i  +  1)  =  I[j])
11.  [1  /  I][j  +  1]  \mleq{}  i
\mvdash{}  False


By

---

Latex:
(RWO  "select\_cons\_tl"  (-1)  THENA  Auto)

---

Home Index