walk_inductions[T: TYPE]: THEORY BEGIN IMPORTING walks[T] P: VAR pred[prewalk] n: VAR nat w,ww: VAR prewalk walk_prep : LEMMA (FORALL w: P(w)) IFF (FORALL n, w : l(w) = n IMPLIES P(w)) digraph_induction_walk : THEOREM (FORALL w: (FORALL ww: l(ww) < l(w) IMPLIES P(ww)) IMPLIES P(w)) IMPLIES (FORALL w: P(w)) END walk_inductions