---

Step * 1 2 2 1 of Lemma vdf-wf+


1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. n : ℤ
5. {L:(a:A × b:B × C[a;b]) List| ||L|| = 0 ∈ ℤ}  ⟶ B ⟶ A ∈ Type
6. f : {L:(a:A × b:B × C[a;b]) List| ||L|| = 0 ∈ ℤ}  ⟶ B ⟶ A
7. u : a:A × b:B × C[a;b]
8. ||[u]|| ≤ 1
9. vdf-eq(A;f;[u]) ∈ ℙ
⊢ vdf-eq(A;f;[u]) ⊆r (∀[i:ℕ1]. ((fst([u][i])) = (f firstn(i;[u]) (fst(snd([u][i])))) ∈ A))
BY
{ (RepeatFor 2 (Thin (-1)) THEN RepeatFor 2 (D -1) THEN RepUR ``vdf-eq dep-all`` 0 THEN (RWO "first0" 0 THENA Auto)) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. n : ℤ
5. {L:(a:A × b:B × C[a;b]) List| ||L|| = 0 ∈ ℤ}  ⟶ B ⟶ A ∈ Type
6. f : {L:(a:A × b:B × C[a;b]) List| ||L|| = 0 ∈ ℤ}  ⟶ B ⟶ A
7. a : A
8. b : B
9. u2 : C[a;b]
⊢ :True ⋂ a = (f [] b) ∈ A ⊆r (∀[i:ℕ1]. ((fst([<a, b, u2>][i])) = (f firstn(i;[<a, b, u2>]) (fst(snd([<a, b, u2>][i]))))\000C ∈ A))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type
4.  n  :  \mBbbZ{}
5.  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List|  ||L||  =  0\}    {}\mrightarrow{}  B  {}\mrightarrow{}  A  \mmember{}  Type
6.  f  :  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List|  ||L||  =  0\}    {}\mrightarrow{}  B  {}\mrightarrow{}  A
7.  u  :  a:A  \mtimes{}  b:B  \mtimes{}  C[a;b]
8.  ||[u]||  \mleq{}  1
9.  vdf-eq(A;f;[u])  \mmember{}  \mBbbP{}
\mvdash{}  vdf-eq(A;f;[u])  \msubseteq{}r  (\mforall{}[i:\mBbbN{}1].  ((fst([u][i]))  =  (f  firstn(i;[u])  (fst(snd([u][i]))))))


By

---

Latex:
(RepeatFor  2  (Thin  (-1))
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``vdf-eq  dep-all``  0
  THEN  (RWO  "first0"  0  THENA  Auto))

---

Home Index