At: quo list accept Alph,St:Type, Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y). Auto(l) By: Analyze 0
THEN
Analyze 0
THEN
Analyze 0
THEN
Inst
Thm*L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y
[Alph;LangOf(Auto)] Generated subgoal: