Lines Matching refs:depth
565 of the minimum depth at which x occurs in a tree, and the minimum
566 index within the list of a tree containing x to that depth.
571 the depth number doesn't change, but the index goes down because
578 moves to the end of the list, but at a reduced depth.
586 (* depth x t n means that x occurs in tree t at depth n *)
588 (!x t1 t2. depth x (Nd x t1 t2) 0) /\
589 (!m x a t1 t2. depth x t1 m ==> depth x (Nd a t1 t2) (SUC m)) /\
590 (!m x a t1 t2. depth x t2 m ==> depth x (Nd a t1 t2) (SUC m))
595 ``!x t. mem x t ==> ?n. depth x t n``,
601 ``!x t n. depth x t n ==> mem x t``,
604 (* mindepth x t returns SOME n if x occurs in t at minimum depth n,
607 mindepth x t = if mem x t then SOME (LEAST n. depth x t n) else NONE
672 `!n. ~depth x t2 n` by METIS_TAC [depth_mem] THEN
683 `!n. ~depth x t1 n` by METIS_TAC [depth_mem] THEN
697 ``(mindepth x t = SOME n) ==> depth x t n``,
1031 ["optmin", "depth", "mindepth", "is_mmindex"]