---

Step * 1 of Lemma longest-prefix_property'

.....wf..... 
1. T : Type
⊢ λL.∀P:T List+ ⟶ 𝔹
       (longest-prefix(P;L) ≤ L
       ∧ longest-prefix(P;L) < L supposing 0 < ||L||
       ∧ (((longest-prefix(P;L) = [] ∈ (T List)) ∧ (∀L':T List. ([] < L' ⇒ L' < L ⇒ (¬↑(P L')))))
         ∨ (0 < ||longest-prefix(P;L)||
           ∧ (↑(P longest-prefix(P;L)))
           ∧ (∀L':T List. (longest-prefix(P;L) < L' ⇒ L' < L ⇒ (¬↑(P L'))))))) ∈ (T List) ⟶ ℙ
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;L)⌝;⌜L'⌝]⋅
      THEN Auto')xxx }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
\mvdash{}  \mlambda{}L.\mforall{}P:T  List\msupplus{}  {}\mrightarrow{}  \mBbbB{}
              (longest-prefix(P;L)  \mleq{}  L
              \mwedge{}  longest-prefix(P;L)  <  L  supposing  0  <  ||L||
              \mwedge{}  (((longest-prefix(P;L)  =  [])  \mwedge{}  (\mforall{}L':T  List.  ([]  <  L'  {}\mRightarrow{}  L'  <  L  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  L')))))
                  \mvee{}  (0  <  ||longest-prefix(P;L)||
                      \mwedge{}  (\muparrow{}(P  longest-prefix(P;L)))
                      \mwedge{}  (\mforall{}L':T  List.  (longest-prefix(P;L)  <  L'  {}\mRightarrow{}  L'  <  L  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  L')))))))  \mmember{}  (T  List)  {}\mrightarrow{}  \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;L)\mkleeneclose{};\mkleeneopen{}L'\mkleeneclose{}]\mcdot{}
        THEN  Auto')xxx

---

Home Index