+++
title = "Proof carrying scheduling"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2e1c1"]
forwardlinks = []
zettelid = "2e1c1a"
+++

Another option to prove this theorem would be to have proof carrying
scheduling, which gives information to the checker about which
transformations took place, so that these can be reversed, if possible,
to get a syntactically equal representation.

However, the main problem with this, is that it is quite difficult to
even identify the different translations that were done to the
predicates, and it may not really help the proof.