{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiaj7jx4x57beea2je2fqh4clpn4liwdl6x24ghp7yi3lmpwcs7l4q",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mo3vaoqnppa2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2606.13367v1",
  "publishedAt": "2026-06-12T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Jan Krajicek"
  ],
  "textContent": "**Authors:** Jan Krajicek\n\nInspired by a statement about Extended Frege proof systems by Jain and Jin (FOCS 2022) we prove that: - there is a p-time binary relation $\\approx$ between circuits that implies their logical equivalence, - the relation $\\approx$ implies that each of the two circuits can be rewritten into the other one by possibly deleting some gates and adding at most seven new gates, - if the equivalence $C \\equiv D$ has a size $s$ proof in an Extended Frege or a Circuit Frege proof system then there is a chain of circuits $E_i$ $$ C = E_0 \\approx \\dots \\approx E_t = D $$ with $t \\le s^{O(1)}$.",
  "title": "Extended Frege proofs, circuits and rewriting"
}