LS2NF.acyclic

• Acyclicity of LS2NF

LS2NF.acyclic_wf

• Acyclic Relation

LS2NF.ambiguity

• Similarity of Parse Trees
• Two Notions of Ambiguity
• They Are Equal

LS2NF.derivation

• Derivation Relation Properties

LS2NF.encoding

• Assumptions
• Satisfying Model
• Encoding
  • Encoding Layout Constraints
  • Encoding Well-Formedness
  • Encoding Derivation Relation
  • Encoding Reachability Relation
  • Encoding the Existence of Dissimilar Parse Trees
  • Overall Encoding
• Formal Properties

LS2NF.grammar

• Sentences
• LS2NF
• Parsing

LS2NF.slice

• List Slice Properties

LS2NF.sub_derive

• Preliminary: Subtree Relation
• Sub-Derivation Relation
• Reachability Relation

LS2NF.util

• Utility Lemmas

LS2NF.witness

• Witness Relation Properties