PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
incl
aux4
quo
1
1
1
2
1
1.
n:
{1...}
2.
E:
n
n
Prop
3.
EquivRel i,j:
n. i E j
4.
x1:
n
5.
x2:
n
6.
x1 E x2
7.
x1 = n-1
i,j:
n//(i E j)
8.
EquivRel x,y:
(n-1). x E y
x2 = n-1
n
By:
Analyze 0
THEN
HypSubst -1 6
THEN
Analyze 7
Generated subgoal:
1
6.
x1 E (n-1)
7.
EquivRel x,y:
(n-1). x E y
8.
x2 = n-1
n
x1 = n-1
i,j:
n//(i E j)
About:
(n-1). x E y
x1 = n-1 
x1 = n-1 
