---

Step * 1 of Lemma l_before_map


1. [A] : Type
2. [B] : Type
3. l : A List@i
4. f : A ⟶ B@i
5. x : B@i
6. y : B@i
7. f@0 : ℕ2 ⟶ ℕ||map(f;l)||@i
8. increasing(f@0;2)
9. ∀j:ℕ2. ([x; y][j] = map(f;l)[f@0 j] ∈ B)
⊢ ∃u,v:A. ((x = (f u) ∈ B) ∧ (y = (f v) ∈ B) ∧ (∃f:ℕ2 ⟶ ℕ||l||. (increasing(f;2) ∧ (∀j:ℕ2. ([u; v][j] = l[f j] ∈ A)))))
BY
{ TACTIC:((InstHyp [⌜0⌝] (-1)⋅ THENA Auto)
          THEN (InstHyp [⌜1⌝] (-2)⋅ THENA Auto)
          THEN AllReduce
          THEN (RW ListC (-2) THENA Auto)
          THEN (RW ListC (-1) THENA Auto)
          THEN InstConcl [⌜l[f@0 0]⌝;⌜l[f@0 1]⌝]⋅
          THEN Auto
          THEN InstConcl [⌜f@0⌝]⋅
          THEN Auto
          THEN IntSegCases (-1)
          THEN Reduce 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  l  :  A  List@i
4.  f  :  A  {}\mrightarrow{}  B@i
5.  x  :  B@i
6.  y  :  B@i
7.  f@0  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||map(f;l)||@i
8.  increasing(f@0;2)
9.  \mforall{}j:\mBbbN{}2.  ([x;  y][j]  =  map(f;l)[f@0  j])
\mvdash{}  \mexists{}u,v:A
      ((x  =  (f  u))
      \mwedge{}  (y  =  (f  v))
      \mwedge{}  (\mexists{}f:\mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||l||.  (increasing(f;2)  \mwedge{}  (\mforall{}j:\mBbbN{}2.  ([u;  v][j]  =  l[f  j])))))


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                THEN  AllReduce
                THEN  (RW  ListC  (-2)  THENA  Auto)
                THEN  (RW  ListC  (-1)  THENA  Auto)
                THEN  InstConcl  [\mkleeneopen{}l[f@0  0]\mkleeneclose{};\mkleeneopen{}l[f@0  1]\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  InstConcl  [\mkleeneopen{}f@0\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  IntSegCases  (-1)
                THEN  Reduce  0
                THEN  Auto)

---

Home Index