---

Step * 1 3 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)||
⊢ G mklist(x;f)[i] = ((λn.G mklist(n + 1;f)[n]) i) ∈ B
BY
{ (Reduce 0 THEN InstHyp [⌜mklist(x;f)⌝;⌜mklist(i + 1;f)⌝;⌜i + 1⌝] 5⋅ THEN Auto) }

1
.....antecedent..... 
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)||
⊢ (i + 1) ≤ ||mklist(x;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)||
11. j : ℕi + 1
⊢ mklist(x;f)[j] = mklist(i + 1;f)[j] ∈ A

---

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


By

---

Latex:
(Reduce  0  THEN  InstHyp  [\mkleeneopen{}mklist(x;f)\mkleeneclose{};\mkleeneopen{}mklist(i  +  1;f)\mkleeneclose{};\mkleeneopen{}i  +  1\mkleeneclose{}]  5\mcdot{}  THEN  Auto)

---

Home Index