scheme :: GLIB_009:sch 2
IndDWalk{ F₁() -> _Graph, P₁[ Walk of F₁()] } :

for W being DWalk of F₁() holds P₁[W]

provided

A1: for W being trivial DWalk of F₁() holds P₁[W] and
A2: for W being DWalk of F₁()
for e being object st e in (W .last()) .edgesOut() & P₁[W] holds
P₁[W .addEdge e]