---

Step * of Lemma ap2-tuple_wf

∀[n:ℕ]. ∀[A,B:Type List].
  ∀[C:Type]. ∀[x:C]. ∀[f:tuple-type(map(λp.(C ⟶ (fst(p)) ⟶ (snd(p)));zip(A;B)))]. ∀[t:tuple-type(A)].
    (ap2-tuple(n;f;x;t) ∈ tuple-type(B)) 
  supposing (||A|| = n ∈ ℤ) ∧ (||B|| = n ∈ ℤ)
BY
{ (Auto
   THEN RepeatFor 8 (MoveToConcl (-1))
   THEN NatInd (-1)
   THEN Auto
   THEN (DVar `B' THEN Auto')
   THEN (DVar `A' THEN Auto')
   THEN RecUnfold `ap2-tuple` 0
   THEN All Reduce
   THEN Auto
   THEN AutoSplit
   THEN Try (((DVar `v' THEN All Reduce THEN Auto') 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) ∈ ℤ)
     ⇒ (∀C:Type. ∀x:C. ∀f:tuple-type(map(λp.(C ⟶ (fst(p)) ⟶ (snd(p)));zip(A;B))). ∀t:tuple-type(A).
           (ap2-tuple(n - 1;f;x;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. C : Type
14. x : C
15. f : if null(map(λp.(C ⟶ (fst(p)) ⟶ (snd(p)));zip(v1;v)))
then C ⟶ u1 ⟶ u
else C ⟶ u1 ⟶ u × tuple-type(map(λp.(C ⟶ (fst(p)) ⟶ (snd(p)));zip(v1;v)))
fi 
16. t : if null(v1) then u1 else u1 × tuple-type(v1) fi 
⊢ <(fst(f)) x (fst(t)), ap2-tuple(n - 1;snd(f);x;snd(t))> ∈ u × tuple-type(v)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  8  (MoveToConcl  (-1))
  THEN  NatInd  (-1)
  THEN  Auto
  THEN  (DVar  `B'  THEN  Auto')
  THEN  (DVar  `A'  THEN  Auto')
  THEN  RecUnfold  `ap2-tuple`  0
  THEN  All  Reduce
  THEN  Auto
  THEN  AutoSplit
  THEN  Try  (((DVar  `v'  THEN  All  Reduce  THEN  Auto')
                        THEN  DVar  `v1'
                        THEN  All  Reduce
                        THEN  Complete  (Auto'))))

---

Home Index