Counterexamples in infinitary rewriting with non-fully-extended rules

We show counterexamples exist to confluence modulo hypercollapsing subterms, fair normalisation, and the normal form property in orthogonal infinitary higher-order rewriting with non-fully-extended rules. This sets these systems apart from both fully-extended and finite systems, where no such counterexamples are possible.

► We study orthogonal infinitary higher-order rewriting with non-fully-extended rules.
► Counterexamples exist to confluence modulo hypercollapsing subterms.
► Counterexamples also exist to fair normalisation and the normal form property.