ch:mixml: ch:mixml

Problem and invariant. Implement finite component compatibility and initialization. After every accepted step, the state list contains exactly the slots written by the accepted prefix. The result is the five named cases recorded in appendix E.

Representation and construction. Use closed datatypes for slots, core types, polarities, components, merge results, and steps. Fold each finite component list into an accumulator. Insertion preserves a one-sided component, combines two imports, resolves an import/export pair to its export, and rejects unequal types or two exports. Then check the ordered keyword/token trace with read-subset and absent-write tests. Strings would shorten the declarations but admit malformed slots.

Failing version and acceptance. Adding a write before checking reads accepts the early-read reversal. Left-biased compatibility accepts duplicate exports; checking isolated pairs without constructing the accumulated list misses conflicts later in a signature. Run all four commands from appendix E and require the exact output and empty audit. The final assertion also requires successful construction of the two-component lexer/parser merge. The program illustrates lemma 15.4, lemma 15.5; it proves neither lemma and says nothing about the full three-pass theorem.