---

Step * of Lemma l_before_map

∀[A,B:Type].
  ∀l:A List. ∀f:A ⟶ B. ∀x,y:B.
    (x before y ∈ map(f;l) ⇐⇒ ∃u,v:A. ((x = (f u) ∈ B) ∧ (y = (f v) ∈ B) ∧ u before v ∈ l))
BY
{ TACTIC:(Auto THEN All(Unfold `l_before`) THEN All(Unfold `sublist`) THEN AllReduce THEN Try (ExRepD)) }

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

2
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. u : A@i
8. v : A@i
9. x = (f u) ∈ B
10. y = (f v) ∈ B
11. f1 : ℕ2 ⟶ ℕ||l||@i
12. increasing(f1;2)
13. ∀j:ℕ2. ([u; v][j] = l[f1 j] ∈ A)
⊢ ∃f@0:ℕ2 ⟶ ℕ||map(f;l)||. (increasing(f@0;2) ∧ (∀j:ℕ2. ([x; y][j] = map(f;l)[f@0 j] ∈ B)))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}l:A  List.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}x,y:B.
        (x  before  y  \mmember{}  map(f;l)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}u,v:A.  ((x  =  (f  u))  \mwedge{}  (y  =  (f  v))  \mwedge{}  u  before  v  \mmember{}  l))


By

---

Latex:
TACTIC:(Auto
                THEN  All(Unfold  `l\_before`)
                THEN  All(Unfold  `sublist`)
                THEN  AllReduce
                THEN  Try  (ExRepD))

---

Home Index