Function concat_replicate_up_to

pub fn concat_replicate_up_to<T>(n: Int, m: Int, s: FSet<T>)

An equation relating s.replicate_up_to(m) and s.replicate_up_to(n).

logic

pearlite! {
    if n + 1 == m {
        concat_empty(s.replicate(n + 1));
    } else {
        concat_union::<T>();
        concat_replicate(n, m - n - 1, s);
        concat_replicate_up_to(n, m - 1, s);
    }
}

requires

0 <= n && n < m

ensures

s.replicate_up_to(m) == s.replicate_up_to(n).union(
    FSet::concat(s.replicate(n + 1), s.replicate_up_to(m - n - 1)))