入れ子のオートマトンはトレースで実現

もう1個、絵を見ればわかる知見。

外側のオートマトンの遷移辺や状態点が、小さなオートマトンになっている状況、まー「入れ子のオートマトン」みたいなことだが、それはトレースで表現できる。つまり、オートマトンの圏がトレース付きなら入れ子オートマトンも自由に作れる、ってこと。