---

Step * 1 1 of Lemma split-tuple_wf


1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[x:if null(v) then u1 else u1 × tuple-type(v) fi ]. ∀[n:ℕ||v|| + 1].
     (split-tuple(x;n) ∈ tuple-type(firstn(n;[u1 / v])) × tuple-type(nth_tl(n;[u1 / v])))
5. x1 : u
6. x2 : if null(v) then u1 else u1 × tuple-type(v) fi 
7. n : ℕ(||v|| + 1) + 1
8. n ≠ 0
9. n = 1 ∈ ℤ
⊢ <x1, x2> ∈ tuple-type(firstn(n;[u; [u1 / v]])) × tuple-type(nth_tl(n;[u; [u1 / v]]))
BY
{ TACTIC:(HypSubst' (-1) 0
          THEN Reduce 0
          THEN Auto
          THEN RecUnfold `firstn` 0
          THEN Reduce 0
          THEN RWO "first0" 0
          THEN Reduce 0
          THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  u  :  Type
2.  u1  :  Type
3.  v  :  Type  List
4.  \mforall{}[x:if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi  ].  \mforall{}[n:\mBbbN{}||v||  +  1].
          (split-tuple(x;n)  \mmember{}  tuple-type(firstn(n;[u1  /  v]))  \mtimes{}  tuple-type(nth\_tl(n;[u1  /  v])))
5.  x1  :  u
6.  x2  :  if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi 
7.  n  :  \mBbbN{}(||v||  +  1)  +  1
8.  n  \mneq{}  0
9.  n  =  1
\mvdash{}  <x1,  x2>  \mmember{}  tuple-type(firstn(n;[u;  [u1  /  v]]))  \mtimes{}  tuple-type(nth\_tl(n;[u;  [u1  /  v]]))


By

---

Latex:
TACTIC:(HypSubst'  (-1)  0
                THEN  Reduce  0
                THEN  Auto
                THEN  RecUnfold  `firstn`  0
                THEN  Reduce  0
                THEN  RWO  "first0"  0
                THEN  Reduce  0
                THEN  Auto)\mcdot{}

---

Home Index