---

Step * of Lemma vdf-eq-firstn

No Annotations
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀i:ℕ||L||.
  (vdf-eq(A;f;firstn(i + 1;L)) ~ x:vdf-eq(A;f;firstn(i;L)) ⋂ let tr = L[i] in
                                                                 (fst(tr)) = (f firstn(i;L) (fst(snd(tr)))) ∈ A)
BY
{ ((Auto THEN RepUR ``vdf-eq let`` 0)
   THEN (RWO "length_firstn" 0 THENA Auto)
   THEN (Assert ¬i + 1 < 1 BY
               Auto)
   THEN RW (AddrC [1] (UnfoldTopAbC)) 0
   THEN (Reduce 0 THENA Auto)
   THEN EqCD
   THEN (Subst' (i + 1) - 1 ~ i 0 THENA Auto)) }

1
1. A : Type
2. f : Top
3. L : (a:Top × b:Top × Top) List
4. i : ℕ||L||
5. ¬i + 1 < 1
⊢ dep-all(i;i@0.let a,b,c = firstn(i + 1;L)[i@0] in 
a = (f firstn(i@0;firstn(i + 1;L)) b) ∈ A) ~ dep-all(i;i@0.let a,b,c = firstn(i;L)[i@0] in 
a = (f firstn(i@0;firstn(i;L)) b) ∈ A)

2
1. A : Type
2. f : Top
3. L : (a:Top × b:Top × Top) List
4. i : ℕ||L||
5. ¬i + 1 < 1
6. @0 : Base
⊢ let a,b,c = firstn(i + 1;L)[i] in 
a = (f firstn(i;firstn(i + 1;L)) b) ∈ A ~ (fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}A:Type.  \mforall{}f:Top.  \mforall{}L:(a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List.  \mforall{}i:\mBbbN{}||L||.
    (vdf-eq(A;f;firstn(i  +  1;L))  \msim{}  x:vdf-eq(A;f;firstn(i;L))  \mcap{}  let  tr  =  L[i]  in
                                                                                                                                  (fst(tr))
                                                                                                                                  =  (f  firstn(i;L)  (fst(snd(tr)))))


By

---

Latex:
((Auto  THEN  RepUR  ``vdf-eq  let``  0)
  THEN  (RWO  "length\_firstn"  0  THENA  Auto)
  THEN  (Assert  \mneg{}i  +  1  <  1  BY
                          Auto)
  THEN  RW  (AddrC  [1]  (UnfoldTopAbC))  0
  THEN  (Reduce  0  THENA  Auto)
  THEN  EqCD
  THEN  (Subst'  (i  +  1)  -  1  \msim{}  i  0  THENA  Auto))

---

Home Index