хочу понять как пишутся алгоритмы для символьных вычислений, типа того что делает Maple или Mathematica

упрощение выражений, дифференцирование, и тому подобное

если кто подобным занимался, посоветуйте пожалуйста какой-нибудь опенсорсный код который можно почитать на эту тему

начал смотреть код cadabra2, но пока мне там ничего не понятно

Суть такова:

есть бинарник с закрытыми сорцами (игра), который требует кучу библиотек, вполне определенных версий.

бинарник 32-битный, и нужных ему библиотек ни в одном приличном 64-битном дистре нет.

нельзя ли, имея этот бинарник и собрав все нужные ему библиотеки (но не имея исходников), соорудить статически слинкованный бинарник которому никакие зависимости не требуются?

нужно вырезать из видео ролика паузы, то есть найти последовательности из идентичных кадров длиннее определенного порогового значения и сократить их до одинаковой длины. Видео снималось с экрана (скринкаст), поэтому кадры там будут полностью идентичны.

чем это можно (проще) сделать?

Собираю для личных нужд декомпилятор байткода для AVM2;
в принципе дело не хирое — почти все операции, которые оперируют только регистрами и стеком операндов можно свернуть
в некое подобие s-выражений с помощью нескольких простых преобразований (типа «((push X) (push Y) (add)) => ((push (add X Y)))»).

Остается последовательность операций с побочными эффектами (присваивание, вызовы функций с неиспользуемым результатом, итп),
а также условные и безусловные переходы. И от них надо бы как-то избавиться.
Можно было бы вместо каждого «(goto labelX)» подставить последовательность выражений которая идет за labelX,
но дальше надо как-то отслеживать рекурсию и заворачивать в
циклы, и как это правильно делать не совсем понятно. Подозреваю,
что об этом должна быть какая-то относительно красивая теория.
Подскажите где искать