---

Step * of Lemma select-qv-add

∀[as,bs:Top List].  ∀[i:ℕdimension(as)]. (qv-add(as;bs)[i] ~ as[i] + bs[i]) supposing dimension(as) = dimension(bs) ∈ ℤ
BY
{ xxx(Unfold `qv-dim` 0
      THEN InductionOnList
      THEN RecUnfold `qv-add` 0
      THEN Reduce 0
      THEN Auto'
      THEN CaseNat 0 `i'
      THEN DVar `bs'
      THEN All Reduce
      THEN Try (Trivial)
      THEN Try (Complete (Auto'))
      THEN RWO "select-cons-tl" 0
      THEN Auto'
      THEN (RWO "4" 0 THENA Auto)
      THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[as,bs:Top  List].
    \mforall{}[i:\mBbbN{}dimension(as)].  (qv-add(as;bs)[i]  \msim{}  as[i]  +  bs[i])  supposing  dimension(as)  =  dimension(bs)


By

---

Latex:
xxx(Unfold  `qv-dim`  0
        THEN  InductionOnList
        THEN  RecUnfold  `qv-add`  0
        THEN  Reduce  0
        THEN  Auto'
        THEN  CaseNat  0  `i'
        THEN  DVar  `bs'
        THEN  All  Reduce
        THEN  Try  (Trivial)
        THEN  Try  (Complete  (Auto'))
        THEN  RWO  "select-cons-tl"  0
        THEN  Auto'
        THEN  (RWO  "4"  0  THENA  Auto)
        THEN  Auto')xxx

---

Home Index