PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
unique
1
1
1
1
1
1.
E:
2.
n:
3.
k:
4.
EquivRel x,y:
. x E y
5.
n E k
6.
E(n) = E(k)
E(k,n) = E(k,k)
By:
Analyze 4
THEN
Analyze 5
THEN
Unfold `sym` 5
Generated subgoal:
1
4.
Refl(
;x,y.x E y)
5.
a,b:
. (a E b)
(b E a)
6.
Trans x,y:
. x E y
7.
n E k
8.
E(n) = E(k)
E(k,n) = E(k,k)
About:
;x,y.x E y)
a,b:. (a E b) 
(b E a). x E y
E(k,n) = E(k,k)
. x E y E(k,n) = E(k,k);x,y.x E y)a,b:. (a E b) (b E a). x E y E(k,n) = E(k,k)
