+++
title = "Main difficulty in destruction proof"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g2b"]
forwardlinks = ["3a8g2d", "3a8g2c1"]
zettelid = "3a8g2c"
+++

The main difficulty is relating dynamic evaluation behaviours of
predicates to the static properties of the predicates. And without a SAT
solver. In the proof, one needs to show that given a predicate $P$ which
evaluates to true, and a predicates $P'$ which simplifies to true along
a single path, that these are actually the same predicate, and therefore
must refer to the same register.