The López–Escobar PC-class interface (issue #10, Unit 4 commit 1)

The base embedding baseGraphEmb : L →ᴸ graphLanguage (KLang L) (available because L is relational), and the code compatibility theorem tying the abstract PCMem on ℕ to membership in codeReduct '' ModelsOf Θ. This freezes the PC-class interface independently of López–Escobar's tree machinery.

def FirstOrder.Language.baseGraphEmb {L : Language} [L.IsRelational] : L →ᴸ L.KLang.graphLanguage

The base embedding of L into the relationalized graphLanguage (KLang L): functions are vacuous (L is relational), base relations go to their graph-language base image.

Equations

• One or more equations did not get rendered due to their size.