Proof of `Positive Ehrenfeucht–Fraïssé games` (1st statement)
groundedproofs/Lax503819Proofs/Definability.lean · lax-503819
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Corollary 3.8, with the finite-rank argument implemented by finite codes of word positions. The proof uses the proved game theorem through its helpers, not the concept axiom. Empty languages and universal languages are covered by empty disjunctions and conjunctions.