PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
equiv
rel
fun
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.
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)
By:
Unfold `trans` 7
THEN
Unfold `sym` 6
Generated subgoal:
1
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)
About:
a,b:T. (a E b) 
(b E a)a,b,c:T. (a E b) (b E c) (a E c)
E(s,x) 
E(t,x)
T
E(s,x) E(t,x)a,b:T. (a E b) (b E a)a,b,c:T. (a E b) (b E c) (a E c) E(s,x) E(t,x)
