PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
ndecrease
1
2
1
2
1
1
1.
q:
2.
n:
3.
i:
4.
0 < i
5.
(q
n
)
(q
n+i-1
)
6.
n+i = 0
7.
n+i-1 = n+i-1
(q
n
)
(q
n+i-1
)+(q
n+i-1)
By:
Inst
Thm*
n,k:
. (n
k)
[q;n+i-1]
Generated subgoals:
None
About:
(q
n
)
(qn+i-1)
n+i = 0
(qn)(qn+i-1)+(qn+i-1)
n,k:. (nk)
[q;n+i-1]
