circuits[T: TYPE]: THEORY % % A circuit is a pre_circuit with no small loops (i.e. reduced) % % pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND % w(0) = w(length(w)-1) % % NOTE: The extra term "w(1) /= w(length(w)-2)" in the definition of % cyclically_reduced? handles the special case where % w(0) is a small loop % % removed "walk?(G,w)" from circuit? defn because it is in pre_circuit % BEGIN
IMPORTING walks[T]
G: VAR graph[T]
reducible?(G: graph[T], w: Seq(G)): bool =
(EXISTS (k: posnat): k < length(w) - 1 AND w(k-1) = w(k+1))
reduced?(G: graph[T], w: Seq(G)): bool = NOT reducible?(G,w)
% % cyclically_reduced?(G: graph[T], w: Long_walk(G)): bool = % reduced?(G,w) AND % (FORALL (j: below(length(w)-1)): reduced?(G,w^(j+1, length(w)-1) o w^(1,j)))
cyclically_reduced?(G: graph[T], w: Seq(G)): bool = length(w) > 2 AND
reduced?(G,w) AND w(1) /= w(length(w)-2)
circuit?(G: graph[T], w: Seq(G)): bool = %% walk?(G,w) AND
cyclically_reduced?(G,w) AND
pre_circuit?(G,w)
