PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
equiv
rel
fun
1
1
1
1
1.
T:
Type
2.
E:
T
T
3.
s:
T
4.
t:
T
5.
Refl(T;x,y.x E y)
6.
a,b:T. (a E b)
(b E a)
7.
a,b,c:T. (a E b)
(b E c)
(a E c)
8.
s E t
9.
x:
T
E(s,x)
E(t,x)
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:
1
10.
E(s,x)
E(t,x)
2
10.
E(t,x)
E(s,x)
About:
E(t,x)
T
a,b:T. (a E b) 
(b E a)
