---

Step * 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)
⊢ nth_tl(||longest-prefix(λL'.(P [u / L']);v)|| + 1;[u / v]) ~ nth_tl(||longest-prefix(λL'.(P [u / L']);v)||;v)
BY
{ (RW (AddrC [1] RecUnfoldTopAbC ) 0 THEN Reduce 0 THEN AutoSplit THEN Try (Complete ((EqCD THEN Auto))))⋅ }

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)
8. (||longest-prefix(λL'.(P [u / L']);v)|| + 1) ≤ 0
⊢ [u / v] ~ nth_tl(||longest-prefix(λL'.(P [u / L']);v)||;v)

---

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)
\mvdash{}  nth\_tl(||longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)||  +  1;[u  /  v]) 
\msim{}  nth\_tl(||longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)||;v)


By

---

Latex:
(RW  (AddrC  [1]  RecUnfoldTopAbC  )  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Try  (Complete  ((EqCD  THEN  Auto))))\mcdot{}

---

Home Index