blob: 94955fbe4d9dee626aab45e687397e3055103769 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
+++
title = "Proving if-conversion correct"
date = "2022-06-08"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3h"]
forwardlinks = ["3c3j", "3c3i1"]
zettelid = "3c3i"
+++
The main problem is that one has two duplicate versions of the block. At
every point, one may be executing the copy, or the original body. The
only thing that I care about in the end is that the **behaviour** is the
same. The problem with that is that I need to be executing one or two
steps in the input to do this. However, this can still be proven using
just one step in the input by saving the intermediate proof state in
when I need to execute two sets.
|
