---

Step * of Lemma vdf-eq_wf1

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[L:(a:A × b:B × C[a;b]) List]. ∀[m:ℤ]. ∀[f:vdf(A;B;a,b.C[a;b];m - 1)].
  vdf-eq(A;f;L) ∈ Type supposing ||L|| ≤ m
BY
{ (InstLemma `vdf-wf` [] THEN RepeatFor 3 (ParallelLast') THEN Intros THEN Unhide) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. ∀n:ℕ
     ((vdf(A;B;a,b.C[a;b];n) ∈ Type)
     ∧ (∀f:vdf(A;B;a,b.C[a;b];n). ∀L:(a:A × b:B × C[a;b]) List.  ((||L|| ≤ (n + 1)) ⇒ (vdf-eq(A;f;L) ∈ ℙ))))
5. L : (a:A × b:B × C[a;b]) List
6. m : ℤ
7. f : vdf(A;B;a,b.C[a;b];m - 1)
8. ||L|| ≤ m
⊢ vdf-eq(A;f;L) ∈ Type

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List].  \mforall{}[m:\mBbbZ{}].
\mforall{}[f:vdf(A;B;a,b.C[a;b];m  -  1)].
    vdf-eq(A;f;L)  \mmember{}  Type  supposing  ||L||  \mleq{}  m


By

---

Latex:
(InstLemma  `vdf-wf`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Intros  THEN  Unhide)

---

Home Index