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::{
    Algebra, AlgebraHomomorphism, BirkhoffVariety, BooleanAlgebra, Clone, CongruenceLattice,
    CongruenceRelation, DirectProductDecomposition, DistributiveLattice, EquationalLaw,
    FreeAlgebra, KnuthBendixCompletion, MaltsevCondition, OpSymbol, QuasiVariety, RewriteRule,
    Signature, SimpleRewriteSystem, Term, TermAlgebra, TermRewriteSystem, Variety,
};

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)
}
/// Algebra : Signature → Carrier → Type
///
/// An algebra over a signature Σ with carrier set A.
pub fn algebra_ty() -> Expr {
    arrow(cst("Signature"), arrow(type0(), type0()))
}
/// Homomorphism between algebras.
///
/// HomAlg A B : Algebra Σ A → Algebra Σ B → Type
pub fn homomorphism_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            impl_pi(
                "B",
                type0(),
                arrow(
                    app2(cst("Algebra"), bvar(2), bvar(1)),
                    arrow(app2(cst("Algebra"), bvar(3), bvar(0)), type0()),
                ),
            ),
        ),
    )
}
/// Congruence relation on an algebra.
///
/// Congruence A : Algebra Σ A → (A → A → Prop) → Prop
pub fn congruence_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app2(cst("Algebra"), bvar(1), bvar(0)),
                arrow(arrow(bvar(1), arrow(bvar(2), prop())), prop()),
            ),
        ),
    )
}
/// Quotient algebra A/θ.
///
/// QuotientAlgebra A θ : Algebra Σ (Quotient A θ)
pub fn quotient_algebra_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app2(cst("Algebra"), bvar(1), bvar(0)),
                arrow(arrow(bvar(1), arrow(bvar(2), prop())), cst("Algebra")),
            ),
        ),
    )
}
/// Free algebra on generators.
///
/// FreeAlgebra Σ X : Algebra Σ (FreeCarrier Σ X)
pub fn free_algebra_ty() -> Expr {
    arrow(cst("Signature"), arrow(type0(), cst("Algebra")))
}
/// Variety: equationally defined class of algebras.
///
/// Variety Σ : List (Equation Σ) → (∀ A, Algebra Σ A → Prop)
pub fn variety_ty() -> Expr {
    arrow(
        cst("Signature"),
        arrow(
            app(cst("List"), cst("Equation")),
            arrow(
                impl_pi(
                    "A",
                    type0(),
                    arrow(app2(cst("Algebra"), bvar(1), bvar(0)), prop()),
                ),
                prop(),
            ),
        ),
    )
}
/// TermAlgebra : Signature → Type → Type
///
/// The term algebra (word algebra) over Σ freely generated by X.
pub fn term_algebra_ty() -> Expr {
    arrow(cst("Signature"), arrow(type0(), type0()))
}
/// AlgSubalgebra : Algebra Σ A → (A → Prop) → Prop
///
/// Predicate that a subset of A forms a subalgebra.
pub fn subalgebra_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app2(cst("Algebra"), bvar(1), bvar(0)),
                arrow(arrow(bvar(1), prop()), prop()),
            ),
        ),
    )
}
/// DirectProduct : Algebra Σ A → Algebra Σ B → Algebra Σ (A × B)
pub fn direct_product_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            impl_pi(
                "B",
                type0(),
                arrow(
                    app2(cst("Algebra"), bvar(2), bvar(1)),
                    arrow(
                        app2(cst("Algebra"), bvar(3), bvar(0)),
                        app2(cst("Algebra"), bvar(4), app2(cst("Prod"), bvar(2), bvar(1))),
                    ),
                ),
            ),
        ),
    )
}
/// SubdirectProduct : characterises subdirectly irreducible algebras.
///
/// SubdirectProduct Σ I (A : I → Type) : (∀ i, Algebra Σ (A i)) → Prop
pub fn subdirect_product_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "I",
            type0(),
            arrow(
                pi(
                    BinderInfo::Default,
                    "i",
                    bvar(0),
                    app2(cst("Algebra"), bvar(2), app(cst("Carrier"), bvar(0))),
                ),
                prop(),
            ),
        ),
    )
}
/// SubdirectlyIrreducible : an algebra is subdirectly irreducible
/// iff every subdirect representation contains an injective factor.
pub fn subdirectly_irreducible_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(app2(cst("Algebra"), bvar(1), bvar(0)), prop()),
        ),
    )
}
/// BirkhoffSubdirect : every algebra embeds subdirectly into subdirectly irreducible algebras.
pub fn birkhoff_subdirect_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app2(cst("Algebra"), bvar(1), bvar(0)),
                app2(
                    cst("HasSubdirectEmbedding"),
                    bvar(1),
                    cst("SubdirectlyIrreducible"),
                ),
            ),
        ),
    )
}
/// Quasivariety : defined by quasi-identities (Horn clauses).
///
/// QuasiVariety Σ : List (QuasiEquation Σ) → (∀ A, Algebra Σ A → Prop)
pub fn quasivariety_ty() -> Expr {
    arrow(
        cst("Signature"),
        arrow(
            app(cst("List"), cst("QuasiEquation")),
            arrow(
                impl_pi(
                    "A",
                    type0(),
                    arrow(app2(cst("Algebra"), bvar(1), bvar(0)), prop()),
                ),
                prop(),
            ),
        ),
    )
}
/// Malcev condition: a variety has a Malcev term iff it is congruence-permutable.
///
/// MalcevCondition Σ : (∃ p : Term Σ 3, satisfies_malcev p) → IsCongruencePermutable Σ
pub fn malcev_condition_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            app2(cst("ExistsTerm"), bvar(0), cst("SatisfiesMalcev")),
            app(cst("IsCongruencePermutable"), bvar(1)),
        ),
    )
}
/// VarietyJoin : the join of two varieties in the lattice of varieties.
///
/// VarietyJoin V W : Variety Σ
pub fn variety_join_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            app(cst("Variety"), bvar(0)),
            arrow(app(cst("Variety"), bvar(1)), app(cst("Variety"), bvar(2))),
        ),
    )
}
/// VarietyMeet : the meet of two varieties in the lattice of varieties.
///
/// VarietyMeet V W : Variety Σ
pub fn variety_meet_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            app(cst("Variety"), bvar(0)),
            arrow(app(cst("Variety"), bvar(1)), app(cst("Variety"), bvar(2))),
        ),
    )
}
/// FiniteBasis : a variety has a finite equational basis.
///
/// FiniteBasis V : Prop
pub fn finite_basis_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(app(cst("Variety"), bvar(0)), prop()),
    )
}
/// OmegaComplete : an algebra is ω-complete (colimits of ω-chains exist).
pub fn omega_complete_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(app2(cst("Algebra"), bvar(1), bvar(0)), prop()),
        ),
    )
}
/// Clone : a clone is a set of operations closed under composition and containing projections.
///
/// Clone A : (List (NaryOp A)) → Prop
pub fn clone_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(app(cst("List"), app(cst("NaryOp"), bvar(0))), prop()),
    )
}
/// MinimalClone : a clone generated by a single essential operation.
pub fn minimal_clone_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(
            app(cst("Clone"), bvar(0)),
            arrow(app(cst("NaryOp"), bvar(1)), prop()),
        ),
    )
}
/// Polymorphism : a polymorphism of a relational structure.
///
/// Polymorphism n R : (NaryOp A n) → Prop
pub fn polymorphism_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        impl_pi(
            "n",
            cst("Nat"),
            arrow(
                app(cst("Relation"), bvar(1)),
                arrow(app2(cst("NaryOp"), bvar(2), bvar(1)), prop()),
            ),
        ),
    )
}
/// PostLattice : the lattice of Boolean clones (Post's completeness theorem).
///
/// PostLatticeElement : BoolClone → Prop
pub fn post_lattice_ty() -> Expr {
    arrow(cst("BoolClone"), prop())
}
/// InfinitaryAlgebra : an algebra allowing operations of infinite arity.
///
/// InfinitaryAlgebra Σ_inf A : Type
pub fn infinitary_algebra_ty() -> Expr {
    arrow(cst("InfinitarySignature"), arrow(type0(), type0()))
}
/// ManySortedSignature : a signature over multiple sorts.
///
/// ManySortedSignature : (Sort → Type) → Type
pub fn many_sorted_signature_ty() -> Expr {
    arrow(arrow(cst("Sort"), type0()), type0())
}
/// ManySortedAlgebra : an algebra over a many-sorted signature.
///
/// ManySortedAlgebra Σ (A : Sort → Type) : Type
pub fn many_sorted_algebra_ty() -> Expr {
    impl_pi(
        "S",
        type0(),
        arrow(
            app(cst("ManySortedSignature"), bvar(0)),
            arrow(arrow(bvar(1), type0()), type0()),
        ),
    )
}
/// HeterogeneousAlgebra : generalization with distinct input/output sorts.
///
/// HeterogeneousAlgebra Σ A : Type
pub fn heterogeneous_algebra_ty() -> Expr {
    arrow(
        cst("HeterogeneousSignature"),
        arrow(arrow(cst("Sort"), type0()), type0()),
    )
}
/// TermRewriteSystem : a set of rewrite rules l → r.
///
/// TRS Σ : List (Rule Σ) → Type
pub fn trs_ty() -> Expr {
    arrow(
        cst("Signature"),
        arrow(app(cst("List"), cst("Rule")), type0()),
    )
}
/// Confluence (Church-Rosser): if s →* t₁ and s →* t₂, then ∃ u, t₁ →* u ∧ t₂ →* u.
///
/// IsConfluent R : Prop
pub fn confluence_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(arrow(bvar(0), arrow(bvar(1), prop())), prop()),
    )
}
/// Termination : a rewrite system is terminating (strongly normalising).
///
/// IsTerminating R : Prop
pub fn termination_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(arrow(bvar(0), arrow(bvar(1), prop())), prop()),
    )
}
/// LocalConfluence : if s → t₁ and s → t₂, then ∃ u, t₁ →* u ∧ t₂ →* u.
pub fn local_confluence_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(arrow(bvar(0), arrow(bvar(1), prop())), prop()),
    )
}
/// NewmanLemma : termination + local confluence ⟹ confluence.
///
/// NewmanLemma R : IsTerminating R → IsLocallyConfluent R → IsConfluent R
pub fn newman_lemma_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        impl_pi(
            "R",
            arrow(bvar(0), arrow(bvar(1), prop())),
            arrow(
                app(cst("IsTerminating"), bvar(0)),
                arrow(
                    app(cst("IsLocallyConfluent"), bvar(1)),
                    app(cst("IsConfluent"), bvar(2)),
                ),
            ),
        ),
    )
}
/// CriticalPair : a critical pair of two rewrite rules.
///
/// CriticalPair l₁ r₁ l₂ r₂ : Prop
pub fn critical_pair_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            app(cst("Rule"), bvar(0)),
            arrow(app(cst("Rule"), bvar(1)), type0()),
        ),
    )
}
/// KnuthBendixCompletion : completes a TRS to a confluent one (if termination order exists).
///
/// KBComplete R : Option (ConfluentTRS Σ)
pub fn knuth_bendix_completion_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            app2(cst("TRS"), bvar(0), app(cst("List"), cst("Rule"))),
            app(cst("Option"), app(cst("ConfluentTRS"), bvar(1))),
        ),
    )
}
/// ChurchRosser : the Church-Rosser property (equivalent to confluence for ARS).
///
/// ChurchRosser R : Prop ↔ IsConfluent R
pub fn church_rosser_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        impl_pi(
            "R",
            arrow(bvar(0), arrow(bvar(1), prop())),
            arrow(
                app(cst("ChurchRosser"), bvar(0)),
                app(cst("IsConfluent"), bvar(1)),
            ),
        ),
    )
}
/// Congruence lattice: the set of all congruences on an algebra forms a lattice.
///
/// CongruenceLattice A : Lattice
pub fn congruence_lattice_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(app2(cst("Algebra"), bvar(1), bvar(0)), cst("Lattice")),
        ),
    )
}
/// ThirdIsomorphismTheorem : (A/α)/(β/α) ≅ A/β for α ≤ β.
pub fn isomorphism_theorem_3_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app2(cst("Algebra"), bvar(1), bvar(0)),
                arrow(
                    app(cst("Congruence"), bvar(0)),
                    arrow(
                        app(cst("Congruence"), bvar(1)),
                        arrow(
                            app2(cst("CongLeq"), bvar(1), bvar(0)),
                            app2(
                                cst("AlgIso"),
                                app(cst("QuotOfQuot"), bvar(3)),
                                app(cst("QuotDirect"), bvar(4)),
                            ),
                        ),
                    ),
                ),
            ),
        ),
    )
}
/// ReductSystem : an abstract reduction system (ARS) without signature.
///
/// ReductSystem A : (A → A → Prop) → Type
pub fn reduct_system_ty() -> Expr {
    impl_pi(
        "A",
        type0(),
        arrow(arrow(bvar(0), arrow(bvar(1), prop())), type0()),
    )
}
/// Birkhoff's HSP Theorem.
///
/// A class K of algebras is a variety iff it is closed under
/// homomorphic images (H), subalgebras (S), and products (P).
pub fn birkhoff_theorem_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        arrow(
            arrow(
                impl_pi(
                    "A",
                    type0(),
                    arrow(app2(cst("Algebra"), bvar(1), bvar(0)), prop()),
                ),
                prop(),
            ),
            arrow(app(cst("IsVariety"), bvar(0)), app(cst("IsHSP"), bvar(1))),
        ),
    )
}
/// First Isomorphism Theorem: A/ker(φ) ≅ Im(φ).
pub fn isomorphism_theorem_1_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            impl_pi(
                "B",
                type0(),
                arrow(
                    app3(cst("Hom"), bvar(2), bvar(1), bvar(0)),
                    app2(
                        cst("AlgIso"),
                        app(cst("QuotByKer"), bvar(0)),
                        app(cst("Image"), bvar(1)),
                    ),
                ),
            ),
        ),
    )
}
/// Second Isomorphism Theorem: (A/α)/(β/α) ≅ A/β.
pub fn isomorphism_theorem_2_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "A",
            type0(),
            arrow(
                app(cst("Congruence"), bvar(0)),
                arrow(
                    app(cst("Congruence"), bvar(1)),
                    arrow(
                        app2(cst("CongLeq"), bvar(1), bvar(0)),
                        app2(
                            cst("AlgIso"),
                            app(cst("QuotQuot"), bvar(2)),
                            app(cst("QuotDirect"), bvar(3)),
                        ),
                    ),
                ),
            ),
        ),
    )
}
/// Universal Property of Free Algebras.
///
/// For any algebra B and map f : X → B, there exists a unique
/// homomorphism φ : Free(Σ, X) → B extending f.
pub fn free_algebra_universal_ty() -> Expr {
    impl_pi(
        "Σ",
        cst("Signature"),
        impl_pi(
            "X",
            type0(),
            impl_pi(
                "B",
                type0(),
                arrow(
                    app2(cst("Algebra"), bvar(2), bvar(0)),
                    arrow(
                        arrow(bvar(2), bvar(1)),
                        app3(
                            cst("ExistsUniqueHom"),
                            app2(cst("FreeAlgebra"), bvar(4), bvar(3)),
                            bvar(1),
                            bvar(2),
                        ),
                    ),
                ),
            ),
        ),
    )
}
/// Build the variety of groups: associativity, identity, inverse.
pub fn group_variety() -> Variety {
    let mut sig = Signature::new();
    sig.add_op(OpSymbol::new("mul", 2));
    sig.add_op(OpSymbol::new("e", 0));
    sig.add_op(OpSymbol::new("inv", 1));
    let mut v = Variety::new("Group", sig);
    v.add_law(EquationalLaw::new(
        "assoc",
        "mul(mul(x,y),z)",
        "mul(x,mul(y,z))",
    ));
    v.add_law(EquationalLaw::new("identity", "mul(e,x)", "x"));
    v.add_law(EquationalLaw::new("inverse", "mul(inv(x),x)", "e"));
    v
}
/// Build the variety of rings: additive group laws plus multiplicativity.
pub fn ring_variety() -> Variety {
    let mut sig = Signature::new();
    sig.add_op(OpSymbol::new("add", 2));
    sig.add_op(OpSymbol::new("mul", 2));
    sig.add_op(OpSymbol::new("zero", 0));
    sig.add_op(OpSymbol::new("neg", 1));
    sig.add_op(OpSymbol::new("one", 0));
    let mut v = Variety::new("Ring", sig);
    v.add_law(EquationalLaw::new(
        "add_assoc",
        "add(add(x,y),z)",
        "add(x,add(y,z))",
    ));
    v.add_law(EquationalLaw::new("add_comm", "add(x,y)", "add(y,x)"));
    v.add_law(EquationalLaw::new("identity", "add(zero,x)", "x"));
    v.add_law(EquationalLaw::new("inverse", "add(neg(x),x)", "zero"));
    v.add_law(EquationalLaw::new(
        "mul_assoc",
        "mul(mul(x,y),z)",
        "mul(x,mul(y,z))",
    ));
    v.add_law(EquationalLaw::new(
        "distrib_l",
        "mul(x,add(y,z))",
        "add(mul(x,y),mul(x,z))",
    ));
    v.add_law(EquationalLaw::new(
        "distrib_r",
        "mul(add(y,z),x)",
        "add(mul(y,x),mul(z,x))",
    ));
    v
}
/// Build the variety of lattices: meet and join with absorption laws.
pub fn lattice_variety() -> Variety {
    let mut sig = Signature::new();
    sig.add_op(OpSymbol::new("meet", 2));
    sig.add_op(OpSymbol::new("join", 2));
    let mut v = Variety::new("Lattice", sig);
    v.add_law(EquationalLaw::new(
        "meet_assoc",
        "meet(meet(x,y),z)",
        "meet(x,meet(y,z))",
    ));
    v.add_law(EquationalLaw::new(
        "join_assoc",
        "join(join(x,y),z)",
        "join(x,join(y,z))",
    ));
    v.add_law(EquationalLaw::new("meet_comm", "meet(x,y)", "meet(y,x)"));
    v.add_law(EquationalLaw::new("join_comm", "join(x,y)", "join(y,x)"));
    v.add_law(EquationalLaw::new("absorb_meet", "meet(x,join(x,y))", "x"));
    v.add_law(EquationalLaw::new("absorb_join", "join(x,meet(x,y))", "x"));
    v
}
/// Build an OxiLean environment containing the universal algebra axioms.
pub fn build_universal_algebra_env() -> Environment {
    let mut env = Environment::new();
    let _ = env.add(Declaration::Axiom {
        name: Name::str("Signature"),
        univ_params: vec![],
        ty: type0(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("Algebra"),
        univ_params: vec![],
        ty: algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("AlgebraHom"),
        univ_params: vec![],
        ty: homomorphism_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("AlgebraCongruence"),
        univ_params: vec![],
        ty: congruence_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("QuotientAlgebra"),
        univ_params: vec![],
        ty: quotient_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("FreeAlgebra"),
        univ_params: vec![],
        ty: free_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("AlgebraVariety"),
        univ_params: vec![],
        ty: variety_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("BirkhoffHSP"),
        univ_params: vec![],
        ty: birkhoff_theorem_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsoThm1"),
        univ_params: vec![],
        ty: isomorphism_theorem_1_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsoThm2"),
        univ_params: vec![],
        ty: isomorphism_theorem_2_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("FreeAlgebraUniversal"),
        univ_params: vec![],
        ty: free_algebra_universal_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("TermAlgebra"),
        univ_params: vec![],
        ty: term_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("AlgSubalgebra"),
        univ_params: vec![],
        ty: subalgebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("DirectProduct"),
        univ_params: vec![],
        ty: direct_product_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("SubdirectProduct"),
        univ_params: vec![],
        ty: subdirect_product_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("SubdirectlyIrreducible"),
        univ_params: vec![],
        ty: subdirectly_irreducible_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("BirkhoffSubdirect"),
        univ_params: vec![],
        ty: birkhoff_subdirect_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("QuasiVariety"),
        univ_params: vec![],
        ty: quasivariety_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("MalcevCondition"),
        univ_params: vec![],
        ty: malcev_condition_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("VarietyJoin"),
        univ_params: vec![],
        ty: variety_join_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("VarietyMeet"),
        univ_params: vec![],
        ty: variety_meet_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("FiniteBasis"),
        univ_params: vec![],
        ty: finite_basis_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("OmegaComplete"),
        univ_params: vec![],
        ty: omega_complete_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("AlgebraicClone"),
        univ_params: vec![],
        ty: clone_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("MinimalClone"),
        univ_params: vec![],
        ty: minimal_clone_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("Polymorphism"),
        univ_params: vec![],
        ty: polymorphism_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("PostLattice"),
        univ_params: vec![],
        ty: post_lattice_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("InfinitaryAlgebra"),
        univ_params: vec![],
        ty: infinitary_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("ManySortedSignature"),
        univ_params: vec![],
        ty: many_sorted_signature_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("ManySortedAlgebra"),
        univ_params: vec![],
        ty: many_sorted_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("HeterogeneousAlgebra"),
        univ_params: vec![],
        ty: heterogeneous_algebra_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("TermRewriteSystem"),
        univ_params: vec![],
        ty: trs_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsConfluent"),
        univ_params: vec![],
        ty: confluence_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsTerminating"),
        univ_params: vec![],
        ty: termination_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsLocallyConfluent"),
        univ_params: vec![],
        ty: local_confluence_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("NewmanLemma"),
        univ_params: vec![],
        ty: newman_lemma_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("CriticalPair"),
        univ_params: vec![],
        ty: critical_pair_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("KnuthBendixCompletion"),
        univ_params: vec![],
        ty: knuth_bendix_completion_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("ChurchRosser"),
        univ_params: vec![],
        ty: church_rosser_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("CongruenceLattice"),
        univ_params: vec![],
        ty: congruence_lattice_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("IsoThm3"),
        univ_params: vec![],
        ty: isomorphism_theorem_3_ty(),
    });
    let _ = env.add(Declaration::Axiom {
        name: Name::str("ReductSystem"),
        univ_params: vec![],
        ty: reduct_system_ty(),
    });
    env
}
#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn test_op_symbol_constant() {
        let op = OpSymbol::new("e", 0);
        assert!(op.is_constant());
        assert_eq!(op.name, "e");
    }
    #[test]
    fn test_op_symbol_binary() {
        let op = OpSymbol::new("mul", 2);
        assert!(!op.is_constant());
        assert_eq!(op.arity, 2);
    }
    #[test]
    fn test_signature_has_op() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("mul", 2));
        sig.add_op(OpSymbol::new("e", 0));
        assert!(sig.has_op("mul"));
        assert!(sig.has_op("e"));
        assert!(!sig.has_op("inv"));
    }
    #[test]
    fn test_signature_arities() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("f", 3));
        sig.add_op(OpSymbol::new("c", 0));
        let arities = sig.arities();
        assert_eq!(arities.len(), 2);
        assert!(arities.contains(&("f".to_string(), 3)));
        assert!(arities.contains(&("c".to_string(), 0)));
    }
    #[test]
    fn test_algebra_closed() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("f", 2));
        let mut alg = Algebra::new(3, sig);
        alg.define_op("f", vec![vec![0, 1, 2], vec![1, 2, 0], vec![2, 0, 1]]);
        assert!(alg.is_closed());
    }
    #[test]
    fn test_algebra_apply_op() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("add", 2));
        let mut alg = Algebra::new(4, sig);
        alg.define_op(
            "add",
            vec![
                vec![0, 1, 2, 3],
                vec![1, 2, 3, 0],
                vec![2, 3, 0, 1],
                vec![3, 0, 1, 2],
            ],
        );
        assert_eq!(alg.apply_op("add", &[2, 3]), Some(1));
        assert_eq!(alg.apply_op("add", &[0, 0]), Some(0));
    }
    #[test]
    fn test_equational_law_trivial() {
        let trivial = EquationalLaw::new("refl", "x", "x");
        assert!(trivial.is_trivial());
        let non_trivial = EquationalLaw::new("comm", "f(x,y)", "f(y,x)");
        assert!(!non_trivial.is_trivial());
    }
    #[test]
    fn test_group_variety() {
        let v = group_variety();
        assert!(v.is_group_variety());
        assert!(v.includes_law("assoc"));
        assert!(v.includes_law("identity"));
        assert!(v.includes_law("inverse"));
        assert!(!v.includes_law("distrib"));
    }
    #[test]
    fn test_build_universal_algebra_env() {
        let env = build_universal_algebra_env();
        assert!(env.get(&Name::str("Signature")).is_some());
        assert!(env.get(&Name::str("Algebra")).is_some());
        assert!(env.get(&Name::str("FreeAlgebra")).is_some());
        assert!(env.get(&Name::str("BirkhoffHSP")).is_some());
        assert!(env.get(&Name::str("TermAlgebra")).is_some());
        assert!(env.get(&Name::str("DirectProduct")).is_some());
        assert!(env.get(&Name::str("SubdirectlyIrreducible")).is_some());
        assert!(env.get(&Name::str("QuasiVariety")).is_some());
        assert!(env.get(&Name::str("MalcevCondition")).is_some());
        assert!(env.get(&Name::str("VarietyJoin")).is_some());
        assert!(env.get(&Name::str("VarietyMeet")).is_some());
        assert!(env.get(&Name::str("FiniteBasis")).is_some());
        assert!(env.get(&Name::str("OmegaComplete")).is_some());
        assert!(env.get(&Name::str("AlgebraicClone")).is_some());
        assert!(env.get(&Name::str("MinimalClone")).is_some());
        assert!(env.get(&Name::str("Polymorphism")).is_some());
        assert!(env.get(&Name::str("PostLattice")).is_some());
        assert!(env.get(&Name::str("InfinitaryAlgebra")).is_some());
        assert!(env.get(&Name::str("ManySortedSignature")).is_some());
        assert!(env.get(&Name::str("ManySortedAlgebra")).is_some());
        assert!(env.get(&Name::str("HeterogeneousAlgebra")).is_some());
        assert!(env.get(&Name::str("TermRewriteSystem")).is_some());
        assert!(env.get(&Name::str("IsConfluent")).is_some());
        assert!(env.get(&Name::str("IsTerminating")).is_some());
        assert!(env.get(&Name::str("IsLocallyConfluent")).is_some());
        assert!(env.get(&Name::str("NewmanLemma")).is_some());
        assert!(env.get(&Name::str("CriticalPair")).is_some());
        assert!(env.get(&Name::str("KnuthBendixCompletion")).is_some());
        assert!(env.get(&Name::str("ChurchRosser")).is_some());
        assert!(env.get(&Name::str("CongruenceLattice")).is_some());
        assert!(env.get(&Name::str("IsoThm3")).is_some());
        assert!(env.get(&Name::str("ReductSystem")).is_some());
    }
    #[test]
    fn test_term_var() {
        let t = Term::var(3);
        assert_eq!(t, Term::Var(3));
        assert_eq!(t.depth(), 0);
        assert_eq!(t.variables(), vec![3]);
    }
    #[test]
    fn test_term_constant() {
        let t = Term::constant("zero");
        assert_eq!(t.depth(), 1);
        assert!(t.variables().is_empty());
    }
    #[test]
    fn test_term_apply_and_depth() {
        let inner = Term::apply("g", vec![Term::var(0)]);
        let outer = Term::apply("f", vec![inner, Term::var(1)]);
        assert_eq!(outer.depth(), 2);
        let vars = outer.variables();
        assert!(vars.contains(&0));
        assert!(vars.contains(&1));
    }
    #[test]
    fn test_term_subst() {
        let t = Term::apply("f", vec![Term::var(0), Term::var(1)]);
        let c = Term::constant("c");
        let result = t.subst(0, &c);
        assert_eq!(
            result,
            Term::apply("f", vec![Term::constant("c"), Term::var(1)])
        );
    }
    #[test]
    fn test_term_eval_mod2() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("add", 2));
        let mut alg = Algebra::new(2, sig);
        alg.define_op("add", vec![vec![0, 1], vec![1, 0]]);
        let t = Term::apply("add", vec![Term::var(0), Term::var(1)]);
        assert_eq!(t.eval(&alg, &[1, 1]), Some(0));
        assert_eq!(t.eval(&alg, &[0, 1]), Some(1));
    }
    #[test]
    fn test_term_algebra_well_formed() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("f", 2));
        sig.add_op(OpSymbol::new("c", 0));
        let ta = TermAlgebra::new(sig, 2);
        let good = Term::apply("f", vec![Term::var(0), Term::constant("c")]);
        assert!(ta.is_well_formed(&good));
        let bad = Term::apply("f", vec![Term::var(0)]);
        assert!(!ta.is_well_formed(&bad));
    }
    #[test]
    fn test_term_algebra_free_term() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("mul", 2));
        let ta = TermAlgebra::new(sig, 3);
        let ft = ta.free_term("mul").expect("free_term should succeed");
        assert_eq!(ft, Term::apply("mul", vec![Term::var(0), Term::var(1)]));
    }
    #[test]
    fn test_congruence_discrete() {
        let mut cong = CongruenceRelation::discrete(4);
        assert!(!cong.are_equiv(0, 1));
        assert!(cong.are_equiv(2, 2));
        assert_eq!(cong.num_classes(), 4);
    }
    #[test]
    fn test_congruence_total() {
        let mut cong = CongruenceRelation::total(3);
        assert!(cong.are_equiv(0, 1));
        assert!(cong.are_equiv(1, 2));
        assert_eq!(cong.num_classes(), 1);
    }
    #[test]
    fn test_congruence_merge_and_classes() {
        let mut cong = CongruenceRelation::discrete(5);
        cong.merge(0, 1);
        cong.merge(2, 3);
        let classes = cong.classes();
        assert_eq!(classes.len(), 3);
        assert!(classes.iter().any(|c| c == &vec![0, 1]));
        assert!(classes.iter().any(|c| c == &vec![2, 3]));
        assert!(classes.iter().any(|c| c == &vec![4]));
    }
    #[test]
    fn test_rewrite_rule_match() {
        let lhs = Term::apply("f", vec![Term::var(0), Term::var(0)]);
        let rhs = Term::apply("g", vec![Term::var(0)]);
        let rule = RewriteRule::new("idem", lhs, rhs);
        let t = Term::apply("f", vec![Term::constant("c"), Term::constant("c")]);
        let result = rule.try_apply_top(&t);
        assert_eq!(result, Some(Term::apply("g", vec![Term::constant("c")])));
    }
    #[test]
    fn test_rewrite_rule_no_match() {
        let lhs = Term::apply("f", vec![Term::var(0), Term::var(0)]);
        let rhs = Term::apply("g", vec![Term::var(0)]);
        let rule = RewriteRule::new("idem", lhs, rhs);
        let t = Term::apply("f", vec![Term::constant("a"), Term::constant("b")]);
        assert!(rule.try_apply_top(&t).is_none());
    }
    #[test]
    fn test_trs_normalize() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("f", 1));
        sig.add_op(OpSymbol::new("c", 0));
        let mut trs = TermRewriteSystem::new(sig);
        let lhs = Term::apply("f", vec![Term::apply("f", vec![Term::var(0)])]);
        let rhs = Term::var(0);
        trs.add_rule(RewriteRule::new("invol", lhs, rhs));
        let t = Term::apply(
            "f",
            vec![Term::apply(
                "f",
                vec![Term::apply(
                    "f",
                    vec![Term::apply("f", vec![Term::constant("c")])],
                )],
            )],
        );
        let nf = trs.normalize(&t, 100);
        assert_eq!(nf, Term::constant("c"));
    }
    #[test]
    fn test_kb_trivial_equation() {
        let sig = Signature::new();
        let eqs = vec![(Term::constant("c"), Term::constant("c"))];
        let mut kb = KnuthBendixCompletion::new(sig, eqs, 100);
        assert!(kb.run());
        assert!(kb.result_rules().is_empty());
    }
    #[test]
    fn test_kb_single_rule() {
        let mut sig = Signature::new();
        sig.add_op(OpSymbol::new("f", 1));
        let lhs = Term::apply("f", vec![Term::apply("f", vec![Term::var(0)])]);
        let rhs = Term::var(0);
        let eqs = vec![(lhs, rhs)];
        let mut kb = KnuthBendixCompletion::new(sig, eqs, 100);
        let success = kb.run();
        assert!(success || !kb.result_rules().is_empty());
    }
}
/// Summary of Birkhoff's HSP theorem.
#[allow(dead_code)]
pub fn birkhoff_hsp_theorem() -> &'static str {
    "A class K of algebras is a variety (defined by equations) \
     if and only if K is closed under homomorphic images (H), \
     subalgebras (S), and direct products (P)."
}
/// Summary of key results in universal algebra.
#[allow(dead_code)]
pub fn universal_algebra_key_results() -> Vec<(&'static str, &'static str)> {
    vec![
        ("Birkhoff", "HSP theorem characterizes varieties"),
        ("Maltsev", "Congruence permutability <-> Maltsev term"),
        ("Jonsson", "Congruence distributivity <-> Jonsson terms"),
        ("Tarski", "Relation algebras and representability"),
        (
            "McKenzie",
            "Decidability of the equational theory of finite algebras",
        ),
        (
            "Post",
            "Lattice of clones on a 2-element set = Post lattice",
        ),
        ("Szabo", "Finite basis problem for finite algebras"),
        (
            "Baker-Pixley",
            "Finite algebras: equational basis implications",
        ),
        (
            "Freese-McKenzie",
            "Commutator theory in congruence modular varieties",
        ),
        (
            "Hobby-McKenzie",
            "Tame congruence theory for finite algebras",
        ),
    ]
}
#[cfg(test)]
mod ua_ext_tests {
    use super::*;
    #[test]
    fn test_birkhoff_variety_groups() {
        let g = BirkhoffVariety::groups();
        assert!(!g.axioms.is_empty());
        assert!(g.is_equationally_definable());
        assert!(g.closed_under_hsp());
    }
    #[test]
    fn test_free_algebra() {
        let fa = FreeAlgebra::new("Groups", 2);
        assert!(!fa.universal_property().is_empty());
    }
    #[test]
    fn test_maltsev_condition() {
        let mc = MaltsevCondition::congruence_permutability();
        assert!(!mc.equations.is_empty());
        assert!(mc.characterizes_variety());
    }
    #[test]
    fn test_key_results_nonempty() {
        let results = universal_algebra_key_results();
        assert!(!results.is_empty());
    }
    #[test]
    fn test_birkhoff_hsp() {
        let stmt = birkhoff_hsp_theorem();
        assert!(stmt.contains("variety"));
    }
}
#[cfg(test)]
mod ua_trs_tests {
    use super::*;
    #[test]
    fn test_trs_complete() {
        let mut trs = SimpleRewriteSystem::new("GroupNF");
        trs.add_rule("x * e", "x");
        trs.add_rule("e * x", "x");
        trs.is_confluent = true;
        trs.is_terminating = true;
        assert!(trs.is_complete());
        assert!(trs.normal_form_unique());
    }
    #[test]
    fn test_homomorphism() {
        let hom = AlgebraHomomorphism::new("Z", "Z/2Z", false, true);
        assert!(!hom.is_isomorphism());
        assert!(!hom.is_embedding());
    }
    #[test]
    fn test_direct_product() {
        let dp = DirectProductDecomposition::new("Z6", vec!["Z2", "Z3"]);
        assert!(dp.is_nontrivial());
    }
}
#[cfg(test)]
mod ba_tests {
    use super::*;
    #[test]
    fn test_boolean_algebra() {
        let ba = BooleanAlgebra::finite(3);
        assert!(ba.is_atomic);
        assert!(ba.is_representable());
        assert!(!ba.stone_representation().is_empty());
    }
    #[test]
    fn test_distributive_lattice() {
        let dl = DistributiveLattice::new("C(3)", true);
        assert!(!dl.birkhoff_representation().is_empty());
    }
}