---

Step * 1 2 2 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. v : (a:A × b:B × C[a;b]) List
9. ||[u / v]|| ≤ 1
10. vdf-eq(A;f;[u / v]) ∈ ℙ
⊢ vdf-eq(A;f;[u / v]) ⊆r (∀[i:ℕ||[u / v]||]. ((fst([u / v][i])) = (f firstn(i;[u / v]) (fst(snd([u / v][i])))) ∈ A))
BY
{ ((DVar `v' THEN Try (((Assert False BY (Reduce -2 THEN Assert ⌜0 ≤ ||v||⌝⋅ THEN Auto)) THEN Trivial)))
   THEN Reduce 0
   ) }

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. 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))

---

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.  v  :  (a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List
9.  ||[u  /  v]||  \mleq{}  1
10.  vdf-eq(A;f;[u  /  v])  \mmember{}  \mBbbP{}
\mvdash{}  vdf-eq(A;f;[u  /  v])  \msubseteq{}r  (\mforall{}[i:\mBbbN{}||[u  /  v]||]
                                                        ((fst([u  /  v][i]))  =  (f  firstn(i;[u  /  v])  (fst(snd([u  /  v][i]))))))


By

---

Latex:
((DVar  `v'
    THEN  Try  (((Assert  False  BY  (Reduce  -2  THEN  Assert  \mkleeneopen{}0  \mleq{}  ||v||\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  Trivial))
    )
  THEN  Reduce  0
  )

---

Home Index