Semi-global and overlap alignment

TheoremThe floored list maximum is nonnegative#✓fully proved

For every list \(L\) of integers, the maximum of \(L\) with floor \(0\) (which is \(0\) for the empty list) is at least \(0\).

theorem zero_le_listMax {xs : List ℤ} : 0 ≤ listMax xs

Uses 1 · Used by 1

Statement usesMaximum of an integer list with floor zero

Used byThe overlap score is nonnegative

DefinitionOverlap pairs#✓fully proved

The overlap pairs of sequences \(x\) and \(y\) are the pairs \((x', y')\) in which \(x'\) is a suffix of \(x\) and \(y'\) is a prefix of \(y\), or \(x'\) is a prefix of \(x\) and \(y'\) is a suffix of \(y\). Prefixes and suffixes include the empty sequence and the whole sequence; the pairs are listed with the suffix–prefix pairs first, and the list can contain repetitions.

def overlapPairs (xs ys : List α) : List (List α × List α) :=
  (xs.tails.product ys.inits) ++ (xs.inits.product ys.tails)

Used by 6

Used byThe overlap score is attained · Overlap-pair scores are at most the overlap score · Overlap alignment score · Upper bounds for the overlap score · The overlap score is at most the local score · The overlap score is nonnegative

DefinitionOverlap alignment score#✓fully proved

Given a substitution score \(\sigma\) and a gap score \(g\), the overlap score of sequences \(s\) and \(t\) is the maximum, with floor \(0\), of the Needleman–Wunsch scores of the overlap pairs of \(s\) and \(t\): the pairs \((s', t')\) where \(s'\) is a suffix of \(s\) and \(t'\) a prefix of \(t\), or \(s'\) is a prefix of \(s\) and \(t'\) a suffix of \(t\).

The pair of two empty sequences is an overlap pair with score \(0\), so the floor never changes the value: this is the best alignment score of a suffix of one sequence against a prefix of the other.

def overlapScore (xs ys : List α) : ℤ :=
  listMax ((overlapPairs xs ys).map (fun p => nwScore σ gap p.1 p.2))

Uses 3 · Used by 5

Statement usesMaximum of an integer list with floor zero · Needleman–Wunsch score · Overlap pairs

Used byThe overlap score is attained · Overlap-pair scores are at most the overlap score · Upper bounds for the overlap score · The overlap score is at most the local score · The overlap score is nonnegative

TheoremOverlap-pair scores are at most the overlap score#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. If \((x', y')\) is an overlap pair of sequences \(x\) and \(y\), then the Needleman–Wunsch score of \(x'\) against \(y'\) is at most the overlap score of \(x\) and \(y\), both taken with \(\sigma\) and \(g\).

theorem nwScore_le_overlapScore {xs' ys' xs ys : List α}
    (h : (xs', ys') ∈ overlapPairs xs ys) :
    nwScore σ gap xs' ys' ≤ overlapScore σ gap xs ys

Uses 4

Statement usesNeedleman–Wunsch score · Overlap pairs · Overlap alignment score

Proof usesMaximum of an integer list with floor zero

TheoremUpper bounds for the overlap score#✓fully proved

Fix a substitution score \(\sigma\) and a gap score \(g\), and sequences \(s\) and \(t\). If an integer \(b\) is at least the Needleman–Wunsch score of every overlap pair of \(s\) and \(t\) (a suffix of \(s\) with a prefix of \(t\), or a prefix of \(s\) with a suffix of \(t\)), then the overlap score of \(s\) and \(t\) is at most \(b\).

theorem overlapScore_le {xs ys : List α} {y : ℤ}
    (h : ∀ p ∈ overlapPairs xs ys, nwScore σ gap p.1 p.2 ≤ y) :
    overlapScore σ gap xs ys ≤ y

Uses 4 · Used by 1

Statement usesNeedleman–Wunsch score · Overlap pairs · Overlap alignment score

Proof usesMaximum of an integer list with floor zero

Used byThe overlap score is at most the local score

TheoremThe overlap score is attained#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. For all sequences \(x\) and \(y\) there is an overlap pair \((x', y')\) of \(x\) and \(y\) such that the Needleman–Wunsch score of \(x'\) against \(y'\) (with \(\sigma\) and \(g\)) equals the overlap score of \(x\) and \(y\).

theorem exists_nwScore_eq_overlapScore (xs ys : List α) :
    ∃ p ∈ overlapPairs xs ys, nwScore σ gap p.1 p.2 = overlapScore σ gap xs ys

Uses 4

Statement usesNeedleman–Wunsch score · Overlap pairs · Overlap alignment score

Proof usesMaximum of an integer list with floor zero

TheoremThe overlap score is nonnegative#✓fully proved

For every substitution score \(\sigma\), gap score \(g\) and sequences \(s\) and \(t\), the overlap score of \(s\) and \(t\) is at least \(0\).

The pair of two empty sequences is an overlap pair, and its score is \(0\).

