yellowsquid/cfe-proof.git/src/Cfe/Expression, branch master [no description] http://git.yellowsquid.uk/yellowsquid/cfe-proof.git/atom?h=master 2021-04-29T19:58:04Z Finally prove that e [ μ e / zero ] ≈ μ e. 2021-04-29T19:58:04Z Chloe Brown chloe.brown.00@outlook.com 2021-04-29T19:58:04Z urn:sha1:8abb1b5601fabf5e7560d08faa6e633e60663e0a Complete proof of generator. Cleanup Derivation. 2021-04-24T14:30:30Z Chloe Brown chloe.brown.00@outlook.com 2021-04-24T14:30:30Z urn:sha1:0708355c7988345c98961cad087dc56eeb16ea7f Cleanup Type properties. 2021-04-12T16:32:02Z Chloe Brown chloe.brown.00@outlook.com 2021-04-12T16:32:02Z urn:sha1:f84e919e12c92c241d3d38203400c2bb14fb0017 Add lexicographic expression ordering. 2021-04-06T14:12:09Z Chloe Brown chloe.brown.00@outlook.com 2021-04-06T14:08:08Z urn:sha1:e890218fab378f8e427d2d3c046875128a23d50b Clean up the Expression hierarchy. 2021-04-05T19:18:53Z Chloe Brown chloe.brown.00@outlook.com 2021-04-05T19:18:53Z urn:sha1:49a2df1e3a210cd8be69afb33f8a3b5e20e41129 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