Define a predomain Dyn that respects the extensional theory
The current definition of Dyn as a predomain is (everything is for a fixed clock k)
Dyn ≅ Nat + ▹(Dyn -->mon L Dyn)
where for a predomain X, L X is defined to have underlying type L℧ X and ordering is the step-sensitive (i.e. lock-step) error ordering on L℧ X.
The motivation for this Issue is the following question: What would happen if we gave L X a different ordering, specifically, the conjunction of two step-semi-insensitive orderings (one that tracks steps of the LHS term, and one that tracks steps of the RHS term)? Then we could define a new predomain Dyn2 using this this new lift predomain.
This will involve the following steps:
-
Define the two step-semi-inseneitive orderings -
Define the new ordering on L X as the conjunction of the above orderings
Edited by ericgio