PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
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
8.
z1
0
z1
m
0
z1
m+z2
By:
Inst
Thm*
i1,i2,j1,j2:
. i1
j1
i2
j2
i1+i2
j1+j2 [z1
0;0;z1
m;z2]
Generated subgoal:
1
9.
z1
0+0
z1
m+z2
0
z1
m+z2
About:
0+0
z1m+z2
0z1m+z2
z1 < n z2 < m0z1m 0z1m+z2
i1,i2,j1,j2:. i1j1 
i2j2 i1+i2j1+j2
[z10;0;z1m;z2]0+0z1m+z2 0z1m+z2
