Function vstd::seq_lib::lemma_seq_skip_of_skip

source ·

pub proof fn lemma_seq_skip_of_skip<A>(s: Seq<A>, m: int, n: int)

Expand description

ensures

(0 <= m && 0 <= n && m + n <= s.len()) ==> s.skip(m).skip(n) =~= s.skip(m + n),

If m + n is less than or equal to the length of sequence s, then skipping the first m elements and then skipping the first n elements of the resulting sequence is equivalent to just skipping the first m + n elements.