Hi, I want to prove some properties of some algorithms that walk directed graphs -- for the moment I'm mostly interested in DAGs, but at some point would like to handle arbitrary directed graphs. Does anyone have a handy theory or collection of theories that supports this? -- Scott