---

Step * of Lemma vdf-eq-firstn-general

No Annotations
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀i:ℕ||L|| + 1.
  (vdf-eq(A;f;firstn(i;L)) ~ if (i =z 0)
  then True
  else x:vdf-eq(A;f;firstn(i - 1;L)) ⋂ let tr = L[i - 1] in
                                           (fst(tr)) = (f firstn(i - 1;L) (fst(snd(tr)))) ∈ A
  fi )
BY
{ (Auto
   THEN (AutoSplit
         THENL [(HypSubst' (-1) 0 THEN (RWO "first0" 0 THENA Auto) THEN RepUR ``vdf-eq dep-all`` 0 THEN Auto)
               ; (RWO "vdf-eq-firstn<" 0 THEN Auto)]
        )
   ) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (AutoSplit
              THENL  [(HypSubst'  (-1)  0
                              THEN  (RWO  "first0"  0  THENA  Auto)
                              THEN  RepUR  ``vdf-eq  dep-all``  0
                              THEN  Auto)
                          ;  (RWO  "vdf-eq-firstn<"  0  THEN  Auto)]
            )
  )

---

Home Index