:: deftheorem defines IndexPoly NUMPOLY1:def 6 :
for s being Nat
for x being b₁ -gonal number holds IndexPoly (s,x) = (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4);