yellowsquid/cfe-proof.git/src/Cfe/Type, branch lemma3.5 [no description] http://git.yellowsquid.uk/yellowsquid/cfe-proof.git/atom?h=lemma3.5 2021-03-27T13:10:40Z Prove satisfaction for concatenation. 2021-03-27T13:10:40Z Chloe Brown chloe.brown.00@outlook.com 2021-03-27T13:10:40Z urn:sha1:a062b83551010213825e41a7acb0221a6c74e6af Prove sequential unique decomposition. 2021-03-25T18:01:19Z Chloe Brown chloe.brown.00@outlook.com 2021-03-25T18:01:19Z urn:sha1:ba7e3b5d9c868af4b5dd7c3af72c48a1dd27cc31 Fix faulty definition of flast set. Prove lemma 3.5 (7). 2021-03-24T17:01:29Z Chloe Brown chloe.brown.00@outlook.com 2021-03-24T17:01:29Z urn:sha1:abe9461e0dc194c160d97fee23a1646097a0c264 Prove lemma 3.5 (5). 2021-03-24T15:55:34Z Chloe Brown chloe.brown.00@outlook.com 2021-03-24T15:55:34Z urn:sha1:11dddff1955a696538afbc1cfb604bbc640242a6 Make progress on lemma 3.5 (4). 2021-03-24T15:24:34Z Chloe Brown chloe.brown.00@outlook.com 2021-03-24T15:24:34Z urn:sha1:ee1b20ca53363eee0362f5a2bbd61b5951098156 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 type relations. 2021-03-05T16:51:43Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T16:51:43Z urn:sha1:5cc5441cc0dd4705735cff985e466d144a23fb70 Add lifted types. 2021-03-05T16:24:02Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T16:24:02Z urn:sha1:701c0a2740b80bfb7f01fa426d18ef656a81f84d Add lemma 3.5.3. 2021-03-05T16:09:13Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T16:09:13Z urn:sha1:f2ad0f65cd73c834f0f94250141b2436c7edd63d Prove satisfiability of τε. 2021-03-05T15:44:38Z Chloe Brown chloe.brown.00@outlook.com 2021-03-05T15:44:38Z urn:sha1:b7227fb6ecb7b54313b14bd50381bdb504f13d5c There is a small error in the paper. It claims that L⊨τε if and only if L≈{ε}. However, from `⊨-anticongˡ` and `≤-min`, we have ∅⊨{ε}.