yellowsquid/cfe-proof.git/src/Cfe/Expression, branch thm4.5a [no description] http://git.yellowsquid.uk/yellowsquid/cfe-proof.git/atom?h=thm4.5a 2021-03-30T17:52:46Z Attempt to prove unrolling. 2021-03-30T17:52:46Z Chloe Brown chloe.brown.00@outlook.com 2021-03-30T17:52:46Z urn:sha1:050206a1ba06d588879171698f2f8120a8b550d4 Introduce < for Languages. 2021-03-29T17:08:09Z Chloe Brown chloe.brown.00@outlook.com 2021-03-29T17:08:09Z urn:sha1:13e0839831a528d26478a3a94c7470204460cce4 Move around some definitions. Introduce non-terminating proof of derivation existence. 2021-03-27T20:32:03Z Chloe Brown chloe.brown.00@outlook.com 2021-03-27T20:32:03Z urn:sha1:adad5280af0d81a2f171df619e9c7169dcb43a02 Begin soundness proof. 2021-03-27T13:34:32Z Chloe Brown chloe.brown.00@outlook.com 2021-03-24T09:30:13Z urn:sha1:a95622ca33a31a8c6d3cb31c7ca3b390e7aa5624 Change judgement to use variable contexts. 2021-03-20T18:18:31Z Chloe Brown chloe.brown.00@outlook.com 2021-03-20T18:18:31Z urn:sha1:16afd9dff6798509a1d654b0f06e409353e01180 Add some useful context transformations. Change Language definition to respects instead of custom congruence. 2021-03-16T18:45:27Z Chloe Brown chloe.brown.00@outlook.com 2021-03-16T18:45:27Z urn:sha1:02a0f87be944b1d43fda265058b891f419d25b65 Add weakening proofs for type judgements. 2021-03-13T20:06:22Z Chloe Brown chloe.brown.00@outlook.com 2021-03-13T20:06:22Z urn:sha1:0dc59b43f78654a746ef5baaeabcc767c64ee0df Remove incomplete unrolling proof. 2021-03-05T16:16:42Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T16:16:42Z urn:sha1:a2bca9eb599e8109ba91e257ee223b39f64703c1 Separate out some Language properties. 2021-03-05T00:10:08Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T00:10:08Z urn:sha1:9c5540562f53be81bfb03ef2b96d7f59b3ddea44 Complete proofs up to Proposition 3.2 (excluding unrolling) 2021-03-05T00:04:46Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T00:00:04Z urn:sha1:5302e4a27a64cb2a97120517df4b6998da7b3168