Step * 1 1 1 of Lemma fresh-cname_wf


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

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


Latex:


Latex:

1.  I  :  Cname  List
2.  [1  /  I]  \mmember{}  \{1...\}  List
3.  i  :  \mBbbZ{}
4.  v1  :  \{x:\{1...\}|  x  =  i\} 
5.  list-max(x.x;[1  /  I])  =  <i,  v1>
6.  (v1  \mmember{}  [1  /  I])
7.  v1  =  i
8.  (\mforall{}y\mmember{}[1  /  I].y  \mleq{}  i)
\mvdash{}  i  +  1  \mmember{}  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 


By


Latex:
(DSetVars  THEN  MemTypeCD  THEN  Auto)




Home Index