theorem String.Slice.toList_splitToSubslice_bool {s : Slice} {p : Char → Bool} : List.map (copy ∘ Subslice.toSlice) (s.splitToSubslice p).toList = List.map ofList (List.splitOnP p s.copy.toList)

theorem String.Slice.toList_split_bool {s : Slice} {p : Char → Bool} : List.map copy (s.split p).toList = List.map ofList (List.splitOnP p s.copy.toList)

theorem String.Slice.Pattern.Model.split_bool_eq_internal {p : Char → Bool} {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : Model.split p f curr hle = if h : curr = s.endPos then [s.subslice f curr hle] else if p (curr.get h) = true then s.subslice f curr hle :: Model.split p (curr.next h) (curr.next h) ⋯ else Model.split p f (curr.next h) ⋯

theorem String.Slice.Pattern.Model.split_eq_split_decide {p : Char → Prop} [DecidablePred p] {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : Model.split p f curr hle = Model.split (fun (x : Char) => decide (p x)) f curr hle

theorem String.Slice.toList_splitToSubslice_prop {s : Slice} {p : Char → Prop} [DecidablePred p] : List.map (copy ∘ Subslice.toSlice) (s.splitToSubslice p).toList = List.map ofList (List.splitOnP (fun (b : Char) => decide (p b)) s.copy.toList)

theorem String.Slice.toList_split_prop {s : Slice} {p : Char → Prop} [DecidablePred p] : List.map copy (s.split p).toList = List.map ofList (List.splitOnP (fun (b : Char) => decide (p b)) s.copy.toList)

theorem String.toList_split_bool {s : String} {p : Char → Bool} : List.map Slice.copy (s.split p).toList = List.map ofList (List.splitOnP p s.toList)

theorem String.toList_split_prop {s : String} {p : Char → Prop} [DecidablePred p] : List.map Slice.copy (s.split p).toList = List.map ofList (List.splitOnP (fun (b : Char) => decide (p b)) s.toList)