---

Step * of Lemma ap-tuple_wf

∀[n:ℕ]. ∀[A,B:Type List].
  ∀[f:tuple-type(map(λp.((fst(p)) ⟶ (snd(p)));zip(A;B)))]. ∀[t:tuple-type(A)].  (ap-tuple(n;f;t) ∈ tuple-type(B)) 
  supposing (||A|| = n ∈ ℤ) ∧ (||B|| = n ∈ ℤ)
BY
{ (Auto
   THEN RepeatFor 6 (MoveToConcl (-1))
   THEN NatInd (-1)
   THEN Auto
   THEN (DVar `B' THEN Auto')
   THEN (DVar `A' THEN Auto')
   THEN RecUnfold `ap-tuple` 0
   THEN All Reduce
   THEN Try (Trivial)
   THEN Auto
   THEN AutoSplit
   THEN Try (((DVar `v' THEN All Reduce) THEN Complete (Auto')))
   THEN Try (((DVar `v' THEN All Reduce) THEN DVar `v1' THEN All Reduce THEN Complete (Auto'))))⋅ }

1
1. n : ℤ
2. n ≠ 1
3. n ≠ 0
4. 0 < n
5. ∀A,B:Type List.
     ((||A|| = (n - 1) ∈ ℤ)
     ⇒ (||B|| = (n - 1) ∈ ℤ)
     ⇒ (∀f:tuple-type(map(λp.((fst(p)) ⟶ (snd(p)));zip(A;B))). ∀t:tuple-type(A).
           (ap-tuple(n - 1;f;t) ∈ tuple-type(B))))
6. u1 : Type
7. v1 : Type List
8. u : Type
9. v : Type List
10. ¬(v = [] ∈ (Type List))
11. (||v1|| + 1) = n ∈ ℤ
12. (||v|| + 1) = n ∈ ℤ
13. f : if null(map(λp.((fst(p)) ⟶ (snd(p)));zip(v1;v)))
then u1 ⟶ u
else u1 ⟶ u × tuple-type(map(λp.((fst(p)) ⟶ (snd(p)));zip(v1;v)))
fi 
14. t : if null(v1) then u1 else u1 × tuple-type(v1) fi 
⊢ <(fst(f)) (fst(t)), ap-tuple(n - 1;snd(f);snd(t))> ∈ u × tuple-type(v)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[A,B:Type  List].
    \mforall{}[f:tuple-type(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(A;B)))].  \mforall{}[t:tuple-type(A)].
        (ap-tuple(n;f;t)  \mmember{}  tuple-type(B)) 
    supposing  (||A||  =  n)  \mwedge{}  (||B||  =  n)


By

---

Latex:
(Auto
  THEN  RepeatFor  6  (MoveToConcl  (-1))
  THEN  NatInd  (-1)
  THEN  Auto
  THEN  (DVar  `B'  THEN  Auto')
  THEN  (DVar  `A'  THEN  Auto')
  THEN  RecUnfold  `ap-tuple`  0
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  Auto
  THEN  AutoSplit
  THEN  Try  (((DVar  `v'  THEN  All  Reduce)  THEN  Complete  (Auto')))
  THEN  Try  (((DVar  `v'  THEN  All  Reduce)  THEN  DVar  `v1'  THEN  All  Reduce  THEN  Complete  (Auto'))))\mcdot{}

---

Home Index