---

Step * 1 2 1 2 2 1 of Lemma split-tuple-append-tuple


1. u : Type
2. v : Type List
3. ¬((||v|| + 1) ≤ 0)
4. ||v|| + 1 ≠ 1
5. ||v|| + 1 ≠ 0
6. ∀[L2:Type List]
     ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||v||;||L2||;x;y);||v||) ~ <x, y>) supposing 0 \000C< ||L2||
7. L2 : Type List
8. 0 < ||L2||
9. x1 : u
10. x2 : tuple-type(v)
11. y : tuple-type(L2)
12. ¬(v = [] ∈ (Type List))
⊢ let a,b = split-tuple(append-tuple((||v|| + 1) - 1;||L2||;x2;y);(||v|| + 1) - 1) 
  in <<x1, a>, b> ~ <<x1, x2>, y>
BY
{ (Subst' (||v|| + 1) - 1 ~ ||v|| 0 THEN Auto) }

1
1. u : Type
2. v : Type List
3. ¬((||v|| + 1) ≤ 0)
4. ||v|| + 1 ≠ 1
5. ||v|| + 1 ≠ 0
6. ∀[L2:Type List]
     ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||v||;||L2||;x;y);||v||) ~ <x, y>) supposing 0 \000C< ||L2||
7. L2 : Type List
8. 0 < ||L2||
9. x1 : u
10. x2 : tuple-type(v)
11. y : tuple-type(L2)
12. ¬(v = [] ∈ (Type List))
⊢ let a,b = split-tuple(append-tuple(||v||;||L2||;x2;y);||v||) 
  in <<x1, a>, b> ~ <<x1, x2>, y>

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mneg{}((||v||  +  1)  \mleq{}  0)
4.  ||v||  +  1  \mneq{}  1
5.  ||v||  +  1  \mneq{}  0
6.  \mforall{}[L2:Type  List]
          \mforall{}[x:tuple-type(v)].  \mforall{}[y:tuple-type(L2)].
              (split-tuple(append-tuple(||v||;||L2||;x;y);||v||)  \msim{}  <x,  y>) 
          supposing  0  <  ||L2||
7.  L2  :  Type  List
8.  0  <  ||L2||
9.  x1  :  u
10.  x2  :  tuple-type(v)
11.  y  :  tuple-type(L2)
12.  \mneg{}(v  =  [])
\mvdash{}  let  a,b  =  split-tuple(append-tuple((||v||  +  1)  -  1;||L2||;x2;y);(||v||  +  1)  -  1) 
    in  <<x1,  a>,  b>  \msim{}  <<x1,  x2>,  y>


By

---

Latex:
(Subst'  (||v||  +  1)  -  1  \msim{}  ||v||  0  THEN  Auto)

---

Home Index