PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
rest
symm
rel
1
1
1.
n:
{1...}
2.
m:
n
3.
E:
n
n
Prop
4.
Sym x,y:
n. x E y
5.
a:
m
b:
m. (a E b)
(b E a)
By:
Unfold `sym` 4
THEN
Analyze 0
Generated subgoal:
1
4.
a,b:
n. (a E b)
(b E a)
5.
a:
m
6.
b:
m
(a E b)
(b E a)
About:
a,b:
n. (a E b) 
(b E a)mm
(a E b) (b E a)nn
nPropn. x E ym b:m. (a E b) (b E a)a,b:n. (a E b) (b E a)mm (a E b) (b E a)
