---

Step * of Lemma longest-prefix_property

No Annotations
∀[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 ⇒ (¬↑(P L')))))
      ∨ ((↑(P longest-prefix(P;L))) ∧ (∀L':T List. (longest-prefix(P;L) < L' ⇒ L' < L ⇒ (¬↑(P L')))))))
BY
{ (InductionOnList
   THEN RecUnfold `longest-prefix` 0
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN Try (Complete ((Auto
                        THEN OrLeft
                        THEN Auto
                        THEN (InstLemma `proper-iseg-length` [⌜T⌝;⌜L'⌝;⌜[]⌝]⋅ THEN Auto')
                        THEN ThinTrivial
                        THEN Auto')))
   THEN RepUR ``let`` 0
   THEN (InstHyp [⌜λL'.(P [u / L'])⌝] (-2)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜longest-prefix(λL'.(P [u / L']);v) = pr ∈ (T List)⌝⋅ THENA Auto)
   THEN All Thin
   THEN DVar `pr'
   THEN Reduce 0) }

1
1. [T] : Type
2. u : T
3. v : T List
4. P : (T List) ⟶ 𝔹
⊢ ([] ≤ v
∧ [] < v supposing 0 < ||v||
∧ ((([] = [] ∈ (T List)) ∧ (∀L':T List. (L' < v ⇒ (¬↑(P [u / L'])))))
  ∨ ((↑(P [u])) ∧ (∀L':T List. ([] < L' ⇒ L' < v ⇒ (¬↑(P [u / L'])))))))
⇒ (if null(v) then []
    if P [u] then [u]
    else []
    fi  ≤ [u / v]
   ∧ if null(v) then [] if P [u] then [u] else [] fi  < [u / v] supposing 0 < ||v|| + 1
   ∧ (((if null(v) then [] if P [u] then [u] else [] fi  = [] ∈ (T List)) ∧ (∀L':T List. (L' < [u / v] ⇒ (¬↑(P L')))))
     ∨ ((↑(P if null(v) then [] if P [u] then [u] else [] fi ))
       ∧ (∀L':T List. (if null(v) then [] if P [u] then [u] else [] fi  < L' ⇒ L' < [u / v] ⇒ (¬↑(P L')))))))

2
1. [T] : Type
2. u : T
3. v : T List
4. P : (T List) ⟶ 𝔹
5. u1 : T
6. v1 : T List
⊢ ([u1 / v1] ≤ v
∧ [u1 / v1] < v supposing 0 < ||v||
∧ ((([u1 / v1] = [] ∈ (T List)) ∧ (∀L':T List. (L' < v ⇒ (¬↑(P [u / L'])))))
  ∨ ((↑(P [u; [u1 / v1]])) ∧ (∀L':T List. ([u1 / v1] < L' ⇒ L' < v ⇒ (¬↑(P [u / L'])))))))
⇒ ([u; [u1 / v1]] ≤ [u / v]
   ∧ [u; [u1 / v1]] < [u / v] supposing 0 < ||v|| + 1
   ∧ ((([u; [u1 / v1]] = [] ∈ (T List)) ∧ (∀L':T List. (L' < [u / v] ⇒ (¬↑(P L')))))
     ∨ ((↑(P [u; [u1 / v1]])) ∧ (∀L':T List. ([u; [u1 / v1]] < L' ⇒ L' < [u / v] ⇒ (¬↑(P L')))))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}P:(T  List)  {}\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'  <  L  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  L')))))
            \mvee{}  ((\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:
(InductionOnList
  THEN  RecUnfold  `longest-prefix`  0
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Complete  ((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')))
  THEN  RepUR  ``let``  0
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}L'.(P  [u  /  L'])\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}longest-prefix(\mlambda{}L'.(P  [u  /  L']);v)  =  pr\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  DVar  `pr'
  THEN  Reduce  0)

---

Home Index