Step * of Lemma pairwise-mapl

[T,T':Type].
  ∀L:T List. ∀f:{x:T| (x ∈ L)}  ⟶ T'.
    ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ L)  (y ∈ L)  P[f x;f y]))  (∀x,y∈mapl(f;L).  P[x;y]))
BY
TACTIC:(InductionOnList
          THEN Auto
          THEN Unfold `mapl` 0
          THEN Reduce 0
          THEN Try (Fold `mapl` 0)
          THEN Try ((RWO "pairwise-nil" THEN Auto))
          THEN Try ((RWO "pairwise-cons" THENA Auto))
          THEN AssertBY f ∈ {x:T| (x ∈ v)}  ⟶ T'
              Auto⋅
          THEN Auto) }

1
1. [T] Type
2. [T'] Type
3. T@i
4. List@i
5. ∀f:{x:T| (x ∈ v)}  ⟶ T'
     ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ v)  (y ∈ v)  P[f x;f y]))  (∀x,y∈mapl(f;v).  P[x;y]))
6. {x:T| (x ∈ [u v])}  ⟶ T'@i
7. [P] T' ⟶ T' ⟶ ℙ'
8. ∀x,y:T.  ((x ∈ [u v])  (y ∈ [u v])  P[f x;f y])
9. f ∈ {x:T| (x ∈ v)}  ⟶ T'
10. (∀x,y∈mapl(f;v).  P[x;y])
⊢ (∀y∈mapl(f;v).P[f u;y])


Latex:


Latex:
\mforall{}[T,T':Type].
    \mforall{}L:T  List.  \mforall{}f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  T'.
        \mforall{}[P:T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}']
            ((\mforall{}x,y:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  P[f  x;f  y]))  {}\mRightarrow{}  (\mforall{}x,y\mmember{}mapl(f;L).    P[x;y]))


By


Latex:
TACTIC:(InductionOnList
                THEN  Auto
                THEN  Unfold  `mapl`  0
                THEN  Reduce  0
                THEN  Try  (Fold  `mapl`  0)
                THEN  Try  ((RWO  "pairwise-nil"  0  THEN  Auto))
                THEN  Try  ((RWO  "pairwise-cons"  0  THENA  Auto))
                THEN  AssertBY  f  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
                        Auto\mcdot{}
                THEN  Auto)




Home Index