Function path_between_properties

Source

pub broadcast proof fn path_between_properties<T: TreeNodeValue<L>, const N: usize, const L: usize>(
    src: Node<T, N, L>,
    dst: Node<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,

path_between_properties

Function path_between_properties Copy item path

Function path_between_properties