---

Step * 1 of Lemma fresh-cname_wf


1. I : Cname List
2. [1 / I] ∈ {1...} List
⊢ fresh-cname(I) ∈ {x:Cname| ¬(x ∈ I)} 
BY
{ (Unfold `fresh-cname` 0
   THEN (InstLemma `list-max-property` [⌜{1...}⌝;⌜λ2x.x⌝;⌜[1 / I]⌝]⋅ THENA (Reduce 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜list-max(x.x;[1 / I])⌝⋅ THENA Auto)) }

1
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)} )

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  [1  /  I]  \mmember{}  \{1...\}  List
\mvdash{}  fresh-cname(I)  \mmember{}  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 


By

---

Latex:
(Unfold  `fresh-cname`  0
  THEN  (InstLemma  `list-max-property`  [\mkleeneopen{}\{1...\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}[1  /  I]\mkleeneclose{}]\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}list-max(x.x;[1  /  I])\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index