---

Step * 1 of Lemma ap-tuple_wf


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)
BY
{ RepeatFor 2 (((SplitOnHypITE -2  THENA Auto)
                THEN Try (((DVar `v' THEN All Reduce) THEN DVar `v1' THEN All Reduce THEN Complete (Auto')))
                )) }

1
.....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)

---

Latex:

---

Latex:

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  :  if  null(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(v1;v)))
then  u1  {}\mrightarrow{}  u
else  u1  {}\mrightarrow{}  u  \mtimes{}  tuple-type(map(\mlambda{}p.((fst(p))  {}\mrightarrow{}  (snd(p)));zip(v1;v)))
fi 
14.  t  :  if  null(v1)  then  u1  else  u1  \mtimes{}  tuple-type(v1)  fi 
\mvdash{}  <(fst(f))  (fst(t)),  ap-tuple(n  -  1;snd(f);snd(t))>  \mmember{}  u  \mtimes{}  tuple-type(v)


By

---

Latex:
RepeatFor  2  (((SplitOnHypITE  -2    THENA  Auto)
                            THEN  Try  (((DVar  `v'  THEN  All  Reduce)
                                                  THEN  DVar  `v1'
                                                  THEN  All  Reduce
                                                  THEN  Complete  (Auto')))
                            ))

---

Home Index