Typing theorems of omega algebra

Typed omega algebras extend Kozen’s typed Kleene algebras by an operation for infinite iteration in a similar way as Cohen’s omega algebras extend Kleene algebras in the untyped case. Typing these algebras is motivated by non-square matrices in automata constructions and applications in program semantics. For several reasons – the theory of untyped (Kleene or omega) algebras is well developed, results are easier to derive, and automation support is much better – it is beneficial to transfer theorems from the untyped algebras to their typed variants instead of constructing new proofs in the typed setting. Such a typing of theorems is facilitated by embedding typed algebras into their untyped variants. Extending previous work, we show that a large class of theorems of 1-free omega algebras can be transferred to typed omega algebras. This covers every universal 1-free formula which does not contain the greatest element at the beginning of an expression in a negative occurrence of an equation. Moreover, the formulas may be infinitary.