PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
1
1
1
1
1
1
1.
n:
2.
m:
3.
0 < m
4.
z1:
5.
0
z1 < n
6.
z2:
7.
0
z2 < m
0
z1
m+z2
By:
Inst
Thm*
a,b:
, n:
. a
b
n
a
n
b [0;m;z1]
Generated subgoal:
1
8.
z1
0
z1
m
0
z1
m+z2
About:
0
z1m
0z1m+z2
z1 < n z2 < m 0z1m+z2
a,b:, n:. ab 
nanb
[0;m;z1]0z1m 0z1m+z2
