Function vstd::seq_lib::lemma_seq_append_take_skip

source ·

pub proof fn lemma_seq_append_take_skip<A>(a: Seq<A>, b: Seq<A>, n: int)

Expand description

ensures

n == a.len() ==> ((a + b).take(n) =~= a && (a + b).skip(n) =~= b),

If n is the length of sequence a, then taking the first n elements of the concatenation a + b is equivalent to the sequence a and skipping the first n elements of the concatenation a + b is equivalent to the sequence b.