4.4.1. Functional dependency invariants involving two constraints

Proposition 167 Given the constraints

π™½πš…π™°π™»=1⇒𝙽𝙸𝙽𝙡=0

Proof 165 Since a single value leads to a plateau.

Proposition 168 Given the constraints

2·𝙿≀|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-𝙻𝙴𝙽

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Β·πš…β‰€|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-𝙻𝙴𝙽

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·𝙿≀|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-𝙻𝙴𝙽

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Β·πš…β‰€|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-𝙻𝙴𝙽

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

𝙻β‰₯π™Όπ™°πš‡

Proposition 173 Given the constraints

𝙻β‰₯π™Όπ™°πš‡

Proposition 174 Given the constraints

π™Όπ™°πš‡β‰₯𝙼𝙸𝙽

Proposition 175 Given the constraints

π™Όπ™°πš‡β‰₯𝙼𝙸𝙽

Proposition 176 Given the constraints

π™Όπ™°πš‡β‰₯𝙼𝙸𝙽

Proposition 177 Given the constraints

πš‚πš„π™Όβ‰€|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|Β·π™Όπ™°πš‡

Proposition 178 Given the constraints

πš‚πš„π™Όβ‰₯|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|·𝙼𝙸𝙽

Proposition 179 Given the constraints

𝙿·𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™·β‰€|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|

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 πš™πšŽπšŠπš”(𝙿,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) and the πš–πš’πš—_πš πš’πšπšπš‘_πš™πšŽπšŠπš”(𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™·,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) constraints when 𝙿 Μ²>0 and 𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²>0, where π‘π‘œπ‘›π‘‘ is the condition |πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-i>max(0,max(𝙿 Μ²-max(S-1,0),0)-1)Β·(𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²+1)+(max(𝙿 Μ²-max(S-1,0),0)β‰₯1)Β·(𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²-max(i-F,0)), and where i, S and F respectively stand for the index of the current pairs (i∈[1,|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-1]), the number of start of potential peaks already encountered, the position of the start of the last potential peak encountered; the quantity max(S-1,0) denotes the number of peaks already encountered, while the quantity max(𝙿 Μ²-max(S-1,0),0) denotes the minimum number of peaks that remain to done from position i.
ctrs/preface-228-tikz

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

πš…Β·π™Όπ™Έπ™½_πš†π™Έπ™³πšƒπ™·β‰€|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|

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 πšŸπšŠπš•πš•πšŽπš’(πš…,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) and the πš–πš’πš—_πš πš’πšπšπš‘_πšŸπšŠπš•πš•πšŽπš’(𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™·,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) constraints when πš… Μ²>0 and 𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²>0, where π‘π‘œπ‘›π‘‘ is the condition |πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-i>max(0,max(πš… Μ²-max(S-1,0),0)-1)·𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²+(max(πš… Μ²-max(S-1,0),0)β‰₯1)Β·(𝙼𝙸𝙽_πš†π™Έπ™³πšƒπ™· Μ²-max(i-F,0)), and where i, S and F respectively stand for the index of the current pairs (i∈[1,|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|-1]), the number of start of potential valleys already encountered, the position of the start of the last potential valley encountered; the quantity max(S-1,0) denotes the number of valleys already encountered, while the quantity max(πš… Μ²-max(S-1,0),0) denotes the minimum number of valleys that remain to done from position i.
ctrs/preface-229-tikz

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

π™½πš…π™°π™»β‰₯𝙽

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

Proposition 184 Given the constraints

π™½πš…π™°π™»β‰₯𝙽

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

Proposition 185 Given the constraints

|𝙿-πš…|≀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 πš™πšŽπšŠπš”(𝙿,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) ∧ πšŸπšŠπš•πš•πšŽπš’(πš…,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) ∧ 𝙿>πš… (we have both to start with a peak and to finish with a peak)
ctrs/preface-230-tikz

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 πšŸπšŠπš•πš•πšŽπš’(πš…,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) ∧ πš™πšŽπšŠπš”(𝙿,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) ∧ πš…>𝙿 (we have both to start with a valley and to finish with a valley)
ctrs/preface-231-tikz

Proof 185 Since valleys and peaks can only alternate and since having more valleys than peaks enforces to start and end on a valley.