circuits[T: TYPE]: THEORY BEGIN IMPORTING walks[T] G: VAR digraph[T] reducible?(G: digraph[T], w: Seq(G)): bool = (EXISTS (k: posnat): k < l(w) - 1 AND w(k-1) = w(k+1)) reduced?(G: digraph[T], w: Seq(G)): bool = NOT reducible?(G,w) % % cyclically_reduced?(G: digraph[T], w: Long_walk(G)): bool = % reduced?(G,w) AND % (FORALL (j: below(l(w)-1)): reduced?(G,w^(j+1, l(w)-1) o w^(1,j))) cyclically_reduced?(G: digraph[T], w: Seq(G)): bool = l(w) > 2 AND reduced?(G,w) AND w(1) /= w(l(w)-2) circuit?(G: digraph[T], w: Seq(G)): bool = walk?(G,w) AND cyclically_reduced?(G,w) AND pre_circuit?(G,w) END circuits