A Completeness Theorem for TLA

This is the beginning of a note that states and proves a relative completeness result for the axioms of TLA in the absence of temporal existential quantification (variable hiding). (The ancient LaTeX macros used to format the note only work on the first part. A text version of the complete note and of all other TLA notes are available here. There are undoubtedly errors in the proof, but I think they’re minor.