PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
nxn
plus
1
ge
0
1
1
1.
n:
0
n
n+1
By:
Inst
Thm*
i1,i2,j1,j2:
. i1
j1
i2
j2
i1+i2
j1+j2 [0;0;n
n;1]
Generated subgoal:
1
0
n
n
About:
0
n
n
0nn+1
i1,i2,j1,j2:
. i1j1 
i2j2 i1+i2j1+j2
[0;0;nn;1] 0nn
