---

Step * 1 3 2 2 of Lemma listfun_mklist


1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
9. i : ℕ
10. i < ||G mklist(x;f)||
11. j : ℕi + 1
⊢ mklist(x;f)[j] = mklist(i + 1;f)[j] ∈ A
BY
{ (RWO "mklist_select" 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
9. i : ℕ
10. i < ||G mklist(x;f)||
11. j : ℤ
12. 0 ≤ j
13. j < i + 1
⊢ j < x

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  G  :  (A  List)  {}\mrightarrow{}  (B  List)
4.  \mforall{}L:A  List.  (||L||  =  ||G  L||)
5.  \mforall{}L1,L2:A  List.  \mforall{}i:\mBbbN{}.
          ((i  \mleq{}  ||L1||)  {}\mRightarrow{}  (i  \mleq{}  ||L2||)  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  (L1[j]  =  L2[j]))  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  (G  L1[j]  =  G  L2[j])))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  A
7.  x  :  \mBbbN{}
8.  \mforall{}x:\mBbbN{}.  (||G  mklist(x;f)||  =  x)
9.  i  :  \mBbbN{}
10.  i  <  ||G  mklist(x;f)||
11.  j  :  \mBbbN{}i  +  1
\mvdash{}  mklist(x;f)[j]  =  mklist(i  +  1;f)[j]


By

---

Latex:
(RWO  "mklist\_select"  0  THEN  Auto)

---

Home Index