---

Step * 1 of Lemma vdf-eq-firstn


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)
BY
{ ((Enough to prove ∀i:ℕ. ∀L:(a:Top × b:Top × Top) List.
                      (i < ||L||
                      ⇒ (∀j:{i + 1...}
                            (dep-all(i;i@0.let a,b,c = firstn(j;L)[i@0] in 
                            a = (f firstn(i@0;firstn(j;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))))
     Because (InstHyp [⌜i⌝;⌜L⌝;⌜i + 1⌝] (-1)⋅ THEN Auto))
   THEN ThinVar `i'
   THEN ThinVar `L'
   THEN InductionOnNat
   THEN Intros
   THEN Try ((Assert ¬i < 1 BY Complete (Auto)))
   THEN Unfold `dep-all` 0
   THEN (Reduce 0 THENA Auto)
   THEN EqCD
   THEN ((RWO "5" 0 THEN Auto) ORELSE (RWO "select-firstn firstn-firstn" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  Top
3.  L  :  (a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List
4.  i  :  \mBbbN{}||L||
5.  \mneg{}i  +  1  <  1
\mvdash{}  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))  \msim{}  dep-all(i;i@0.let  a,b,c  =  firstn(i;L)[i@0]  in 
a  =  (f  firstn(i@0;firstn(i;L))  b))


By

---

Latex:
((Enough  to  prove  \mforall{}i:\mBbbN{}.  \mforall{}L:(a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List.
                                        (i  <  ||L||
                                        {}\mRightarrow{}  (\mforall{}j:\{i  +  1...\}
                                                    (dep-all(i;i@0.let  a,b,c  =  firstn(j;L)[i@0]  in 
                                                    a  =  (f  firstn(i@0;firstn(j;L))  b)) 
                                                    \msim{}  dep-all(i;i@0.let  a,b,c  =  firstn(i;L)[i@0]  in 
                                                    a  =  (f  firstn(i@0;firstn(i;L))  b)))))
      Because  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i  +  1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  ThinVar  `i'
  THEN  ThinVar  `L'
  THEN  InductionOnNat
  THEN  Intros
  THEN  Try  ((Assert  \mneg{}i  <  1  BY  Complete  (Auto)))
  THEN  Unfold  `dep-all`  0
  THEN  (Reduce  0  THENA  Auto)
  THEN  EqCD
  THEN  ((RWO  "5"  0  THEN  Auto)  ORELSE  (RWO  "select-firstn  firstn-firstn"  0  THEN  Auto)))

---

Home Index