---

Step * 2 of Lemma longest-prefix_property'


1. [T] : Type
⊢ ∀P:T List+ ⟶ 𝔹
    (longest-prefix(P;[]) ≤ []
    ∧ longest-prefix(P;[]) < [] supposing 0 < ||[]||
    ∧ (((longest-prefix(P;[]) = [] ∈ (T List)) ∧ (∀L':T List. ([] < L' ⇒ L' < [] ⇒ (¬↑(P L')))))
      ∨ (0 < ||longest-prefix(P;[])||
        ∧ (↑(P longest-prefix(P;[])))
        ∧ (∀L':T List. (longest-prefix(P;[]) < L' ⇒ L' < [] ⇒ (¬↑(P L')))))))
BY
{ xxx(RecUnfold `longest-prefix` 0
      THEN Reduce 0
      THEN Auto
      THEN OrLeft
      THEN Auto
      THEN (InstLemma `proper-iseg-length` [⌜T⌝;⌜L'⌝;⌜[]⌝]⋅ THEN Auto')
      THEN ThinTrivial
      THEN Auto')xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}P:T  List\msupplus{}  {}\mrightarrow{}  \mBbbB{}
        (longest-prefix(P;[])  \mleq{}  []
        \mwedge{}  longest-prefix(P;[])  <  []  supposing  0  <  ||[]||
        \mwedge{}  (((longest-prefix(P;[])  =  [])  \mwedge{}  (\mforall{}L':T  List.  ([]  <  L'  {}\mRightarrow{}  L'  <  []  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  L')))))
            \mvee{}  (0  <  ||longest-prefix(P;[])||
                \mwedge{}  (\muparrow{}(P  longest-prefix(P;[])))
                \mwedge{}  (\mforall{}L':T  List.  (longest-prefix(P;[])  <  L'  {}\mRightarrow{}  L'  <  []  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  L')))))))


By

---

Latex:
xxx(RecUnfold  `longest-prefix`  0
        THEN  Reduce  0
        THEN  Auto
        THEN  OrLeft
        THEN  Auto
        THEN  (InstLemma  `proper-iseg-length`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L'\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto')
        THEN  ThinTrivial
        THEN  Auto')xxx

---

Home Index