---

Step * 4 of Lemma longest-prefix_property'

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

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  MemTypeCD
        THEN  Auto
        THEN  InstLemma  `proper-iseg-length`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}L'\mkleeneclose{}]\mcdot{}
        THEN  Auto'
        THEN  InstLemma  `proper-iseg-length`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}longest-prefix(P;L1)\mkleeneclose{};\mkleeneopen{}L'\mkleeneclose{}]\mcdot{}
        THEN  Auto')xxx

---

Home Index