mb automata 3 Sections GenAutomata Doc

TheoremName
Thm* r:rel(), e,a,s,ds,da,de,rho,tr:Top. [[r]] rho ds da de e s a tr ~ [[rel_unprime(r)]] rho ds da de e s a tr[rel_mng_unprime]
cites
Thm* t:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr[term_mng_unprime]

mb automata 3 Sections GenAutomata Doc