Propositional Representation of Arithmetic Proofs (Preliminary Version)
Equations f@@@@ &equil; g@@@@ between polynomial time computable functions can be represented by sets of propositional formulas. If f@@@@ &equil; g@@@@ is provable in certain arithmetic systems, then polynomial length proofs of the representing formulas exist in certain propositional systems. Two cases of this phenomenon and a general theory are given.