count_alt.key

\functions {
    Seq s1;
    int maxx;
}

\problem {
    \forall int i; (
        (0 <= i & i < seqLen(s1))
        -> (0 <= int::seqGet(s1, i) & int::seqGet(s1, i) < maxx))
    & \forall int i; (\forall int j; (
        (0 <= i & i < seqLen(s1) & 0 <= j & j < seqLen(s1) & i != j)
        -> (int::seqGet(s1, i) != int::seqGet(s1, j))))
    & maxx >= 0
    -> 
    seqLen(s1) <= maxx
}

// prove by int_induction:
// \forall Seq s; ((
//  \forall int i; (0 <= i & i < s.length -> 0 <= (int)s[i] & (int)s[i] < nv) &
//  \forall int i;
//   \forall int j;
//     (0 <= i & i < s.length & 0 <= j & j < s.length & !i = j -> !(int)s[i] = (int)s[j])) -> s.length <= nv)
// base case / use case are trivial.
// step case: cut on \exists int i; (0 <= i & i < s_0.length & (int)(s_0[i]) = nv_0)
// then use induction quantifier on:
// seqConcat(seqSub(s_0, 0, i_0), seqSub(s_0, i_0 + 1, s_0.length))