---

Step * of Lemma longest-prefix_property'

∀[T:Type]
  ∀L:T List. ∀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')))))))
BY
{ InductionOnListA }

1
.....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) ⟶ ℙ

2
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')))))))

3
1. [T] : Type
2. L : T
3. L1 : T List
4. ∀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')))))))
⊢ ∀P:T List+ ⟶ 𝔹
    (longest-prefix(P;[L / L1]) ≤ [L / L1]
    ∧ longest-prefix(P;[L / L1]) < [L / L1] supposing 0 < ||[L / L1]||
    ∧ (((longest-prefix(P;[L / L1]) = [] ∈ (T List)) ∧ (∀L':T List. ([] < L' ⇒ L' < [L / L1] ⇒ (¬↑(P L')))))
      ∨ (0 < ||longest-prefix(P;[L / L1])||
        ∧ (↑(P longest-prefix(P;[L / L1])))
        ∧ (∀L':T List. (longest-prefix(P;[L / L1]) < L' ⇒ L' < [L / L1] ⇒ (¬↑(P L')))))))

4
.....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'))))))) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \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')))))))


By

---

Latex:
InductionOnListA

---

Home Index