Domination tools for the repeated tailored programs

The running times of the repeated programs (issue #280) are bounded in the shape c (W + 1)^m X^{e (K + 1)} of MIPRE.Repeat.Dom, with W a bound on the parameters, X the size of the input plus one and K the input programs' degree. Their stages are polynomial-time functions and calls to the input programs, so two facts do most of the work: a polynomial of a dominated quantity is dominated (dom_poly), and a size linear in X raised to the power K is dominated once 10^K ≤ W (dom_powK).

theorem MIPRE.Repeat.Dom.ofLin {W X K : ℕ} (hX : 1 ≤ X) {a b c v : ℕ} (h : v ≤ a * W + b * X + c) : Dom W X K (a + b + c) 1 1 v

A linear combination of W and X.

theorem MIPRE.Repeat.dom_poly (P : Polynomial ℕ) (cy my ey : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {y : ℕ}, 1 ≤ X → Dom W X K cy my ey y → Dom W X K c m e (Polynomial.eval y P)

A polynomial of a dominated quantity is dominated.

theorem MIPRE.Repeat.dom_powK {W X K : ℕ} (hX : 1 ≤ X) (hW : 10 ^ K ≤ W) {a j y : ℕ} (ha : a ≤ 10 ^ j) (hy : y ≤ a * X) : Dom W X K 1 j 1 (y ^ K)

A size linear in X, to the power K, is dominated when 10^K ≤ W.

theorem MIPRE.Repeat.dom_mapCallCost (cm mm em cT mT eT cC mC eC cZ mZ eZ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {M T C Z : ℕ}, 1 ≤ X → Dom W X K cm mm em M → Dom W X K cT mT eT T → Dom W X K cC mC eC C → Dom W X K cZ mZ eZ Z → Dom W X K c m e (Tailored.Calls.mapCallCost M T C Z)

The cost of the loop of calls, dominated.