---

Step * of Lemma map-tuple_wf

∀[n:ℕ]. ∀[A,B:Type List].
  ∀[f:⋂i:ℕn. (A[i] ⟶ B[i])]. ∀[t:tuple-type(A)].  (map-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 `map-tuple` 0
   THEN All Reduce
   THEN Try (Trivial)
   THEN ((BoolCase ⌜null(v)⌝⋅ THENA Auto)
         THENL [((Subst' n ~ 1 0 THENA (DVar `v' THEN All Reduce THEN Auto'))
                 THEN Reduce 0
                 THEN (Subst' null(v1) ~ tt -2 THENA (DVar `v' THEN DVar `v1' THEN All Reduce THEN Auto'))
                 THEN Reduce -2)
               ; ((Assert 2 ≤ n BY
                         (DVar `v' THEN All Reduce THEN Auto'))
                  THEN (Subst' null(v1) ~ ff -2 THENA (DVar `v' THEN DVar `v1' THEN All Reduce THEN Auto'))
                  THEN Reduce -2
                  THEN D -2
                  THEN Reduce 0)]
   )
   THEN Try ((InstHyp [⌜v1⌝;⌜v⌝;⌜f⌝;⌜t2⌝] 3⋅ THENA Auto))
   THEN Try (((Assert f ∈ [u1 / v1][0] ⟶ [u / v][0] BY
                     Auto)
              THEN Reduce (-1)
              THEN (DVar `v1' THEN DVar `v')
              THEN All Reduce
              THEN Auto'))
   THEN With ⌜i + 1⌝ ( D(-6))⋅
   THEN Try (RWO "select_cons_tl" (-1))
   THEN Auto
   THEN Subst' (i + 1) - 1 ~ i -1
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[A,B:Type  List].
    \mforall{}[f:\mcap{}i:\mBbbN{}n.  (A[i]  {}\mrightarrow{}  B[i])].  \mforall{}[t:tuple-type(A)].    (map-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  `map-tuple`  0
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  ((BoolCase  \mkleeneopen{}null(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((Subst'  n  \msim{}  1  0  THENA  (DVar  `v'  THEN  All  Reduce  THEN  Auto'))
                              THEN  Reduce  0
                              THEN  (Subst'  null(v1)  \msim{}  tt  -2
                                          THENA  (DVar  `v'  THEN  DVar  `v1'  THEN  All  Reduce  THEN  Auto')
                                          )
                              THEN  Reduce  -2)
                          ;  ((Assert  2  \mleq{}  n  BY
                                              (DVar  `v'  THEN  All  Reduce  THEN  Auto'))
                                THEN  (Subst'  null(v1)  \msim{}  ff  -2
                                            THENA  (DVar  `v'  THEN  DVar  `v1'  THEN  All  Reduce  THEN  Auto')
                                            )
                                THEN  Reduce  -2
                                THEN  D  -2
                                THEN  Reduce  0)]
  )
  THEN  Try  ((InstHyp  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}t2\mkleeneclose{}]  3\mcdot{}  THENA  Auto))
  THEN  Try  (((Assert  f  \mmember{}  [u1  /  v1][0]  {}\mrightarrow{}  [u  /  v][0]  BY
                                      Auto)
                        THEN  Reduce  (-1)
                        THEN  (DVar  `v1'  THEN  DVar  `v')
                        THEN  All  Reduce
                        THEN  Auto'))
  THEN  With  \mkleeneopen{}i  +  1\mkleeneclose{}  (  D(-6))\mcdot{}
  THEN  Try  (RWO  "select\_cons\_tl"  (-1))
  THEN  Auto
  THEN  Subst'  (i  +  1)  -  1  \msim{}  i  -1
  THEN  Auto')

---

Home Index