<p><span class="h-card" translate="no"><a href="https://mastodon.social/@regehr" class="u-url mention">@<span>regehr</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@lenary" class="u-url mention">@<span>lenary</span></a></span> <span class="h-card" translate="no"><a href="https://hachyderm.io/@unlambda" class="u-url mention">@<span>unlambda</span></a></span> </p><p>ok so the problem I'm solving is: suppose you have inputs i, outputs o, states s and s', and combinational boolean functions f, f'</p><p>given relation s',o = f(s,i), rewrite f to smaller f'</p><p>so `forall s,i; f(s,i) == f'(s,i)` is easy but once you no longer require s/s' to match between the functions, just the observable behavior for evolution from the base case and identical `i`, it gets way harder</p>
