---

Step * 1 of Lemma select-tuple_wf


1. v : Type List
2. u : Type
3. ∀[n:ℕ]. ∀[k:ℤ].  ∀[x:tuple-type(v)]. (x.n ∈ v[n]) supposing n < ||v|| ∧ (k = ||v|| ∈ ℤ)
4. n : ℕ
5. n < ||v|| + 1
6. x : if null(v) then u else u × tuple-type(v) fi 
⊢ x.n ∈ [u / v][n]
BY
{ (RecUnfold `select-tuple` 0⋅
   THEN AutoSplit
   THEN ((RWO "select-cons-tl" 0 THEN Auto' THEN BHyp 3  THEN Auto') ORELSE (HypSubst' (-1) 0⋅ THEN Reduce 0))
   THEN (DVar `v' THEN All Reduce THEN Try ((DVar `x' THEN Reduce 0)) THEN Auto')⋅) }

---

Latex:

---

Latex:

1.  v  :  Type  List
2.  u  :  Type
3.  \mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbZ{}].    \mforall{}[x:tuple-type(v)].  (x.n  \mmember{}  v[n])  supposing  n  <  ||v||  \mwedge{}  (k  =  ||v||)
4.  n  :  \mBbbN{}
5.  n  <  ||v||  +  1
6.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
\mvdash{}  x.n  \mmember{}  [u  /  v][n]


By

---

Latex:
(RecUnfold  `select-tuple`  0\mcdot{}
  THEN  AutoSplit
  THEN  ((RWO  "select-cons-tl"  0  THEN  Auto'  THEN  BHyp  3    THEN  Auto')
  ORELSE  (HypSubst'  (-1)  0\mcdot{}  THEN  Reduce  0)
  )
  THEN  (DVar  `v'  THEN  All  Reduce  THEN  Try  ((DVar  `x'  THEN  Reduce  0))  THEN  Auto')\mcdot{})

---

Home Index