---

Step * 1 1 of Lemma vdf-eq-witness


1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. L : (a:A × b:B × C[a;b]) List
6. n : ℤ
7. 0 < n
8. ((n - 1) ≤ ||L||) ⇒ vdf-eq(A;f;firstn(n - 1;L)) ⇒ (Ax ∈ vdf-eq(A;f;firstn(n - 1;L)))
9. n ≤ ||L||
10. vdf-eq(A;f;firstn(n;L))
⊢ Ax ∈ vdf-eq(A;f;firstn(n;L))
BY
{ ((InstLemma `vdf-eq-firstn` [⌜A⌝;⌜B⌝;⌜C⌝;⌜f⌝;⌜L⌝;⌜n - 1⌝]⋅ THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n -1 THENA Auto)
   THEN RWO "-1" (-2)
   THEN RWO "-1" 0
   THEN Thin (-1)) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. L : (a:A × b:B × C[a;b]) List
6. n : ℤ
7. 0 < n
8. ((n - 1) ≤ ||L||) ⇒ vdf-eq(A;f;firstn(n - 1;L)) ⇒ (Ax ∈ vdf-eq(A;f;firstn(n - 1;L)))
9. n ≤ ||L||
10. x:vdf-eq(A;f;firstn(n - 1;L)) ⋂ let tr = L[n - 1] in
                                        (fst(tr)) = (f firstn(n - 1;L) (fst(snd(tr)))) ∈ A
⊢ Ax ∈ x:vdf-eq(A;f;firstn(n - 1;L)) ⋂ let tr = L[n - 1] in
                                           (fst(tr)) = (f firstn(n - 1;L) (fst(snd(tr)))) ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type
4.  f  :  very-dep-fun(A;B;a,b.C[a;b])
5.  L  :  (a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List
6.  n  :  \mBbbZ{}
7.  0  <  n
8.  ((n  -  1)  \mleq{}  ||L||)  {}\mRightarrow{}  vdf-eq(A;f;firstn(n  -  1;L))  {}\mRightarrow{}  (Ax  \mmember{}  vdf-eq(A;f;firstn(n  -  1;L)))
9.  n  \mleq{}  ||L||
10.  vdf-eq(A;f;firstn(n;L))
\mvdash{}  Ax  \mmember{}  vdf-eq(A;f;firstn(n;L))


By

---

Latex:
((InstLemma  `vdf-eq-firstn`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -1  THENA  Auto)
  THEN  RWO  "-1"  (-2)
  THEN  RWO  "-1"  0
  THEN  Thin  (-1))

---

Home Index