Any theories about massively large numbers and Collatz conjecture? Would Collatz conjecture reduce Graham's number to 1? Would these proofs get presented before a generic one?
Here is the non-branching form:
0. Start with an odd number n
1. Apply n = 3n + 1
2. Count trailing zeroes of n
3. Right shift n by the trailing zero count
4. Return to (1), stopping at n = 1
If you're trying to feed a SAT solver, you can bound the size of the numbers at some level, and then pass one of the closed-form formulas into the solver.
Naively, it seems like any starting value (except those for which you already know the full sequence) might lead to values that exceed any arbitrary bound.
There's nothing inherently special about the branchiness of "remove trailing zeros" as an operation if you drill down into it: addition, for example, also needs conditional execution (based on the carry in to each section of a number).
Otherwise, if you're searching for a counterexample, bound n by some ridiculous number of bits (whatever your supercomputer supports) and run your solver with a simple closed form.
f = lambda n: (n & 1) * n + ((n + 1) >> 1)
Of course, the multiplication sort-of acts as a branch.
I mean, lambda calculus doesn't have any build-in branching, but you can style write arbitrary programs in it. Same for 'post correspondence problem' or SKI calculus.
All of these can be defined as "branching" or "non-branching" however you want.
'Branching' and 'non-branching' make sense in the context of specific architectures and/or languages. Just not really in an abstract algorithmic sense.