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