Proof complexity compares the strength of proof systems using the notion of simulation. A proof system "P" "p-simulates" a proof system "Q" if there is a polynomial-time function which given a "Q"-proof outputs a "P"-proof of the same tautology. If "P" p-simulates "Q" and "Q" p-simulates "P", the proof systems "P" and "Q" are "p-equivalent". There is also a weaker notion of simulation: a proof system "P" "simulates" a proof system "Q" if there is a polynomial "p" such that for every "Q"-proof "x" of a tautology "A", there is a "P"-proof "y" of "A" such that the length of "y", |"y"| is at most "p"(|"x"|).