@[implicit_reducible]

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instForwardPatternModel {pat : Slice} : ForwardPatternModel pat

Equations

• String.Slice.Pattern.Model.ForwardSliceSearcher.instForwardPatternModel = { Matches := fun (s : String) => s ≠ "" ∧ s = pat.copy, not_matches_empty := ⋯ }

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instNoPrefixForwardPatternModel {pat : Slice} : NoPrefixForwardPatternModel pat

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : IsMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (pat.copy ++ t₂) ∧ pos₂.Splits (t₁ ++ pat.copy) t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) : IsLongestMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.offset_of_isLongestMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) (h' : IsLongestMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : MatchesAt pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits t₁ (pat.copy ++ t₂)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : MatchesAt pat pos ↔ ∃ (h : Pos.Raw.IsValidForSlice s (pos.offset.increaseBy pat.utf8ByteSize)), IsLongestMatchAt pat pos (s.pos (pos.offset.increaseBy pat.utf8ByteSize) h)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_getElem {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : MatchesAt pat pos ↔ ∃ (h : pos.offset.byteIdx + pat.copy.toByteArray.size ≤ s.copy.toByteArray.size), ∀ (j : Nat) (hj : j < pat.copy.toByteArray.size), pat.copy.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j]

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.le_of_matchesAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) (h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos