---

Step * of Lemma longest-prefix-is-nil

∀[T:Type]. ∀[L:T List]. ∀[P:(T List) ⟶ 𝔹].
  ∀[L':T List]. (¬↑(P L')) supposing (L' < L and [] < L') supposing longest-prefix(P;L) = [] ∈ (T List)
BY
{ xxx(InstLemma `longest-prefix_property` []
      THEN RepeatFor 3 (ParallelLast')
      THEN MoveToConcl (-1)
      THEN (GenConcl ⌜longest-prefix(P;L) = pr ∈ (T List)⌝⋅ THENA Auto)
      THEN All Thin
      THEN Auto
      THEN SplitOrHyps
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[L':T  List].  (\mneg{}\muparrow{}(P  L'))  supposing  (L'  <  L  and  []  <  L')  supposing  longest-prefix(P;L)  =  []


By

---

Latex:
xxx(InstLemma  `longest-prefix\_property`  []
        THEN  RepeatFor  3  (ParallelLast')
        THEN  MoveToConcl  (-1)
        THEN  (GenConcl  \mkleeneopen{}longest-prefix(P;L)  =  pr\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  All  Thin
        THEN  Auto
        THEN  SplitOrHyps
        THEN  Auto)xxx

---

Home Index