---

Step * of Lemma fseg_extend

∀[T:Type]
  ∀l1:T List. ∀v:T. ∀l2:T List.
    (fseg(T;l1;l2) ⇒ fseg(T;[v / l1];l2) supposing ||l1|| < ||l2|| c∧ (l2[||l2|| - ||l1|| + 1] = v ∈ T))
BY
{ xxx(Unfold `fseg` 0
      THEN Auto'
      THEN D -1
      THEN ExRepD
      THEN WeakSubstFor ⌜l2⌝ 0⋅
      THEN (Assert ¬↑null(L) BY
                  (DVar `L' THEN Reduce 0 THEN Auto THEN (HypSubst' -3 -2 THENM (Reduce (-2))) THEN Auto))
      THEN ((InstLemma `last_lemma` [⌜T⌝; ⌜L⌝])⋅ THENA Auto))xxx }

1
1. [T] : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1) ∈ (T List)
7. ||l1|| < ||l2||
8. l2[||l2|| - ||l1|| + 1] = v ∈ T
9. ¬↑null(L)
10. ∃L':T List. (L = (L' @ [last(L)]) ∈ (T List))
⊢ ∃L@0:T List. ((L @ l1) = (L@0 @ [v / l1]) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}l1:T  List.  \mforall{}v:T.  \mforall{}l2:T  List.
        (fseg(T;l1;l2)
        {}\mRightarrow{}  fseg(T;[v  /  l1];l2)  supposing  ||l1||  <  ||l2||  c\mwedge{}  (l2[||l2||  -  ||l1||  +  1]  =  v))


By

---

Latex:
xxx(Unfold  `fseg`  0
        THEN  Auto'
        THEN  D  -1
        THEN  ExRepD
        THEN  WeakSubstFor  \mkleeneopen{}l2\mkleeneclose{}  0\mcdot{}
        THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                                (DVar  `L'
                                  THEN  Reduce  0
                                  THEN  Auto
                                  THEN  (HypSubst'  -3  -2  THENM  (Reduce  (-2)))
                                  THEN  Auto))
        THEN  ((InstLemma  `last\_lemma`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THENA  Auto))xxx

---

Home Index