PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
ndecrease
1
1.
q:
2.
n:
3.
i:
(q
n
)
(q
n+i
)
By:
NatInd 3
Generated subgoals:
1
(q
n
)
(q
n+0
)
2
3.
i:
4.
0 < i
5.
(q
n
)
(q
n+i-1
)
(q
n
)
(q
n+i
)
About:
(q
n
)
(qn+0)
(qn)(qn+i-1) (qn)(qn+i)
(qn)(qn+i) (qn)(qn+0)(qn)(qn+i-1) (qn)(qn+i)
