Auto:Automata(Alph;St), x,y,z:Alph*.
(Result(Auto)x) = (Result(Auto)y) 
(Result(Auto)z @ x) = (Result(Auto)z @ y)
compute_l_inv
bs ; a.as' a.(as' @ bs) (recursive)
Thm* Auto:Automata(Alph;St), x,y,z:Alph*.
(Result(Auto)x) = (Result(Auto)y)
(Result(Auto)z @ x) = (Result(Auto)z @ y)
compute_l_inv
In prior sections: list 1 list 3 autom action sets