{aⁿbⁿcⁿ} is not deterministic context-free

Since {aⁿbⁿcⁿ} is not context-free (notCF_lang_eq_eq) and every deterministic context-free language is context-free, it is not deterministic context-free either.

theorem notDCF_lang_eq_eq : ¬is_DCF lang_eq_eq

{aⁿbⁿcⁿ | n ≥ 0} is not deterministic context-free.