----------------------------- MODULE CostAlgebra -----------------------------
EXTENDS Integers, FiniteSets, Sequences

\* These pure operators keep signed intermediate values and floor only once.
SumMap(f) ==
    LET RECURSIVE Add(_)
        Add(S) == IF S = {} THEN 0
                  ELSE LET x == CHOOSE y \in S : TRUE
                       IN f[x] + Add(S \ {x})
    IN Add(DOMAIN f)

SeqSum(s) == SumMap([i \in 1..Len(s) |-> s[i]])
MaxOf(a, b) == IF a >= b THEN a ELSE b

ModifiedCost(base, increases, reductions) ==
    MaxOf(0, base + SeqSum(increases) - SeqSum(reductions))
=============================================================================