---

Step * 1 of Lemma split-tuple_wf


1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[x:tuple-type([u1 / v])]. ∀[n:ℕ||[u1 / v]||].
     (split-tuple(x;n) ∈ tuple-type(firstn(n;[u1 / v])) × tuple-type(nth_tl(n;[u1 / v])))
5. x : if null([u1 / v]) then u else u × tuple-type([u1 / v]) fi 
6. n : ℕ||[u1 / v]|| + 1
7. n ≠ 0
⊢ if (n =z 1) then <fst(x), snd(x)> else let a,b = split-tuple(snd(x);n - 1) in <<fst(x), a>, b> fi 
  ∈ tuple-type(firstn(n;[u; [u1 / v]])) × tuple-type(nth_tl(n;[u; [u1 / v]]))
BY
{ (All Reduce THEN DVar `x' THEN Reduce 0 THEN AutoSplit) }

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

2
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 ≠ 1
9. n ≠ 0
⊢ let a,b = split-tuple(x2;n - 1) 
  in <<x1, a>, b> ∈ tuple-type(firstn(n;[u; [u1 / v]])) × tuple-type(nth_tl(n;[u; [u1 / v]]))

---

Latex:

---

Latex:

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


By

---

Latex:
(All  Reduce  THEN  DVar  `x'  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index