oxilean-std 0.1.2

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};

use super::types::{
    AnalyticSet, AnalyticSetData, BaireCategory, BorelHierarchy, BorelHierarchyChecker, BorelLevel,
    DescriptiveTree, DeterminacyGameSolver, DetermincyStrength, EffectiveBorelSet, FiniteTopSpace,
    ForcingPoset, InfiniteGame, LargeCardinal, LipschitzFunction, MartinsAxiom,
    OrbitEquivalenceRelation, PerfectSet, PolishSpace, PolishSpaceExample, ProjectiveHierarchy,
    ProjectiveLevel, ProjectiveLevelData, ProperForcingAxiom, ScottRank, UniversallyMeasurable,
    WadgeDegree, WadgeDegreesComputer, WadgeHierarchy, WellfoundedRelation,
};

pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
    app(app(f, a), b)
}
pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
    app(app2(f, a, b), c)
}
pub fn cst(s: &str) -> Expr {
    Expr::Const(Name::str(s), vec![])
}
pub fn prop() -> Expr {
    Expr::Sort(Level::zero())
}
pub fn type0() -> Expr {
    Expr::Sort(Level::succ(Level::zero()))
}
pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
}
pub fn arrow(a: Expr, b: Expr) -> Expr {
    pi(BinderInfo::Default, "_", a, b)
}
pub fn impl_pi(name: &str, dom: Expr, body: Expr) -> Expr {
    pi(BinderInfo::Implicit, name, dom, body)
}
pub fn bvar(n: u32) -> Expr {
    Expr::BVar(n)
}
pub fn nat_ty() -> Expr {
    cst("Nat")
}
pub fn bool_ty() -> Expr {
    cst("Bool")
}
pub fn real_ty() -> Expr {
    cst("Real")
}
/// PolishSpace type: a type X equipped with a separable complete metric.
/// PolishSpace : Type → Prop
pub fn polish_space_ty() -> Expr {
    arrow(type0(), prop())
}
/// BorelSet type: (X : Type) → Set X → Prop
/// A set is Borel if it lies in the σ-algebra generated by the open sets.
pub fn borel_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// SigmaClass (Σ⁰_α): (X : Type) → Ordinal → Set X → Prop
pub fn sigma_class_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(cst("Ordinal"), arrow(app(cst("Set"), bvar(1)), prop())),
    )
}
/// PiClass (Π⁰_α): (X : Type) → Ordinal → Set X → Prop
pub fn pi_class_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(cst("Ordinal"), arrow(app(cst("Set"), bvar(1)), prop())),
    )
}
/// DeltaClass (Δ⁰_α): (X : Type) → Ordinal → Set X → Prop
pub fn delta_class_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(cst("Ordinal"), arrow(app(cst("Set"), bvar(1)), prop())),
    )
}
/// OpenSet : (X : Type) → Set X → Prop (Σ⁰_1)
pub fn open_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// ClosedSet : (X : Type) → Set X → Prop (Π⁰_1)
pub fn closed_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// F_sigmaSet : (X : Type) → Set X → Prop (Σ⁰_2 = countable union of closed)
pub fn f_sigma_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// G_deltaSet : (X : Type) → Set X → Prop (Π⁰_2 = countable intersection of open)
pub fn g_delta_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// AnalyticSet (Σ¹_1): continuous image of a Borel set in a Polish space.
/// AnalyticSet : (X : Type) → Set X → Prop
pub fn analytic_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// CoanalyticSet (Π¹_1): complement of an analytic set.
/// CoanalyticSet : (X : Type) → Set X → Prop
pub fn coanalytic_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// SuslinScheme: a scheme of sets indexed by finite sequences.
/// SuslinScheme : (X : Type) → Type
pub fn suslin_scheme_ty() -> Expr {
    arrow(type0(), type0())
}
/// SuslinOperation (𝒜): applies a Suslin scheme and takes the analytic set.
/// SuslinOperation : (X : Type) → SuslinScheme X → Set X
pub fn suslin_operation_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(app(cst("SuslinScheme"), bvar(0)), app(cst("Set"), bvar(1))),
    )
}
/// ProjectiveSet (Σ¹_n / Π¹_n / Δ¹_n): defined by quantifying over reals.
/// ProjectiveClass : (X : Type) → Nat → Nat → Set X → Prop
/// Third Nat: 0 = Sigma, 1 = Pi, 2 = Delta.
pub fn projective_class_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            nat_ty(),
            arrow(nat_ty(), arrow(app(cst("Set"), bvar(2)), prop())),
        ),
    )
}
/// Sigma11Set: (X : Type) → Set X → Prop  (Σ¹_1 = analytic)
pub fn sigma11_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// Pi11Set: (X : Type) → Set X → Prop  (Π¹_1 = co-analytic)
pub fn pi11_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// Sigma12Set: (X : Type) → Set X → Prop  (Σ¹_2)
pub fn sigma12_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// PerfectSet: closed with no isolated points.
/// PerfectSet : (X : Type) → Set X → Prop
pub fn perfect_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// ScatteredSet: no perfect subset (Cantor–Bendixson complement).
/// ScatteredSet : (X : Type) → Set X → Prop
pub fn scattered_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// CantorBendixsonRank: the CB-rank of a point in a scattered set.
/// CBRank : (X : Type) → X → Ordinal
pub fn cb_rank_ty() -> Expr {
    impl_pi("X", type0(), arrow(bvar(0), cst("Ordinal")))
}
/// CantorBendixsonDerivative: X' = X minus isolated points.
/// CBDerivative : (X : Type) → Set X → Set X
pub fn cb_derivative_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(app(cst("Set"), bvar(0)), app(cst("Set"), bvar(1))),
    )
}
/// CantorBendixsonTheorem: every closed set = perfect ∪ countable scattered.
/// CBTheorem : (X : Type) → \[PolishSpace X\] → ∀ (F : Set X), ClosedSet F →
///             ∃ P C, PerfectSet P ∧ ScatteredSet C ∧ F = P ∪ C
pub fn cb_theorem_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("PolishSpace"), bvar(0)),
            arrow(
                app(cst("Set"), bvar(1)),
                arrow(
                    app2(cst("ClosedSet"), bvar(2), bvar(0)),
                    app2(cst("CBDecomposition"), bvar(3), bvar(1)),
                ),
            ),
        ),
    )
}
/// SeparableSpace: X has a countable dense subset.
/// SeparableSpace : Type → Prop
pub fn separable_space_ty() -> Expr {
    arrow(type0(), prop())
}
/// CompleteMetricSpace: X admits a complete metric.
/// CompleteMetricSpace : Type → Prop
pub fn complete_metric_space_ty() -> Expr {
    arrow(type0(), prop())
}
/// BaireSpace: the space ℕ^ℕ of infinite sequences of naturals.
/// BaireSpace : Type
pub fn baire_space_ty() -> Expr {
    type0()
}
/// CantorSpace: the Cantor set 2^ℕ.
/// CantorSpace : Type
pub fn cantor_space_ty() -> Expr {
    type0()
}
/// PolishEmbedding: every Polish space embeds into Baire space.
/// PolishEmbedding : (X : Type) → \[PolishSpace X\] → X → BaireSpace → Prop
pub fn polish_embedding_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("PolishSpace"), bvar(0)),
            arrow(bvar(1), arrow(cst("BaireSpace"), prop())),
        ),
    )
}
/// ZeroDiscloses: the space is zero-dimensional (basis of clopen sets).
/// ZeroDimensional : Type → Prop
pub fn zero_dimensional_ty() -> Expr {
    arrow(type0(), prop())
}
/// LuzinSeparation: disjoint analytic sets are separated by a Borel set.
/// LuzinSeparation :
///   (X : Type) → \[PolishSpace X\] →
///   ∀ (A B : Set X), AnalyticSet A → AnalyticSet B → Disjoint A B →
///   ∃ C : Set X, BorelSet C ∧ A ⊆ C ∧ B ⊆ Cᶜ
pub fn luzin_separation_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("PolishSpace"), bvar(0)),
            arrow(
                app(cst("Set"), bvar(1)),
                arrow(
                    app(cst("Set"), bvar(2)),
                    arrow(
                        app2(cst("AnalyticSet"), bvar(3), bvar(1)),
                        arrow(
                            app2(cst("AnalyticSet"), bvar(4), bvar(1)),
                            arrow(
                                app2(cst("Disjoint"), bvar(2), bvar(1)),
                                app3(cst("BorelSeparator"), bvar(5), bvar(3), bvar(2)),
                            ),
                        ),
                    ),
                ),
            ),
        ),
    )
}
/// SuslinTheorem: Δ¹_1 = Borel in a Polish space.
/// SuslinTheorem : (X : Type) → \[PolishSpace X\] →
///   ∀ (A : Set X), Delta11Set A ↔ BorelSet A
pub fn suslin_theorem_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("PolishSpace"), bvar(0)),
            arrow(
                app(cst("Set"), bvar(1)),
                app2(
                    cst("Iff"),
                    app2(cst("Delta11Set"), bvar(2), bvar(0)),
                    app2(cst("BorelSet"), bvar(3), bvar(0)),
                ),
            ),
        ),
    )
}
/// SuslinRepresentation: every analytic set has a Suslin representation.
/// SuslinRepresentation : (X : Type) → \[PolishSpace X\] →
///   ∀ (A : Set X), AnalyticSet A → ∃ s : SuslinScheme X, SuslinOperation s = A
pub fn suslin_representation_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("PolishSpace"), bvar(0)),
            arrow(
                app(cst("Set"), bvar(1)),
                arrow(
                    app2(cst("AnalyticSet"), bvar(2), bvar(0)),
                    app2(cst("HasSuslinRepresentation"), bvar(3), bvar(1)),
                ),
            ),
        ),
    )
}
/// GameTree: the game tree Aω of infinite plays over an alphabet A.
/// GameTree : Type → Type
pub fn game_tree_ty() -> Expr {
    arrow(type0(), type0())
}
/// Strategy: a function choosing moves for one player.
/// Strategy : (A : Type) → GameTree A → Type
pub fn strategy_ty() -> Expr {
    impl_pi("A", type0(), arrow(app(cst("GameTree"), bvar(0)), type0()))
}
/// WinningStrategy: a strategy that wins every play against any opponent.
/// WinningStrategy : (A : Type) → GameTree A → Strategy A t → Prop
pub fn winning_strategy_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(
            app(cst("GameTree"), bvar(0)),
            arrow(app2(cst("Strategy"), bvar(1), bvar(0)), prop()),
        ),
    )
}
/// Determined: the payoff set A ⊆ ωω — one player has a winning strategy.
/// Determined : Set (GameTree Nat) → Prop
pub fn determined_ty() -> Expr {
    arrow(app(cst("Set"), app(cst("GameTree"), nat_ty())), prop())
}
/// OpenDeterminacy (Gale–Stewart): every open payoff set is determined.
pub fn open_determinacy_ty() -> Expr {
    arrow(
        app2(cst("OpenSet"), app(cst("GameTree"), nat_ty()), bvar(0)),
        app(cst("Determined"), bvar(0)),
    )
}
/// BorelDeterminacy (Martin): every Borel payoff set is determined (ZFC).
pub fn borel_determinacy_ty() -> Expr {
    arrow(
        app2(cst("BorelSet"), app(cst("GameTree"), nat_ty()), bvar(0)),
        app(cst("Determined"), bvar(0)),
    )
}
/// AnalyticDeterminacy: every analytic payoff is determined (from measurable cardinal).
pub fn analytic_determinacy_ty() -> Expr {
    arrow(
        app(cst("MeasurableCardinal"), cst("kappa")),
        arrow(
            app2(cst("AnalyticSet"), app(cst("GameTree"), nat_ty()), bvar(1)),
            app(cst("Determined"), bvar(1)),
        ),
    )
}
/// AxiomOfDeterminacy (AD): all subsets of ωω are determined.
/// AD : Prop
pub fn axiom_of_determinacy_ty() -> Expr {
    prop()
}
/// ProjectiveDeterminacy (PD): all projective sets are determined.
/// PD : Prop
pub fn projective_determinacy_ty() -> Expr {
    prop()
}
/// MeasurableCardinal: a cardinal κ with a κ-complete non-principal ultrafilter.
/// MeasurableCardinal : Ordinal → Prop
pub fn measurable_cardinal_ty() -> Expr {
    arrow(cst("Ordinal"), prop())
}
/// WoodinCardinal: a large cardinal stronger than measurable, key for AD.
/// WoodinCardinal : Ordinal → Prop
pub fn woodin_cardinal_ty() -> Expr {
    arrow(cst("Ordinal"), prop())
}
/// StrongCardinal: a strong cardinal (Ketonen–Solovay).
/// StrongCardinal : Ordinal → Prop
pub fn strong_cardinal_ty() -> Expr {
    arrow(cst("Ordinal"), prop())
}
/// MeasurableImpliesAnalyticDet: measurable cardinal implies analytic determinacy.
pub fn measurable_implies_analytic_det_ty() -> Expr {
    arrow(
        app(cst("MeasurableCardinal"), cst("kappa")),
        cst("AnalyticDeterminacy"),
    )
}
/// WoodinImpliesProjectiveDet: ω many Woodin cardinals imply PD.
pub fn woodin_implies_projective_det_ty() -> Expr {
    arrow(
        app(cst("OmegaManyWoodinCardinals"), cst("delta")),
        cst("ProjectiveDeterminacy"),
    )
}
/// UniversalBorelSet: a set that is Σ⁰_n-universal (complete for the class).
/// UniversalBorelSet : (X : Type) → Nat → Set (Nat × X) → Prop
pub fn universal_borel_set_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            nat_ty(),
            arrow(
                app(cst("Set"), app2(cst("Prod"), nat_ty(), bvar(1))),
                prop(),
            ),
        ),
    )
}
/// CompleteBorelSet: a set that is Σ⁰_n-complete (hardest in the class).
/// CompleteBorelSet : (X : Type) → Nat → Set X → Prop
pub fn complete_borel_set_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(nat_ty(), arrow(app(cst("Set"), bvar(1)), prop())),
    )
}
/// BorelIsomorphism: a bijection that is Borel in both directions.
/// BorelIsomorphism : (X Y : Type) → (X → Y) → Prop
pub fn borel_isomorphism_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        impl_pi("Y", type0(), arrow(arrow(bvar(1), bvar(1)), prop())),
    )
}
/// StandardBorelSpace: a measurable space isomorphic to a Borel subset of a Polish space.
/// StandardBorelSpace : Type → Prop
pub fn standard_borel_space_ty() -> Expr {
    arrow(type0(), prop())
}
/// Pi11Norm: a Π¹_1 rank function witnessing Π¹_1-completeness.
/// Pi11Norm : (X : Type) → Set X → (X → Ordinal) → Prop
pub fn pi11_norm_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("Set"), bvar(0)),
            arrow(arrow(bvar(1), cst("Ordinal")), prop()),
        ),
    )
}
/// Sigma12Set (Σ¹_2): (X : Type) → Set X → Prop  (already exists as sigma12_set_ty)
/// Pi12Set (Π¹_2): (X : Type) → Set X → Prop
pub fn pi12_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// Delta12Set (Δ¹_2): (X : Type) → Set X → Prop
pub fn delta12_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// ProjectiveDeterminacyAxiom: all Σ¹_n sets are determined.
/// PDAxiom : Nat → Prop
pub fn pd_axiom_ty() -> Expr {
    arrow(nat_ty(), prop())
}
/// WadgeDegree: the equivalence class of a set under Wadge reducibility.
/// WadgeDegree : (X : Type) → Set X → Type
pub fn wadge_degree_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), type0()))
}
/// WadgeLemma: any two sets are Wadge comparable (assuming AD).
/// WadgeLemma : (X : Type) → Set X → Set X → Prop
pub fn wadge_lemma_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("Set"), bvar(0)),
            arrow(app(cst("Set"), bvar(1)), prop()),
        ),
    )
}
/// WeihrauchReducibility: f ≤_W g (Weihrauch reducibility of multi-valued functions).
/// WeihrauchReducibility : (A B C D : Type) → (A → B) → (C → D) → Prop
pub fn weihrauch_reducibility_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        impl_pi(
            "B",
            type0(),
            arrow(
                arrow(bvar(1), bvar(1)),
                arrow(arrow(bvar(2), bvar(2)), prop()),
            ),
        ),
    )
}
/// SteelWadge: under AD, the Wadge order is well-founded.
/// SteelWadge : Prop
pub fn steel_wadge_ty() -> Expr {
    prop()
}
/// OrbitEquivRelation: E_G on X — the orbit equivalence relation of a group action.
/// OrbitEquivRelation : (G X : Type) → (G → X → X) → Set (X × X) → Prop
pub fn orbit_equiv_relation_ty() -> Expr {
    impl_pi(
        "G",
        type0(),
        impl_pi(
            "X",
            type0(),
            arrow(
                arrow(bvar(1), arrow(bvar(1), bvar(1))),
                arrow(app(cst("Set"), app2(cst("Prod"), bvar(2), bvar(2))), prop()),
            ),
        ),
    )
}
/// BorelReducibility: E ≤_B F (Borel reducibility of equivalence relations).
/// BorelReducibility : (X Y : Type) → Set (X × X) → Set (Y × Y) → Prop
pub fn borel_reducibility_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        impl_pi(
            "Y",
            type0(),
            arrow(
                app(cst("Set"), app2(cst("Prod"), bvar(1), bvar(1))),
                arrow(app(cst("Set"), app2(cst("Prod"), bvar(2), bvar(2))), prop()),
            ),
        ),
    )
}
/// HyperfiniteEquivRelation: equivalence relation that is a union of finite equiv. relations.
/// HyperfiniteEquivRelation : (X : Type) → Set (X × X) → Prop
pub fn hyperfinite_equiv_relation_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(app(cst("Set"), app2(cst("Prod"), bvar(0), bvar(0))), prop()),
    )
}
/// BorelEmbedding: a Borel reduction witnessing E ≤_B F injectively.
/// BorelEmbedding : (X Y : Type) → (X → Y) → Prop
pub fn borel_embedding_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        impl_pi("Y", type0(), arrow(arrow(bvar(1), bvar(1)), prop())),
    )
}
/// LebesgueMeasurable: a set is Lebesgue measurable.
/// LebesgueMeasurable : Set Real → Prop
pub fn lebesgue_measurable_ty() -> Expr {
    arrow(app(cst("Set"), real_ty()), prop())
}
/// LuzinNSet: a set of Lebesgue measure zero (Luzin N-property).
/// LuzinNSet : Set Real → Prop
pub fn luzin_n_set_ty() -> Expr {
    arrow(app(cst("Set"), real_ty()), prop())
}
/// UniformlyMeasurableFamily: a parametric family of measurable sets.
/// UniformlyMeasurableFamily : (X : Type) → (X → Set Real) → Prop
pub fn uniformly_measurable_family_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(arrow(bvar(0), app(cst("Set"), real_ty())), prop()),
    )
}
/// RegularBorelMeasure: a Borel measure that is inner/outer regular.
/// RegularBorelMeasure : Type → Prop
pub fn regular_borel_measure_ty() -> Expr {
    arrow(type0(), prop())
}
/// MeagerSet: a set of first category (countable union of nowhere dense sets).
/// MeagerSet : (X : Type) → Set X → Prop
pub fn meager_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// ComeagerSet: complement of a meager set (residual).
/// ComeagerSet : (X : Type) → Set X → Prop
pub fn comeager_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// NowhereDenseSet: a set whose closure has empty interior.
/// NowhereDenseSet : (X : Type) → Set X → Prop
pub fn nowhere_dense_set_ty() -> Expr {
    impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop()))
}
/// KuratowskiUlam: the Kuratowski–Ulam theorem (Fubini for category).
/// KuratowskiUlam : (X Y : Type) → \[PolishSpace X\] → \[PolishSpace Y\] →
///   ∀ (A : Set (X × Y)), MeagerSet A ↔ ...
pub fn kuratowski_ulam_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        impl_pi(
            "Y",
            type0(),
            arrow(
                app(cst("PolishSpace"), bvar(1)),
                arrow(
                    app(cst("PolishSpace"), bvar(1)),
                    arrow(app(cst("Set"), app2(cst("Prod"), bvar(3), bvar(2))), prop()),
                ),
            ),
        ),
    )
}
/// BaireCategoryTheorem: a completely metrizable space is not meager in itself.
/// BaireCategoryTheorem : (X : Type) → \[CompleteMetricSpace X\] → Prop
pub fn baire_category_theorem_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(app(cst("CompleteMetricSpace"), bvar(0)), prop()),
    )
}
/// Pi11Complete: a set is Π¹_1-complete (hardest co-analytic set).
/// Pi11Complete : Set Nat → Prop
pub fn pi11_complete_ty() -> Expr {
    arrow(app(cst("Set"), nat_ty()), prop())
}
/// HyperarithmeticSet: a set in the lightface Δ¹_1 (hyperarithmetic) hierarchy.
/// HyperarithmeticSet : Set Nat → Prop
pub fn hyperarithmetic_set_ty() -> Expr {
    arrow(app(cst("Set"), nat_ty()), prop())
}
/// RecursiveOrdinal: a computable ordinal (< ω_1^CK).
/// RecursiveOrdinal : Ordinal → Prop
pub fn recursive_ordinal_ty() -> Expr {
    arrow(cst("Ordinal"), prop())
}
/// ChurchKleeneOrdinal: ω_1^CK, the first non-recursive ordinal.
/// ChurchKleeneOrdinal : Ordinal
pub fn church_kleene_ordinal_ty() -> Expr {
    cst("Ordinal")
}
/// CoanalyticRank: a Π¹_1 norm / rank function on a co-analytic set.
/// CoanalyticRank : (X : Type) → Set X → (X → Ordinal) → Prop
pub fn coanalytic_rank_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("Set"), bvar(0)),
            arrow(arrow(bvar(1), cst("Ordinal")), prop()),
        ),
    )
}
/// BoundednessTheorem: every Π¹_1 set of ordinals is bounded below ω_1^CK.
/// BoundednessTheorem : Set Ordinal → Prop
pub fn boundedness_theorem_ty() -> Expr {
    arrow(app(cst("Set"), cst("Ordinal")), prop())
}
/// ScottRank: the Scott rank of a countable structure.
/// ScottRank : Type → Ordinal
pub fn scott_rank_ty() -> Expr {
    arrow(type0(), cst("Ordinal"))
}
/// VaughtConjecture: an Lω1ω sentence has either ≤ ℵ_0 or exactly 2^ℵ_0 countable models.
/// VaughtConjecture : Prop
pub fn vaught_conjecture_ty() -> Expr {
    prop()
}
/// LopezEscobarTheorem: invariant Borel sets correspond to Lω1ω formulas.
/// LopezEscobarTheorem : Prop
pub fn lopez_escobar_theorem_ty() -> Expr {
    prop()
}
/// ChoquetGame: the Choquet game on a topological space.
/// ChoquetGame : Type → Type
pub fn choquet_game_ty() -> Expr {
    arrow(type0(), type0())
}
/// ChoquetComplete: a space where Player II has a winning strategy in the Choquet game.
/// ChoquetComplete : Type → Prop
pub fn choquet_complete_ty() -> Expr {
    arrow(type0(), prop())
}
/// ChoquetCompleteImpliesPolish: a second-countable Choquet-complete space is Polish.
/// ChoquetCompleteImpliesPolish : (X : Type) → \[Choquet_Complete X\] → PolishSpace X
pub fn choquet_complete_implies_polish_ty() -> Expr {
    impl_pi(
        "X",
        type0(),
        arrow(
            app(cst("ChoquetComplete"), bvar(0)),
            app(cst("PolishSpace"), bvar(1)),
        ),
    )
}
/// Register all descriptive-set-theory axioms into the given kernel environment.
pub fn build_descriptive_set_theory_env() -> Environment {
    let mut env = Environment::new();
    let axioms: &[(&str, Expr)] = &[
        ("PolishSpace", polish_space_ty()),
        ("SeparableSpace", separable_space_ty()),
        ("CompleteMetricSpace", complete_metric_space_ty()),
        ("BaireSpace", baire_space_ty()),
        ("CantorSpace", cantor_space_ty()),
        ("ZeroDimensional", zero_dimensional_ty()),
        ("PolishEmbedding", polish_embedding_ty()),
        ("BorelSet", borel_set_ty()),
        ("SigmaClass", sigma_class_ty()),
        ("PiClass", pi_class_ty()),
        ("DeltaClass", delta_class_ty()),
        ("OpenSet", open_set_ty()),
        ("ClosedSet", closed_set_ty()),
        ("FSigmaSet", f_sigma_set_ty()),
        ("GDeltaSet", g_delta_set_ty()),
        ("AnalyticSet", analytic_set_ty()),
        ("CoanalyticSet", coanalytic_set_ty()),
        ("SuslinScheme", suslin_scheme_ty()),
        ("SuslinOperation", suslin_operation_ty()),
        ("ProjectiveClass", projective_class_ty()),
        ("Sigma11Set", sigma11_set_ty()),
        ("Pi11Set", pi11_set_ty()),
        ("Sigma12Set", sigma12_set_ty()),
        ("PerfectSet", perfect_set_ty()),
        ("ScatteredSet", scattered_set_ty()),
        ("CBRank", cb_rank_ty()),
        ("CBDerivative", cb_derivative_ty()),
        ("CantorBendixsonTheorem", cb_theorem_ty()),
        ("LuzinSeparation", luzin_separation_ty()),
        ("SuslinTheorem", suslin_theorem_ty()),
        ("SuslinRepresentation", suslin_representation_ty()),
        ("GameTree", game_tree_ty()),
        ("Strategy", strategy_ty()),
        ("WinningStrategy", winning_strategy_ty()),
        ("Determined", determined_ty()),
        ("OpenDeterminacy", open_determinacy_ty()),
        ("BorelDeterminacy", borel_determinacy_ty()),
        ("AnalyticDeterminacy", analytic_determinacy_ty()),
        ("AxiomOfDeterminacy", axiom_of_determinacy_ty()),
        ("ProjectiveDeterminacy", projective_determinacy_ty()),
        ("MeasurableCardinal", measurable_cardinal_ty()),
        ("WoodinCardinal", woodin_cardinal_ty()),
        ("StrongCardinal", strong_cardinal_ty()),
        (
            "MeasurableImpliesAnalyticDet",
            measurable_implies_analytic_det_ty(),
        ),
        (
            "WoodinImpliesProjectiveDet",
            woodin_implies_projective_det_ty(),
        ),
        ("Ordinal", type0()),
        ("Disjoint", arrow(type0(), arrow(type0(), prop()))),
        ("Set", arrow(type0(), type0())),
        (
            "Delta11Set",
            impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop())),
        ),
        (
            "CBDecomposition",
            impl_pi(
                "X",
                type0(),
                arrow(
                    app(cst("Set"), bvar(0)),
                    arrow(app(cst("Set"), bvar(1)), prop()),
                ),
            ),
        ),
        (
            "HasSuslinRepresentation",
            impl_pi("X", type0(), arrow(app(cst("Set"), bvar(0)), prop())),
        ),
        (
            "BorelSeparator",
            impl_pi(
                "X",
                type0(),
                arrow(
                    app(cst("Set"), bvar(0)),
                    arrow(app(cst("Set"), bvar(1)), prop()),
                ),
            ),
        ),
        ("OmegaManyWoodinCardinals", arrow(cst("Ordinal"), prop())),
        ("UniversalBorelSet", universal_borel_set_ty()),
        ("CompleteBorelSet", complete_borel_set_ty()),
        ("BorelIsomorphism", borel_isomorphism_ty()),
        ("StandardBorelSpace", standard_borel_space_ty()),
        ("Prod", arrow(type0(), arrow(type0(), type0()))),
        ("Pi12Set", pi12_set_ty()),
        ("Delta12Set", delta12_set_ty()),
        ("PDAxiom", pd_axiom_ty()),
        ("Pi11Norm", pi11_norm_ty()),
        ("WadgeDegree", wadge_degree_ty()),
        ("WadgeLemma", wadge_lemma_ty()),
        ("WeihrauchReducibility", weihrauch_reducibility_ty()),
        ("SteelWadge", steel_wadge_ty()),
        ("OrbitEquivRelation", orbit_equiv_relation_ty()),
        ("BorelReducibility", borel_reducibility_ty()),
        ("HyperfiniteEquivRelation", hyperfinite_equiv_relation_ty()),
        ("BorelEmbedding", borel_embedding_ty()),
        ("LebesgueMeasurable", lebesgue_measurable_ty()),
        ("LuzinNSet", luzin_n_set_ty()),
        (
            "UniformlyMeasurableFamily",
            uniformly_measurable_family_ty(),
        ),
        ("RegularBorelMeasure", regular_borel_measure_ty()),
        ("MeagerSet", meager_set_ty()),
        ("ComeagerSet", comeager_set_ty()),
        ("NowhereDenseSet", nowhere_dense_set_ty()),
        ("KuratowskiUlam", kuratowski_ulam_ty()),
        ("BaireCategoryTheorem", baire_category_theorem_ty()),
        ("Pi11Complete", pi11_complete_ty()),
        ("HyperarithmeticSet", hyperarithmetic_set_ty()),
        ("RecursiveOrdinal", recursive_ordinal_ty()),
        ("ChurchKleeneOrdinal", church_kleene_ordinal_ty()),
        ("CoanalyticRank", coanalytic_rank_ty()),
        ("BoundednessTheorem", boundedness_theorem_ty()),
        ("ScottRank", scott_rank_ty()),
        ("VaughtConjecture", vaught_conjecture_ty()),
        ("LopezEscobarTheorem", lopez_escobar_theorem_ty()),
        ("ChoquetGame", choquet_game_ty()),
        ("ChoquetComplete", choquet_complete_ty()),
        (
            "ChoquetCompleteImpliesPolish",
            choquet_complete_implies_polish_ty(),
        ),
    ];
    for (name, ty) in axioms {
        let _ = env.add(Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        });
    }
    env
}
#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn test_build_descriptive_set_theory_env() {
        let env = build_descriptive_set_theory_env();
        assert!(env.get(&Name::str("PolishSpace")).is_some());
        assert!(env.get(&Name::str("BorelSet")).is_some());
        assert!(env.get(&Name::str("AnalyticSet")).is_some());
        assert!(env.get(&Name::str("PerfectSet")).is_some());
        assert!(env.get(&Name::str("CantorBendixsonTheorem")).is_some());
        assert!(env.get(&Name::str("LuzinSeparation")).is_some());
        assert!(env.get(&Name::str("SuslinTheorem")).is_some());
        assert!(env.get(&Name::str("BorelDeterminacy")).is_some());
        assert!(env.get(&Name::str("MeasurableCardinal")).is_some());
        assert!(env.get(&Name::str("WoodinCardinal")).is_some());
    }
    #[test]
    fn test_borel_level_dual() {
        assert_eq!(BorelLevel::Sigma(1).dual(), BorelLevel::Pi(1));
        assert_eq!(BorelLevel::Pi(2).dual(), BorelLevel::Sigma(2));
        assert_eq!(BorelLevel::Delta(3).dual(), BorelLevel::Delta(3));
    }
    #[test]
    fn test_borel_level_properties() {
        assert!(BorelLevel::Sigma(1).is_open());
        assert!(BorelLevel::Pi(1).is_closed());
        assert!(!BorelLevel::Sigma(2).is_open());
        assert_eq!(BorelLevel::Sigma(3).rank(), 3);
        assert_eq!(BorelLevel::Delta(5).rank(), 5);
    }
    #[test]
    fn test_projective_level() {
        assert!(ProjectiveLevel::Sigma(1).is_analytic());
        assert!(ProjectiveLevel::Pi(1).is_coanalytic());
        assert!(ProjectiveLevel::Delta(1).is_borel());
        assert_eq!(ProjectiveLevel::Sigma(2).dual(), ProjectiveLevel::Pi(2));
    }
    #[test]
    fn test_cantor_bendixson_scattered() {
        let mut space = FiniteTopSpace::new(3);
        space.mark_isolated(0);
        space.mark_isolated(1);
        space.mark_isolated(2);
        assert!(space.is_scattered());
        assert_eq!(space.cb_rank(), 1);
    }
    #[test]
    fn test_cantor_bendixson_perfect_candidate() {
        let space = FiniteTopSpace::new(4);
        assert!(!space.is_scattered());
        assert_eq!(space.cb_rank(), u32::MAX);
    }
    #[test]
    fn test_polish_space_examples() {
        let r = PolishSpaceExample::real_line();
        assert!(!r.compact);
        assert!(r.locally_compact);
        let bs = PolishSpaceExample::baire_space();
        assert!(bs.is_baire_space);
        assert!(bs.zero_dimensional);
        let cs = PolishSpaceExample::cantor_space();
        assert!(cs.compact);
        assert!(cs.zero_dimensional);
    }
    #[test]
    fn test_determinacy_strength_ordering() {
        assert!(DetermincyStrength::Open < DetermincyStrength::Borel);
        assert!(DetermincyStrength::Borel < DetermincyStrength::Analytic);
        assert!(DetermincyStrength::Analytic < DetermincyStrength::Full);
        assert!(DetermincyStrength::Borel.provable_in_zfc());
        assert!(!DetermincyStrength::Analytic.provable_in_zfc());
        assert!(DetermincyStrength::Projective.requires_large_cardinal());
        assert!(!DetermincyStrength::Open.requires_large_cardinal());
    }
}
#[cfg(test)]
mod spec_wrapper_tests {
    use super::*;
    #[test]
    fn test_polish_space() {
        let ps = PolishSpace::new(true, true);
        assert!(ps.is_polish());
        assert!(ps.is_zero_dimensional());
        assert_eq!(ps.topological_classification(), "Polish");
        let ns = PolishSpace::new(false, true);
        assert!(!ns.is_polish());
        assert_eq!(ns.topological_classification(), "non-separable");
    }
    #[test]
    fn test_borel_hierarchy() {
        let s1 = BorelHierarchy::sigma(1);
        assert!(s1.closed_under_unions());
        assert!(!s1.closed_under_intersections());
        assert!(!s1.closed_under_complements());
        assert_eq!(s1.dual(), BorelHierarchy::pi(1));
        let p2 = BorelHierarchy::pi(2);
        assert!(!p2.closed_under_unions());
        assert!(p2.closed_under_intersections());
    }
    #[test]
    fn test_analytic_set() {
        let a = AnalyticSet::new("reals");
        assert!(a.is_continuous_image_of_borel());
        assert!(a.is_souslin());
        let b = AnalyticSet::new("reals");
        assert!(a.luzin_separation(&b));
    }
    #[test]
    fn test_universally_measurable() {
        let um = UniversallyMeasurable::new("A");
        assert!(um.is_universally_measurable());
        assert!(um.inner_regularity());
    }
    #[test]
    fn test_projective_hierarchy() {
        let p1 = ProjectiveHierarchy::new(1);
        assert!(p1.sigma_1_1_is_analytic());
        assert!(p1.pi_1_1_is_coanalytic());
        assert!(p1.determinacy());
        let p2 = ProjectiveHierarchy::new(2);
        assert!(!p2.sigma_1_1_is_analytic());
        assert!(!p2.determinacy());
    }
    #[test]
    fn test_perfect_set() {
        let ps = PerfectSet::new("Cantor space");
        assert!(ps.has_continuum_many_points());
        let (has_perfect, has_scattered) = ps.cantor_bendixson();
        assert!(has_perfect);
        assert!(has_scattered);
        assert!(ps.perfect_set_thm());
    }
    #[test]
    fn test_lipschitz_function() {
        let f = LipschitzFunction::new(2.0, "R");
        assert!(f.is_uniformly_continuous());
        assert!(f.is_measurable());
        assert!(f.rademacher_theorem());
    }
    #[test]
    fn test_wadge_hierarchy() {
        let wh = WadgeHierarchy::new();
        assert!(wh.wadge_reducibility());
        assert!(wh.martin_steel_theorem());
    }
    #[test]
    fn test_infinite_game() {
        let g = InfiniteGame::new("Player I", "Borel set");
        assert!(g.is_determined());
        assert!(g.borel_determinacy());
    }
}
#[cfg(test)]
mod new_impl_tests {
    use super::*;
    #[test]
    fn test_borel_hierarchy_checker() {
        let mut checker = BorelHierarchyChecker::new(1, true);
        checker.register("open_set_A");
        checker.register("open_set_B");
        assert!(checker.contains("open_set_A"));
        assert!(!checker.contains("closed_set_C"));
        assert_eq!(checker.class_name(), "Σ⁰_1");
        assert!(checker.closed_under_unions());
        assert!(!checker.closed_under_intersections());
        let dual = checker.dual();
        assert_eq!(dual.class_name(), "Π⁰_1");
        let succ = checker.successor();
        assert_eq!(succ.class_name(), "Π⁰_1");
        let succ2 = dual.successor();
        assert_eq!(succ2.class_name(), "Σ⁰_2");
    }
    #[test]
    fn test_wadge_degrees_computer() {
        let mut wdc = WadgeDegreesComputer::new();
        wdc.assign("clopen", 1);
        wdc.assign("open", 2);
        wdc.assign("closed", 2);
        wdc.assign("f_sigma", 3);
        assert!(wdc.wadge_le("clopen", "open"));
        assert!(wdc.wadge_le("open", "f_sigma"));
        assert!(!wdc.wadge_le("f_sigma", "clopen"));
        assert!(wdc.wadge_equiv("open", "closed"));
        let min = wdc.minimal();
        assert_eq!(min, Some("clopen"));
        let red = wdc.reducible_to("open");
        assert!(red.contains(&"clopen"));
    }
    #[test]
    fn test_determinacy_game_solver_trivial() {
        let mut solver = DeterminacyGameSolver::new(1);
        solver.set_payoff(0, true);
        assert!(solver.is_determined());
        assert_eq!(solver.winner(), Some(true));
    }
    #[test]
    fn test_determinacy_game_solver_tree() {
        let mut solver = DeterminacyGameSolver::new(3);
        solver.set_player(0, true);
        solver.add_move(0, 1);
        solver.add_move(0, 2);
        solver.set_payoff(1, false);
        solver.set_payoff(2, true);
        assert!(solver.is_determined());
        assert_eq!(solver.winner(), Some(true));
    }
    #[test]
    fn test_orbit_equivalence_relation() {
        let mut rel = OrbitEquivalenceRelation::new(5);
        rel.union(0, 1);
        rel.union(1, 2);
        rel.union(3, 4);
        assert!(rel.same_orbit(0, 2));
        assert!(rel.same_orbit(3, 4));
        assert!(!rel.same_orbit(0, 3));
        assert_eq!(rel.num_orbits(), 2);
        assert!(rel.is_smooth());
        assert!(rel.is_hyperfinite());
    }
    #[test]
    fn test_dst_env_new_axioms() {
        let env = build_descriptive_set_theory_env();
        assert!(env.get(&Name::str("UniversalBorelSet")).is_some());
        assert!(env.get(&Name::str("StandardBorelSpace")).is_some());
        assert!(env.get(&Name::str("Pi12Set")).is_some());
        assert!(env.get(&Name::str("PDAxiom")).is_some());
        assert!(env.get(&Name::str("WadgeLemma")).is_some());
        assert!(env.get(&Name::str("SteelWadge")).is_some());
        assert!(env.get(&Name::str("BorelReducibility")).is_some());
        assert!(env.get(&Name::str("HyperfiniteEquivRelation")).is_some());
        assert!(env.get(&Name::str("LebesgueMeasurable")).is_some());
        assert!(env.get(&Name::str("RegularBorelMeasure")).is_some());
        assert!(env.get(&Name::str("MeagerSet")).is_some());
        assert!(env.get(&Name::str("BaireCategoryTheorem")).is_some());
        assert!(env.get(&Name::str("Pi11Complete")).is_some());
        assert!(env.get(&Name::str("HyperarithmeticSet")).is_some());
        assert!(env.get(&Name::str("CoanalyticRank")).is_some());
        assert!(env.get(&Name::str("BoundednessTheorem")).is_some());
        assert!(env.get(&Name::str("VaughtConjecture")).is_some());
        assert!(env.get(&Name::str("LopezEscobarTheorem")).is_some());
        assert!(env.get(&Name::str("ChoquetComplete")).is_some());
        assert!(env
            .get(&Name::str("ChoquetCompleteImpliesPolish"))
            .is_some());
    }
}
#[cfg(test)]
mod extended_dst_tests {
    use super::*;
    #[test]
    fn test_analytic_set() {
        let a = AnalyticSetData::new("A", false);
        assert!(!a.is_borel);
        assert_eq!(
            AnalyticSetData::separation_description(),
            "Disjoint analytic sets are Borel-separated"
        );
    }
    #[test]
    fn test_projective_level() {
        let l1 = ProjectiveLevelData::level(1);
        assert!(l1.is_analytic());
        assert!(l1.closed_under_continuous_preimage());
    }
    #[test]
    fn test_descriptive_tree() {
        let t = DescriptiveTree::well_founded(vec!["0".to_string(), "1".to_string()]);
        assert!(t.is_well_founded);
        assert!(!t.has_infinite_branch());
        assert!(t.kleene_brouwer_applies());
    }
    #[test]
    fn test_baire_category() {
        let m = BaireCategory::meager("R");
        assert!(m.is_meager);
        assert!(!m.is_comeager);
    }
    #[test]
    fn test_wadge() {
        let w = WadgeDegree::new("A", 3, false);
        assert!(w.has_complement_pair());
        assert!(WadgeDegree::wadge_lemma_description().contains("Wadge"));
    }
    #[test]
    fn test_scott_rank() {
        let sr = ScottRank::new("(Q, <)", 2);
        assert!(sr.scott_sentence_description().contains("Scott"));
    }
}
#[cfg(test)]
mod tests_dst_ext {
    use super::*;
    #[test]
    fn test_effective_borel_set() {
        let rec = EffectiveBorelSet::recursive_set("K");
        assert!(rec.is_recursive);
        let corr = rec.lightface_boldface_correspondence();
        assert!(corr.contains("oracle"));
        let charac = rec.characterization();
        assert!(charac.contains("Δ"));
        let re_set = EffectiveBorelSet::re_set("W_e");
        assert!(!re_set.is_recursive);
        let mosc = re_set.moschovakis_theorem();
        assert!(mosc.contains("Moschovakis"));
    }
    #[test]
    fn test_wellfounded_relation() {
        let nat = WellfoundedRelation::natural_numbers();
        assert!(nat.is_linear);
        assert_eq!(nat.order_type, "ω");
        let kb = nat.kleene_brouwer_ordering();
        assert!(kb.contains("KB"));
        let pi11 = nat.rank_pi11_characterization();
        assert!(pi11.contains("Π^1_1"));
    }
    #[test]
    fn test_large_cardinal() {
        let meas = LargeCardinal::measurable_cardinal();
        assert!(meas.is_measurable);
        let pd = meas.projective_determinacy_connection();
        assert!(pd.contains("Martin"));
        let sharp = meas.silver_indiscernibles();
        assert!(sharp.contains("0#"));
        let woodin = LargeCardinal::woodin_cardinal();
        let wd = woodin.projective_determinacy_connection();
        assert!(wd.contains("Woodin"));
    }
    #[test]
    fn test_forcing_poset() {
        let cohen = ForcingPoset::cohen_forcing();
        assert!(!cohen.collapses_cardinals);
        assert!(cohen.adds_real);
        let ind = cohen.independence_of_ch();
        assert!(ind.contains("Cohen"));
        let abs = cohen.generic_absoluteness();
        assert!(abs.contains("Shoenfield"));
        let col = ForcingPoset::collapsing_forcing("κ");
        assert!(col.collapses_cardinals);
    }
    #[test]
    fn test_martins_axiom() {
        let ma = MartinsAxiom::ma_not_ch();
        assert!(ma.ccc_forcing);
        assert!(ma.consequence_count() > 0);
        let cons = ma.consistency();
        assert!(cons.contains("Solovay"));
    }
    #[test]
    fn test_pfa() {
        let pfa = ProperForcingAxiom::pfa();
        assert!(pfa.implies_not_ch);
        assert!(pfa.implies_ma);
        let woodin = pfa.woodin_provable_consequences();
        assert!(woodin.contains("Woodin"));
    }
}