---

Step * 1 of Lemma ap2-tuple_wf


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

---

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


By

---

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

---

Home Index