-- AUTO1

constructs: D dot plus minus E
defuncts:   states labels atoms

axioms:

  states == [1]
& labels == [D,dot,plus,minus,E]
& atoms  == [final]

& (1,D) -> 2
& (2,D) -> 3 & (2,dot) -> 4
& (3,D) -> 5 & (3,dot) -> 4
& (4,D) -> 6 & (4,E) -> 7
& (5,D) -> 5 & (5,dot) -> 4
& (6,D) -> 6 & (6,E) -> 7
& (7,D) -> 9 & (7,plus) -> 8 & (7,minus) -> 8 & (7,dot) -> 10 & (7,E) -> 10
& (8,D) -> 9
& (9,D) -> 9
& (10,y) -> 10
& (x `in` [1,8,9] & y `in` labels-[D] |
   x `in` [2,3,5] & y `in` labels-[D,dot] |
   x `in` [4,6] & y `in` labels-[D,E] ==> (x,y) -> 10)

& final -> branch[2,3,4,5,6,9]

-- equivalences: 2~3~5 4~6