PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

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

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

About:
listuniverseallimpliesapply