theorem
Cedar.Thm.reachable_of_le
{entities : Spec.Entities}
{start : Data.Set Spec.EntityUID}
{uid : Spec.EntityUID}
{n m : Nat}
(hr : ReachableIn entities start uid n)
(hle : n ≤ m)
:
ReachableIn entities start uid m
Weakening: if uid is reachable at level n, it's reachable at any level m ≥ n.
theorem
Cedar.Thm.reachable_child
{entities : Spec.Entities}
{start : Data.Set Spec.EntityUID}
{uid uid2 : Spec.EntityUID}
{ed : Spec.EntityData}
{n : Nat}
(hr : ReachableIn entities start uid (n + 1))
(hf : Data.Map.find? entities uid = some ed)
(hm : uid2 ∈ ed.sliceEUIDs)
:
ReachableIn entities start uid2 (n + 2)
If uid is reachable at level n+1, entities.find? uid = some ed, and
uid2 ∈ ed.sliceEUIDs, then uid2 is reachable at level n+2.