---

Step * of Lemma longest-prefix-decomp

∀[T:Type]. ∀[L:T List]. ∀[P:(T List) ⟶ 𝔹].  (L ~ longest-prefix(P;L) @ nth_tl(||longest-prefix(P;L)||;L))
BY
{ (InductionOnList
   THEN RecUnfold `longest-prefix` 0
   THEN (Reduce 0 THEN Try (Complete ((Reduce 0 THEN Auto))))
   THEN (D 0 THENA Auto)
   THEN Try (Complete (Auto))
   THEN RepUR ``let`` 0
   THEN (InstHyp [⌜λL'.(P [u / L'])⌝] (-2)⋅ THENA Auto)
   THEN AutoSplit
   THEN Try (RepeatFor 2 (AutoSplit))
   THEN EqCD
   THEN Try (Trivial)
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)
   THEN Try (Trivial)) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[P:(T List) ⟶ 𝔹]. (v ~ longest-prefix(P;v) @ nth_tl(||longest-prefix(P;v)||;v))
5. P : (T List) ⟶ 𝔹
6. ¬(longest-prefix(λL'.(P [u / L']);v) = [] ∈ (T List))
7. v ~ longest-prefix(λL'.(P [u / L']);v) @ nth_tl(||longest-prefix(λL'.(P [u / L']);v)||;v)
⊢ nth_tl(||longest-prefix(λL'.(P [u / L']);v)|| + 1;[u / v]) ~ nth_tl(||longest-prefix(λL'.(P [u / L']);v)||;v)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbB{}].
    (L  \msim{}  longest-prefix(P;L)  @  nth\_tl(||longest-prefix(P;L)||;L))


By

---

Latex:
(InductionOnList
  THEN  RecUnfold  `longest-prefix`  0
  THEN  (Reduce  0  THEN  Try  (Complete  ((Reduce  0  THEN  Auto))))
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``let``  0
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}L'.(P  [u  /  L'])\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  Try  (RepeatFor  2  (AutoSplit))
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (Trivial))

---

Home Index