PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
series
wf
q,n:
.
(q
n
)
By:
UnivCD
THEN
NatInd 2
THEN
RecCaseSplit `geom_series`
Generated subgoals:
1
1.
q:
2.
0 = 0
0
2
1.
q:
2.
0 = 0
(q
-1
)+(q
-1)
3
1.
q:
2.
n:
3.
0 < n
4.
(q
n-1
)
5.
n = 0
0
4
1.
q:
2.
n:
3.
0 < n
4.
(q
n-1
)
5.
n = 0
(q
n-1
)+(q
n-1)
About: