PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
equiv
rel
fun
1
1
1.
T:
Type
2.
E:
T
T
3.
s:
T
4.
t:
T
5.
EquivRel x,y:T. x E y
6.
s E t
7.
x:
T
E(s,x)
E(t,x)
By:
Analyze 5
THEN
Analyze 6
Generated subgoal:
1
5.
Refl(T;x,y.x E y)
6.
Sym x,y:T. x E y
7.
Trans x,y:T. x E y
8.
s E t
9.
x:
T
E(s,x)
E(t,x)
About:
E(s,x) 
E(t,x)
T
E(s,x) E(t,x) E(s,x) E(t,x)
