PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lang rel symm 1
1. A: Type
2. L: LangOver(A)

Sym x,y:A*. x L-induced Equiv y
By:
Unfolds [`sym`;`lang_rel`] 0
THEN
Reduce 0
Generated subgoal:

1 a,b:A*. (z:A*. L(z @ a) L(z @ b)) (z:A*. L(z @ b) L(z @ a))

About:
listuniverseallimpliesapply