Skip to content

Commit

Permalink
README: fix FST rows in proof table
Browse files Browse the repository at this point in the history 
In the camera ready paper, the theorems and proofs for FSTs changed a
bit.
This commit updates the paper<->agda correspondence table accordingly.
  • Loading branch information
@pmbittner
pmbittner committed Aug 28, 2024
1 parent 5f66d0e commit 42b9bef
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,9 +346,9 @@ The following table shows where each of the definitions, theorems, and proofs fr
| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.lagda.md](src/Lang/FST.lagda.md) | |
| Theorem 5.17 | OC ⋡ FST | `WFOC⋡FST` | [src/Translation/Lang/FST-to-OC.lagda.md](src/Translation/Lang/FST-to-OC.lagda.md) | |
| Theorem 5.18 | FST ⋡ OC | `FSTL⋡WFOCL` | [src/Translation/Lang/OC-to-FST.agda](src/Translation/Lang/OC-to-FST.agda) | |
| Corollary 5.19 | FST ⋡ 2CC | `FST⋡2CC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Theorem 5.20 | Sound(FST) | `FST-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| | 2CC ≽ FST | `2CC≽FST` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Corollary 5.19 | FST ⋡ CaO | `FST⋡VariantList` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Theorem 5.20 | CaO ≽ FST | `VariantList≽FST` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Corollary 5.21 | Sound(FST) | `FST-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |

Some formalizations in the library differ slightly from their in-paper-representation:

Expand Down

0 comments on commit 42b9bef

Please sign in to comment.