theorem String.Slice.Pattern.ForwardSliceSearcher.startsWith_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : ForwardPattern.startsWith pat s = true

theorem String.Slice.Pattern.ForwardSliceSearcher.skipPrefix?_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : ForwardPattern.skipPrefix? pat s = some s.startPos

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instLawfulForwardPattern {pat : Slice} : LawfulForwardPattern pat

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.lawfulForwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) : LawfulForwardPatternModel pat

instance String.Slice.Pattern.Model.ForwardStringSearcher.instLawfulForwardPattern {pat : String} : LawfulForwardPattern pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") : LawfulForwardPatternModel pat

theorem String.Slice.Pattern.BackwardSliceSearcher.endsWith_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : BackwardPattern.endsWith pat s = true

theorem String.Slice.Pattern.BackwardSliceSearcher.skipSuffix?_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : BackwardPattern.skipSuffix? pat s = some s.endPos

instance String.Slice.Pattern.Model.BackwardSliceSearcher.instLawfulBackwardPattern {pat : Slice} : LawfulBackwardPattern pat

theorem String.Slice.Pattern.Model.BackwardSliceSearcher.lawfulBackwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) : LawfulBackwardPatternModel pat

instance String.Slice.Pattern.Model.BackwardStringSearcher.instLawfulBackwardPattern {pat : String} : LawfulBackwardPattern pat

theorem String.Slice.Pattern.Model.BackwardStringSearcher.lawfulBackwardPatternModel {pat : String} (hpat : pat ≠ "") : LawfulBackwardPatternModel pat

theorem String.Slice.startsWith_string_eq_startsWith_toSlice {pat : String} {s : Slice} : s.startsWith pat = s.startsWith pat.toSlice

theorem String.Slice.dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Slice} : s.dropPrefix? pat = s.dropPrefix? pat.toSlice

theorem String.Slice.dropPrefix_string_eq_dropPrefix_toSlice {pat : String} {s : Slice} : s.dropPrefix pat = s.dropPrefix pat.toSlice

theorem String.Slice.skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} : s.skipPrefix? pat = s.skipPrefix? pat.toSlice

theorem String.Slice.Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} : skipPrefix? pat s = skipPrefix? pat.toSlice s

theorem String.Slice.Pos.skipWhile_string_eq_skipWhile_toSlice {pat : String} {s : Slice} (curr : s.Pos) : curr.skipWhile pat = curr.skipWhile pat.toSlice

theorem String.Slice.skipPrefixWhile_string_eq_skipPrefixWhile_toSlice {pat : String} {s : Slice} : s.skipPrefixWhile pat = s.skipPrefixWhile pat.toSlice

theorem String.Slice.dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} : s.dropWhile pat = s.dropWhile pat.toSlice

theorem String.Slice.takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} : s.takeWhile pat = s.takeWhile pat.toSlice

theorem String.Slice.all_string_eq_all_toSlice {pat : String} {s : Slice} : s.all pat = s.all pat.toSlice

theorem String.Slice.endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} : s.endsWith pat = s.endsWith pat.toSlice

theorem String.Slice.skipSuffix?_string_eq_skipSuffix?_toSlice {pat : String} {s : Slice} : s.skipSuffix? pat = s.skipSuffix? pat.toSlice

theorem String.Slice.dropSuffix?_string_eq_dropSuffix?_toSlice {pat : String} {s : Slice} : s.dropSuffix? pat = s.dropSuffix? pat.toSlice

theorem String.Slice.dropSuffix_string_eq_dropSuffix_toSlice {pat : String} {s : Slice} : s.dropSuffix pat = s.dropSuffix pat.toSlice

theorem String.Slice.Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice {pat : String} {s : Slice} : skipSuffix? pat s = skipSuffix? pat.toSlice s

theorem String.Slice.Pos.revSkipWhile_string_eq_revSkipWhile_toSlice {pat : String} {s : Slice} (curr : s.Pos) : curr.revSkipWhile pat = curr.revSkipWhile pat.toSlice

theorem String.Slice.skipSuffixWhile_string_eq_skipSuffixWhile_toSlice {pat : String} {s : Slice} : s.skipSuffixWhile pat = s.skipSuffixWhile pat.toSlice

theorem String.Slice.dropEndWhile_string_eq_dropEndWhile_toSlice {pat : String} {s : Slice} : s.dropEndWhile pat = s.dropEndWhile pat.toSlice

theorem String.Slice.takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : Slice} : s.takeEndWhile pat = s.takeEndWhile pat.toSlice