Function lemma_count_present_upto_unchanged

pub proof fn lemma_count_present_upto_unchanged<E: PageTableEntryTrait>(
    s: Seq<E>,
    s2: Seq<E>,
    n: int,
    idx: int,
)

Expand description

requires

0 <= n <= idx,

forall |k: int| 0 <= k < n ==> s[k] == s2[k],

ensures

count_present_upto(s2, n) == count_present_upto(s, n),

If two sequences agree on [0, n), their counts up to n are equal.

lemma_count_present_upto_unchanged