---

Step * 2 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. 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)
14. increasing(f1;2)
15. j : ℤ
16. j = 0 ∈ ℤ
⊢ x = (f l[f1 0]) ∈ B
BY
{ (InstHyp [⌜0⌝] (-4)⋅ THEN AllReduce 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.  u  :  A@i
8.  v  :  A@i
9.  x  =  (f  u)
10.  y  =  (f  v)
11.  f1  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||l||@i
12.  increasing(f1;2)
13.  \mforall{}j:\mBbbN{}2.  ([u;  v][j]  =  l[f1  j])
14.  increasing(f1;2)
15.  j  :  \mBbbZ{}
16.  j  =  0
\mvdash{}  x  =  (f  l[f1  0])


By

---

Latex:
(InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-4)\mcdot{}  THEN  AllReduce  THEN  Auto)

---

Home Index