Membership facts for the positive a b c slice witnesses

abcPositive is regular; the positive-slice intersections lang_eq_any_pos / lang_any_eq_pos (and the complement variants lang_not_eq_any_pos / lang_not_any_eq_pos) are deterministic context-free; and the positive {aⁿbⁿcⁿ} witness lang_eq_eq_pos is neither context-free nor deterministic context-free.

The bridge lang_eq_eq_pos_eq_inter identifies the explicit-replicate lang_eq_eq_pos (from Langlib.Examples.AnBnCnPos) with the intersection lang_eq_eq ⊓ abcPositive, so the deterministic non-closure proofs can reuse the shared definition.

theorem lang_eq_eq_pos_eq_inter : lang_eq_eq_pos = lang_eq_eq ⊓ abcPositive

The explicit positive witness lang_eq_eq_pos equals lang_eq_eq ⊓ abcPositive.

theorem abcPositive_regular : abcPositive.IsRegular

The slice a⁺ b⁺ c⁺ is regular.

theorem DCF_lang_eq_any_pos : is_DCF lang_eq_any_pos

theorem DCF_lang_any_eq_pos : is_DCF lang_any_eq_pos

theorem DCF_lang_not_eq_any_pos : is_DCF lang_not_eq_any_pos

theorem DCF_lang_not_any_eq_pos : is_DCF lang_not_any_eq_pos

theorem notDCF_lang_eq_eq_pos : ¬is_DCF lang_eq_eq_pos