---

Step * 1 3 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)||
⊢ G mklist(x;f)[i] = mklist(x;λn.G mklist(n + 1;f)[n])[i] ∈ B
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. n : ℕx
⊢ n < ||G mklist(n + 1;f)||

2
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)||
⊢ G mklist(x;f)[i] = ((λn.G mklist(n + 1;f)[n]) i) ∈ B

---

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)||
\mvdash{}  G  mklist(x;f)[i]  =  mklist(x;\mlambda{}n.G  mklist(n  +  1;f)[n])[i]


By

---

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

---

Home Index