PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
series
step
1
1.
q:
2.
n:
(q
n+1
) =
(q
n
)+(q
n)
By:
RW (AddrC [2] (RecUnfoldC `geom_series`)) 0
THEN
SplitOnConclITE
Generated subgoals:
1
3.
n+1 = 0
0 =
(q
n
)+(q
n)
2
3.
n+1 = 0
(q
n+1-1
)+(q
n+1-1) =
(q
n
)+(q
n)
About:
0 = 
(q
n
)+(qn) 
n+1 = 0 (qn+1-1)+(qn+1-1) = (qn)+(qn) (qn+1) = (qn)+(qn) 0 = (qn)+(qn) n+1 = 0 (qn+1-1)+(qn+1-1) = (qn)+(qn) 
