PrintForm Definitions exponent Sections AutomataTheory Doc

At: geom ndecrease 1 2

1. q:
2. n:
3. i:
4. 0 < i
5. (qn)(qn+i-1)

(qn)(qn+i)

By: RW (AddrC [2] (RecUnfoldC `geom_series`)) 0

Generated subgoal:

1 (qn)if n+i=0 0 else (qn+i-1)+(qn+i-1) fi


About:
addintless_thannatural_numbersubtractifthenelse