theorem overlapScore_nonneg (xs ys : List α) : 0 ≤ overlapScore σ gap xs ys

Uses 4

Statement usesOverlap alignment score

Proof usesNeedleman–Wunsch score · Overlap pairs · The floored list maximum is nonnegative

DefinitionInfixes#✓fully proved

The infixes of a sequence \(y\) are its contiguous substrings: the sequences \(l\) such that \(y\) is the concatenation of \(s\), \(l\) and \(t\) for some sequences \(s\) and \(t\), including the empty sequence and \(y\) itself. They are listed as the suffixes of the prefixes of \(y\), so the list can contain repetitions.

def infixes (ys : List α) : List (List α) :=
  ys.inits.flatMap (fun pre => pre.tails)

Used by 5

Used byThe fitting score is attained · Fitting score · Upper bounds on the fitting score · The fitting score is at most the local score · Infix scores are at most the fitting score

DefinitionFitting score#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. The fitting score of a sequence \(x\) against a sequence \(y\) is the maximum, over all infixes \(l\) of \(y\) (including the empty one), of the Needleman–Wunsch score of \(x\) against \(l\) with \(\sigma\) and \(g\): the best global alignment score of \(x\) against a substring of \(y\).

The empty infix is always a candidate, so the maximum is attained. Unlike the overlap score, the fitting score is not floored at \(0\): it can be negative when every fitting alignment scores negatively.

def fittingScore (xs ys : List α) : ℤ :=
  ((infixes ys).map (fun l => nwScore σ gap xs l)).foldl max (nwScore σ gap xs [])

Uses 2 · Used by 4

Statement usesInfixes · Needleman–Wunsch score

Used byThe fitting score is attained · Upper bounds on the fitting score · The fitting score is at most the local score · Infix scores are at most the fitting score

TheoremInfix scores are at most the fitting score#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. If \(l\) is an infix of a sequence \(y\), then for every sequence \(x\) the Needleman–Wunsch score of \(x\) against \(l\) is at most the fitting score of \(x\) against \(y\), both taken with \(\sigma\) and \(g\).

theorem nwScore_le_fittingScore {l xs ys : List α} (h : l ∈ infixes ys) :
    nwScore σ gap xs l ≤ fittingScore σ gap xs ys

Uses 3

Statement usesFitting score · Infixes · Needleman–Wunsch score

TheoremUpper bounds on the fitting score#✓fully proved

Let \(\sigma\) be a substitution score, \(g\) a gap score, \(x\) and \(y\) sequences and \(b\) an integer. If the Needleman–Wunsch score of \(x\) against every infix of \(y\) (with \(\sigma\) and \(g\)) is at most \(b\), then the fitting score of \(x\) against \(y\) is at most \(b\).

theorem fittingScore_le {xs ys : List α} {y : ℤ}
    (h : ∀ l ∈ infixes ys, nwScore σ gap xs l ≤ y) :
    fittingScore σ gap xs ys ≤ y

Uses 3 · Used by 1

Statement usesFitting score · Infixes · Needleman–Wunsch score

Used byThe fitting score is at most the local score

TheoremThe fitting score is attained#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. For all sequences \(x\) and \(y\) there is an infix \(l\) of \(y\) such that the Needleman–Wunsch score of \(x\) against \(l\) (with \(\sigma\) and \(g\)) equals the fitting score of \(x\) against \(y\).

theorem exists_nwScore_eq_fittingScore (xs ys : List α) :
    ∃ l ∈ infixes ys, nwScore σ gap xs l = fittingScore σ gap xs ys

Uses 3

Statement usesFitting score · Infixes · Needleman–Wunsch score

TheoremThe overlap score is at most the local score#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. For all sequences \(x\) and \(y\), the overlap score of \(x\) and \(y\) is at most the local score of \(x\) and \(y\), both taken with \(\sigma\) and \(g\).

Every overlap pair is an infix pair.

theorem overlapScore_le_localScore (xs ys : List α) :
    overlapScore σ gap xs ys ≤ localScore σ gap xs ys

Uses 8

Statement usesLocal alignment score · Overlap alignment score

Proof usesInfix pairs · Needleman–Wunsch score · Infix pairs score at most the local score · Overlap pairs · Upper bounds for the overlap score · Pairs of prefixes

TheoremThe fitting score is at most the local score#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score. For all sequences \(x\) and \(y\), the fitting score of \(x\) against \(y\) is at most the local score of \(x\) and \(y\), both taken with \(\sigma\) and \(g\).

Every fitting candidate, all of \(x\) against an infix of \(y\), is an infix pair.

theorem fittingScore_le_localScore (xs ys : List α) :
    fittingScore σ gap xs ys ≤ localScore σ gap xs ys

Uses 8

Statement usesFitting score · Local alignment score

Proof usesUpper bounds on the fitting score · Infix pairs · Infixes · Needleman–Wunsch score · Infix pairs score at most the local score · Pairs of prefixes

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.