Function lemma_inc_slot_indices 

pub proof fn lemma_inc_slot_indices<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
)

requires

1 <= level <= C::NR_LEVELS(),

pte_index_spec::<C>(va, level) + 1 < nr_subpage_per_huge::<C>(),

ensures

va + page_size::<C>(level) <= usize::MAX,

({
    let next = (va + page_size::<C>(level)) as Vaddr;
    &&& next % C::BASE_PAGE_SIZE() == va % C::BASE_PAGE_SIZE()
    &&& vaddr_upper_bits_spec::<C>(next) == vaddr_upper_bits_spec::<C>(va)
    &&& forall |i: int| {
        1 <= i <= C::NR_LEVELS()
            ==> #[trigger] pte_index_spec::<C>(next, i as PagingLevel)
                == pte_index_spec::<C>(va, i as PagingLevel)
                    + if i == level { 1int } else { 0int }
    }

}),

Advancing a nonterminal slot preserves every other index and cannot wrap the machine word.