---

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)
BY
{ ((InstLemma `vdf-wf` [] THEN RepeatFor 3 (ParallelLast')) THEN Intro THEN Unhide THEN (Decide ⌜0 ≤ n⌝⋅ THENA Auto)) }

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. n : ℤ
6. 0 ≤ n
⊢ vdf(A;B;a,b.C[a;b];n) ∈ Type

2
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. n : ℤ
6. ¬(0 ≤ n)
⊢ vdf(A;B;a,b.C[a;b];n) ∈ Type

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbZ{}].    (vdf(A;B;a,b.C[a;b];n)  \mmember{}  Type)


By

---

Latex:
((InstLemma  `vdf-wf`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  Intro
  THEN  Unhide
  THEN  (Decide  \mkleeneopen{}0  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index