Theory Encodings
theory Encodings
imports ProcessCalculi
begin
section ‹Encodings›
text ‹In the simplest case an encoding from a source into a target language is a mapping from
source into target terms. Encodability criteria describe properties on such mappings. To
analyse encodability criteria we map them on conditions on relations between source and
target terms. More precisely, we consider relations on pairs of the disjoint union of
source and target terms. We denote this disjoint union of source and target terms by Proc.
›