---

Step * 1 2 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 ≠ 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]]))
BY
{ ((InstHyp [⌜x2⌝;⌜n - 1⌝] (-6)⋅ THENA Auto)
   THEN GenConclAtAddr [2;1]
   THEN D -2
   THEN RecUnfold `nth_tl` 0⋅
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto) }

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
10. n ≠ 0
11. split-tuple(x2;n - 1) ∈ tuple-type(firstn(n - 1;[u1 / v])) × tuple-type(nth_tl(n - 1;[u1 / v]))
12. v2 : tuple-type(firstn(n - 1;[u1 / v]))
13. v3 : tuple-type(nth_tl(n - 1;[u1 / v]))
14. split-tuple(x2;n - 1) = <v2, v3> ∈ (tuple-type(firstn(n - 1;[u1 / v])) × tuple-type(nth_tl(n - 1;[u1 / v])))
⊢ <x1, v2> ∈ tuple-type(firstn(n;[u; [u1 / v]]))

---

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{}  1
9.  n  \mneq{}  0
\mvdash{}  let  a,b  =  split-tuple(x2;n  -  1) 
    in  <<x1,  a>,  b>  \mmember{}  tuple-type(firstn(n;[u;  [u1  /  v]]))  \mtimes{}  tuple-type(nth\_tl(n;[u;  [u1  /  v]]))


By

---

Latex:
((InstHyp  [\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  GenConclAtAddr  [2;1]
  THEN  D  -2
  THEN  RecUnfold  `nth\_tl`  0\mcdot{}
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto)

---

Home Index