Function vstd::seq_lib::lemma_seq_skip_index2

source ·

pub proof fn lemma_seq_skip_index2<A>(s: Seq<A>, n: int, k: int)

Expand description

ensures

0 <= n <= k < s.len() ==> (s.skip(n))[k - n] == s[k],

If k is a valid index between n (inclusive) and the length of sequence s (exclusive), then the k-nth element of the sequence s.skip(n) is the same as the kth element of the original sequence s.