---

Step * 1 1 of Lemma longest-prefix-decomp


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)
8. (||longest-prefix(λL'.(P [u / L']);v)|| + 1) ≤ 0
⊢ [u / v] ~ nth_tl(||longest-prefix(λL'.(P [u / L']);v)||;v)
BY
{ (Assert ⌜False⌝⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbB{}].  (v  \msim{}  longest-prefix(P;v)  @  nth\_tl(||longest-prefix(P;v)||;v))
5.  P  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
6.  \mneg{}(longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)  =  [])
7.  v  \msim{}  longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)  @  nth\_tl(||longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)||;v)
8.  (||longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)||  +  1)  \mleq{}  0
\mvdash{}  [u  /  v]  \msim{}  nth\_tl(||longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)||;v)


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index