18def ballP {α : Type} (K : Kinematics α) (x : α) : Nat → α → Prop 19| 0, y => y = x 20| Nat.succ n, y => ballP K x n y ∨ ∃ z, ballP K x n z ∧ K.step z y 21 22namespace ConeBound 23 24variable {α : Type} {d : Nat} 25variable [DecidableEq α] 26variable [B : BoundedStep α d] 27
used by (11)
From the project-wide theorem graph. These declarations reference this one in their body.