---

Step * 1 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 ∈ ℕ)
⊢ ||G mklist(x;f)|| = ||mklist(x;λn.G mklist(n + 1;f)[n])|| ∈ ℤ
BY
{ (RWO "mklist_length" 0 THEN Auto) }

---

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


By

---

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

---

Home Index