Function vstd::seq_lib::lemma_seq_skip_update_commut2

source ·

pub proof fn lemma_seq_skip_update_commut2<A>(s: Seq<A>, i: int, v: A, n: int)

Expand description

ensures

0 <= i < n <= s.len() ==> s.update(i, v).skip(n) =~= s.skip(n),

If i is a valid index in the first n indices of sequence s, updating sequence s at index i with value v and then skipping the first n elements is equivalent to just skipping the first n elements without the update.