PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
rest
equi
rel
1
1
2
2
1.
n:
{1...}
2.
m:
n
3.
E:
n
n
Prop
4.
Refl(
n;x,y.x E y)
5.
Sym x,y:
n. x E y
6.
Trans x,y:
n. x E y
Trans x,y:
m. x E y
By:
BackThru
Thm*
n:{1...}, m:
n, E:(
n
n
Prop). Trans x,y:
n. x E y
Trans x,y:
m. x E y
Generated subgoals:
None
About:
nn
nPropn;x,y.x E y)n. x E yn. x E y
Trans x,y:m. x E y
n:{1...}, m:n, E:(nnProp).
Trans x,y:n. x E y 
Trans x,y:m. x E y