pith. machine review for the scientific record. sign in
inductive definition def or abbrev

ReachN

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

   9inductive ReachN {α} (K : Kinematics α) : Nat → α → α → Prop
  10| zero {x} : ReachN K 0 x x
  11| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z

used by (29)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.