---

Step * of Lemma tuple_wf

∀[L:Type List]. ∀[F:i:ℕ||L|| ⟶ L[i]]. ∀[n:{n:ℤ| n = ||L|| ∈ ℤ} ].  (tuple(n;i.F[i]) ∈ tuple-type(L))
BY
{ (Auto
   THEN D -1
   THEN HypSubst' (-1) 0
   THEN ThinVar `n'
   THEN RepUR ``tuple`` 0
   THEN ListInd 1
   THEN Reduce 0
   THEN Auto
   THEN (RWO "upto_decomp2" 0 THENA Auto')
   THEN Reduce 0
   THEN ((RWO "map-map" 0 THENM RepUR ``compose`` 0) THENA Auto)
   THEN (RWW "null-map null-upto" 0 THENA Auto)
   THEN ((Decide ⌜↑null(v)⌝⋅ THENA Auto) THENL [(DVar `v' THEN All Reduce THEN Auto); RepeatFor 2 (AutoSplit)])) }

1
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
5. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
6. ¬False
7. ((||v|| + 1) - 1) = 0 ∈ ℤ
⊢ F[0] ∈ u × tuple-type(v)

2
1. u : Type
2. v : Type List
3. (||v|| + 1) - 1 ≠ 0
4. ¬(v = [] ∈ (Type List))
5. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
6. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
7. ¬False
⊢ <F[0], rec-case(map(λx.F[x + 1];upto((||v|| + 1) - 1))) of [] => ⋅ | h::t => r.if null(t) then h else <h, r> fi > ∈ u
  × tuple-type(v)

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[F:i:\mBbbN{}||L||  {}\mrightarrow{}  L[i]].  \mforall{}[n:\{n:\mBbbZ{}|  n  =  ||L||\}  ].    (tuple(n;i.F[i])  \mmember{}  tuple-type(L))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `n'
  THEN  RepUR  ``tuple``  0
  THEN  ListInd  1
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "upto\_decomp2"  0  THENA  Auto')
  THEN  Reduce  0
  THEN  ((RWO  "map-map"  0  THENM  RepUR  ``compose``  0)  THENA  Auto)
  THEN  (RWW  "null-map  null-upto"  0  THENA  Auto)
  THEN  ((Decide  \mkleeneopen{}\muparrow{}null(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(DVar  `v'  THEN  All  Reduce  THEN  Auto);  RepeatFor  2  (AutoSplit)]
  ))

---

Home Index