- Syntax of PCF2 - Generated by Autosubst2
- Preliminaries
- Typing and Reduction Relation in PCF2
- Contexts in PCF2
- Useful Functions and Results in PCF2
- Contextual and Observational Equivalence on PCF2
- Restricted Preorder Systems
- Preorder Systems
- Satisfiability of Words
- Equivalence of String Rewriting and Satisfiability of words - Attempt of Forward direction
- Reducing from Satisfiability of Words to Preorder Systems
- Reducing from Preorder Systems to Restricted Preorder Systems
- Reducing from the Complement of Restricted Preorder Systems to Contextual Equivalence
- Undecidability of Contextual Equivalence on PCF2