3 ms·
How can I prove dfs graph termination in Agda? I tried passing "visited" subset but nothing
by evolveyourmind 7y ago
How can I prove dfs graph termination in Agda? I tried passing "visited" subset but nothing
- Kutta 7y agoYou need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work for some reason.
- evolveyourmind 7y agoThe decreasing number worked, ty. Writing proofs with this will be impossible tho :D