---

Step * of Lemma vdf-wf

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type].
  ∀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) ∈ ℙ))))
BY
{ ((InstLemma `vdf-wf+` [] THEN RepeatFor 4 (ParallelLast')) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].
    \mforall{}n:\mBbbN{}
        ((vdf(A;B;a,b.C[a;b];n)  \mmember{}  Type)
        \mwedge{}  (\mforall{}f:vdf(A;B;a,b.C[a;b];n).  \mforall{}L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List.
                  ((||L||  \mleq{}  (n  +  1))  {}\mRightarrow{}  (vdf-eq(A;f;L)  \mmember{}  \mBbbP{}))))


By

---

Latex:
((InstLemma  `vdf-wf+`  []  THEN  RepeatFor  4  (ParallelLast'))  THEN  Auto)

---

Home Index