---

Step * of Lemma listfun_mklist

∀A,B:Type. ∀G:(A List) ⟶ (B List).
  ((∀L:A List. (||L|| = ||G L|| ∈ ℕ))
  ⇒ (∀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))))
  ⇒ (∀f:ℕ ⟶ A. ∀x:ℕ.  ((G mklist(x;f)) = mklist(x;λn.G mklist(n + 1;f)[n]) ∈ (B List))))
BY
{ ((Auto THEN Try (Complete ((RWO "4<" 0  THEN Auto))))
   THEN (Assert ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ) BY
               (Auto⋅
                THEN (InstHyp [⌜mklist(x1;f)⌝] 4⋅ THEN Auto)
                THEN RevHypSubst' (-1) 0
                THEN Auto
                THEN RWO "mklist_length" 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 ∈ ℕ)
⊢ (G mklist(x;f)) = mklist(x;λn.G mklist(n + 1;f)[n]) ∈ (B List)

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}G:(A  List)  {}\mrightarrow{}  (B  List).
    ((\mforall{}L:A  List.  (||L||  =  ||G  L||))
    {}\mRightarrow{}  (\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]))))
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  A.  \mforall{}x:\mBbbN{}.    ((G  mklist(x;f))  =  mklist(x;\mlambda{}n.G  mklist(n  +  1;f)[n]))))


By

---

Latex:
((Auto  THEN  Try  (Complete  ((RWO  "4<"  0    THEN  Auto))))
  THEN  (Assert  \mforall{}x:\mBbbN{}.  (||G  mklist(x;f)||  =  x)  BY
                          (Auto\mcdot{}
                            THEN  (InstHyp  [\mkleeneopen{}mklist(x1;f)\mkleeneclose{}]  4\mcdot{}  THEN  Auto)
                            THEN  RevHypSubst'  (-1)  0
                            THEN  Auto
                            THEN  RWO  "mklist\_length"  0
                            THEN  Auto))
  )

---

Home Index