Step * 1 of Lemma split-tuple_wf


1. Type
2. u1 Type
3. 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. if null([u1 v]) then else u × tuple-type([u1 v]) fi 
6. : ℕ||[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 THEN AutoSplit) }

1
1. Type
2. u1 Type
3. 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. : ℕ(||v|| 1) 1
8. n ≠ 0
9. 1 ∈ ℤ
⊢ <x1, x2> ∈ tuple-type(firstn(n;[u; [u1 v]])) × tuple-type(nth_tl(n;[u; [u1 v]]))

2
1. Type
2. u1 Type
3. 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. : ℕ(||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