blob: 351ea9ec29fe873d329280ae9eba3c62a02f479a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
+++
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.
|
