Function lemma_path_between_properties

Source

pub broadcast proof fn lemma_path_between_properties<T: TreeNodeValue<L>, const N: usize, const L: usize>(
    src: TreeNode<T, N, L>,
    dst: TreeNode<T, N, L>,
)

Expand description

requires

src.inv(),

dst.inv(),

src.level() <= dst.level(),

#[trigger] src.on_subtree(dst),

ensures

path_between(src, dst).inv(),

path_between(src, dst).len() == dst.level() - src.level(),

dst.level() == src.level() ==> path_between(src, dst).is_empty() && src == dst,

dst.level() > src.level() ==> src.recursive_visit(path_between(src, dst)).last() == dst,

lemma_path_between_properties

Function lemma_path_between_properties Copy item path

Function lemma_path_between_properties