---

Step * 1 1 of Lemma ap-tuple_wf

.....falsecase..... 
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 : u1 ⟶ u × tuple-type(map(λp.((fst(p)) ⟶ (snd(p)));zip(v1;v)))
14. t : u1 × tuple-type(v1)
15. ¬(map(λp.((fst(p)) ⟶ (snd(p)));zip(v1;v)) = [] ∈ (𝕌{[1 | i 0]} List))
16. ¬(v1 = [] ∈ (Type List))
⊢ <(fst(f)) (fst(t)), ap-tuple(n - 1;snd(f);snd(t))> ∈ u × tuple-type(v)
BY
{ (DVar `f' THEN DVar `t' THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  n  :  \mBbbZ{}
2.  n  \mneq{}  1
3.  n  \mneq{}  0
4.  0  <  n
5.  \mforall{}A,B:Type  List.
          ((||A||  =  (n  -  1))
          {}\mRightarrow{}  (||B||  =  (n  -  1))
          {}\mRightarrow{}  (\mforall{}f:tuple-type(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(A;B))).  \mforall{}t:tuple-type(A).
                      (ap-tuple(n  -  1;f;t)  \mmember{}  tuple-type(B))))
6.  u1  :  Type
7.  v1  :  Type  List
8.  u  :  Type
9.  v  :  Type  List
10.  \mneg{}(v  =  [])
11.  (||v1||  +  1)  =  n
12.  (||v||  +  1)  =  n
13.  f  :  u1  {}\mrightarrow{}  u  \mtimes{}  tuple-type(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(v1;v)))
14.  t  :  u1  \mtimes{}  tuple-type(v1)
15.  \mneg{}(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(v1;v))  =  [])
16.  \mneg{}(v1  =  [])
\mvdash{}  <(fst(f))  (fst(t)),  ap-tuple(n  -  1;snd(f);snd(t))>  \mmember{}  u  \mtimes{}  tuple-type(v)


By

---

Latex:
(DVar  `f'  THEN  DVar  `t'  THEN  All  Reduce  THEN  Auto)

---

Home Index