A two-line algorithm for proving terminating hypergeometric identities (Q1917998)

Given a terminating hypergeometric identity of the form \[ \sum^\infty_{k=-\infty} F(n,k)=f(n),\quad n\geq n_0,\tag{\(*\)} \] \(F(n,k)\) and \(f(n)\) being hypergeometric terms w.r.t. \(n\) and \(k\), then it is known that \((*)\) is valid iff it is valid for finitely many initial values \(n=n_0\), \(n_0+1,\dots,n_1\). The question remains to find a reasonable value for \(n_1\). In this paper, a bound \(n_1\) only depending on the given \(F\), \(f\) and \(n_0\) is given. This is theoretically very interesting. The given bound is too large to be of practical value, though.