### 4.4.1. Functional dependency invariants involving two constraints

Proposition 167 Given the constraints

$\mathrm{𝙽𝚅𝙰𝙻}=1⇒\mathrm{𝙽𝙸𝙽𝙵}=0$

Proof 165 Since a single value leads to a plateau.

Proposition 168 Given the constraints

$2·𝙿\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-\mathrm{𝙻𝙴𝙽}$

Proof 166 Beside a first sequence with a small value, we alternate between large and small values in order to maximise the number of peaks.

Proposition 169 Given the constraints

$2·𝚅\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-\mathrm{𝙻𝙴𝙽}$

Proof 167 Beside a first sequence with a large value, we alternate between small and large values in order to maximise the number of valleys.

Proposition 170 Given the constraints

$2·𝙿\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-\mathrm{𝙻𝙴𝙽}$

Proof 168 Beside a last sequence with a small value, we alternate between large and small values in order to maximise the number of peaks.

Proposition 171 Given the constraints

$2·𝚅\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-\mathrm{𝙻𝙴𝙽}$

Proof 169 Beside a last sequence with a large value, we alternate between small and large values in order to maximise the number of valleys.

Proposition 172 Given the constraints

$𝙻\ge \mathrm{𝙼𝙰𝚇}$

Proof 170

Proposition 173 Given the constraints

$𝙻\ge \mathrm{𝙼𝙰𝚇}$

Proof 171

Proposition 174 Given the constraints

$\mathrm{𝙼𝙰𝚇}\ge \mathrm{𝙼𝙸𝙽}$

Proof 172

Proposition 175 Given the constraints

$\mathrm{𝙼𝙰𝚇}\ge \mathrm{𝙼𝙸𝙽}$

Proof 173

Proposition 176 Given the constraints

$\mathrm{𝙼𝙰𝚇}\ge \mathrm{𝙼𝙸𝙽}$

Proposition 177 Given the constraints

$\mathrm{𝚂𝚄𝙼}\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|·\mathrm{𝙼𝙰𝚇}$

Proposition 178 Given the constraints

$\mathrm{𝚂𝚄𝙼}\ge |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|·\mathrm{𝙼𝙸𝙽}$

Proposition 179 Given the constraints

$𝙿·\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|$

Proof 177 Cumulated minimum width of the different peaks cannot exceed size of sequence.

Proposition 180 Given the constraints

The automaton depicted by Figure 4.4.1 provides a necessary condition.

##### Figure 4.4.1. Automaton for a redundant constraint between the $\mathrm{𝚙𝚎𝚊𝚔}$$\left(𝙿,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)$ and the $\mathrm{𝚖𝚒𝚗}_\mathrm{𝚠𝚒𝚍𝚝𝚑}_\mathrm{𝚙𝚎𝚊𝚔}$$\left(\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷},\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)$ constraints when $\underline{𝙿}>0$ and $\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}>0$, where $\mathrm{𝑐𝑜𝑛𝑑}$ is the condition $|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-i>max\left(0,max\left(\underline{𝙿}-max\left(S-1,0\right),0\right)-1\right)·\left(\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}+1\right)+\left(max\left(\underline{𝙿}-max\left(S-1,0\right),0\right)\ge 1\right)·\left(\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}-max\left(i-F,0\right)\right)$, and where $i$, $S$ and $F$ respectively stand for the index of the current pairs ($i\in \left[1,|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-1\right]$), the number of start of potential peaks already encountered, the position of the start of the last potential peak encountered; the quantity $max\left(S-1,0\right)$ denotes the number of peaks already encountered, while the quantity $max\left(\underline{𝙿}-max\left(S-1,0\right),0\right)$ denotes the minimum number of peaks that remain to done from position $i$. Proof 178 The condition associated with each transition of the automaton checks that there is enough space between the current position and the end of the sequence to place the remaining minimum number of required peaks.

Proposition 181 Given the constraints

$𝚅·\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}\le |\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|$

Proof 179 Cumulated minimum width of the different valleys cannot exceed size of sequence.

Proposition 182 Given the constraints

The automaton depicted by Figure 4.4.2 provides a necessary condition.

##### Figure 4.4.2. Automaton for a redundant constraint between the $\mathrm{𝚟𝚊𝚕𝚕𝚎𝚢}$$\left(𝚅,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)$ and the $\mathrm{𝚖𝚒𝚗}_\mathrm{𝚠𝚒𝚍𝚝𝚑}_\mathrm{𝚟𝚊𝚕𝚕𝚎𝚢}$$\left(\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷},\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)$ constraints when $\underline{𝚅}>0$ and $\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}>0$, where $\mathrm{𝑐𝑜𝑛𝑑}$ is the condition $|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-i>max\left(0,max\left(\underline{𝚅}-max\left(S-1,0\right),0\right)-1\right)·\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}+\left(max\left(\underline{𝚅}-max\left(S-1,0\right),0\right)\ge 1\right)·\left(\underline{\mathrm{𝙼𝙸𝙽}_\mathrm{𝚆𝙸𝙳𝚃𝙷}}-max\left(i-F,0\right)\right)$, and where $i$, $S$ and $F$ respectively stand for the index of the current pairs ($i\in \left[1,|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}|-1\right]$), the number of start of potential valleys already encountered, the position of the start of the last potential valley encountered; the quantity $max\left(S-1,0\right)$ denotes the number of valleys already encountered, while the quantity $max\left(\underline{𝚅}-max\left(S-1,0\right),0\right)$ denotes the minimum number of valleys that remain to done from position $i$. Proof 180 The condition associated with each transition of the automaton checks that there is enough space between the current position and the end of the sequence to place the remaining minimum number of required valleys.

Proposition 183 Given the constraints

$\mathrm{𝙽𝚅𝙰𝙻}\ge 𝙽$

Proof 181 Since stairs visible from the end are located at different altitudes.

Proposition 184 Given the constraints

$\mathrm{𝙽𝚅𝙰𝙻}\ge 𝙽$

Proof 182 Since stairs visible from the start are located at different altitudes.

Proposition 185 Given the constraints

$|𝙿-𝚅|\le 1$

Proof 183 Since peaks and valleys can only alternate.

Proposition 186 Given the constraints

with $𝙿>𝚅$, the automaton depicted by Figure 4.4.3 provides a necessary condition.

##### Figure 4.4.3. Automaton for a redundant constraint for the conjunction $\mathrm{𝚙𝚎𝚊𝚔}$$\left(𝙿,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)\wedge$ $\mathrm{𝚟𝚊𝚕𝚕𝚎𝚢}$$\left(𝚅,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)\wedge 𝙿>𝚅$ (we have both to start with a peak and to finish with a peak) Proof 184 Since peaks and valleys can only alternate and since having more peaks than valleys enforces to start and end on a peak.

Proposition 187 Given the constraints

with $𝚅>𝙿$ the automaton depicted by Figure 4.4.4 provides a necessary condition.

##### Figure 4.4.4. Automaton for a redundant constraint for the conjunction $\mathrm{𝚟𝚊𝚕𝚕𝚎𝚢}$$\left(𝚅,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)\wedge$ $\mathrm{𝚙𝚎𝚊𝚔}$$\left(𝙿,\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right)\wedge 𝚅>𝙿$ (we have both to start with a valley and to finish with a valley) Proof 185 Since valleys and peaks can only alternate and since having more valleys than peaks enforces to start and end on a valley.