Synthetic Philosophy and Deductive Engineering
The task is to write ProofPower HOL specifications to define the SPaDEroot theory.
The details of why we need this theory, the role it will play and the content of the theory are provided in a first draft of the specification document The SPaDEroot Theory.
This theory is an exception to the general pattern of giving the same name to a theory as the document that specifies it.
The definition of the task is effectively split between the task descriptions given here, the text in the draft specification and the standard procedure for creating a new theory in ProofPower HOL ampd012.md.
This one task description document will be used to cover a sequence of stages in the development of the SPaDEroot theory, all progressive stages in writing the one specification document.
The prelude and the consistency mechanism are the present content of tlcd002.md.
The theory of T-expressions, including the packing functions used in its representation, is not part of this task. It is the theory T_ex, commissioned by tltd004.md and specified in tlcd004.md.
Further stages of SPaDEroot will be added here as that theory gains further content.