---

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


1. u : Type
2. v : Type List
3. ||v|| + 1 ≠ 1
4. ||v|| + 1 ≠ 0
5. ∀[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||
6. L2 : Type List
7. 0 < ||L2||
8. x : if null(v) then u else u × tuple-type(v) fi 
9. y : tuple-type(L2)
⊢ let a,b = split-tuple(snd(if ||v|| + 1 ≤z 0
  then y
  else let a,b = x 
       in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
  fi );(||v|| + 1) - 1) 
  in <<fst(if ||v|| + 1 ≤z 0 then y else let a,b = x in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)> fi ), a>, b> ~ <x
                                                                                                                     , y
                                                                                                                     >
BY
{ (At ⌜𝕌'⌝ (SplitOnHypITE -2 )⋅ THENA Auto) }

1
.....truecase..... 
1. u : Type
2. v : Type List
3. ||v|| + 1 ≠ 1
4. ||v|| + 1 ≠ 0
5. ∀[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||
6. L2 : Type List
7. 0 < ||L2||
8. x : u
9. y : tuple-type(L2)
10. v = [] ∈ (Type List)
⊢ let a,b = split-tuple(snd(if ||v|| + 1 ≤z 0
  then y
  else let a,b = x 
       in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
  fi );(||v|| + 1) - 1) 
  in <<fst(if ||v|| + 1 ≤z 0 then y else let a,b = x in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)> fi ), a>, b> ~ <x
                                                                                                                     , y
                                                                                                                     >

2
.....falsecase..... 
1. u : Type
2. v : Type List
3. ||v|| + 1 ≠ 1
4. ||v|| + 1 ≠ 0
5. ∀[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||
6. L2 : Type List
7. 0 < ||L2||
8. x : u × tuple-type(v)
9. y : tuple-type(L2)
10. ¬(v = [] ∈ (Type List))
⊢ let a,b = split-tuple(snd(if ||v|| + 1 ≤z 0
  then y
  else let a,b = x 
       in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
  fi );(||v|| + 1) - 1) 
  in <<fst(if ||v|| + 1 ≤z 0 then y else let a,b = x in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)> fi ), a>, b> ~ <x
                                                                                                                     , y
                                                                                                                     >

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  ||v||  +  1  \mneq{}  1
4.  ||v||  +  1  \mneq{}  0
5.  \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||
6.  L2  :  Type  List
7.  0  <  ||L2||
8.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
9.  y  :  tuple-type(L2)
\mvdash{}  let  a,b  =  split-tuple(snd(if  ||v||  +  1  \mleq{}z  0
    then  y
    else  let  a,b  =  x 
              in  <a,  append-tuple((||v||  +  1)  -  1;||L2||;b;y)>
    fi  );(||v||  +  1)  -  1) 
    in  <<fst(if  ||v||  +  1  \mleq{}z  0
              then  y
              else  let  a,b  =  x 
                        in  <a,  append-tuple((||v||  +  1)  -  1;||L2||;b;y)>
              fi  )
            ,  a
            >
          ,  b
          >  \msim{}  <x,  y>


By

---

Latex:
(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (SplitOnHypITE  -2  )\mcdot{}  THENA  Auto)

---

Home Index