litex/verify/verify_builtin_rules/

in_fact_builtin.rs

use crate::infer::obj_eligible_for_known_objs_in_fn_sets;
use crate::prelude::*;
use crate::verify::{
    number_is_in_n, number_is_in_n_pos, number_is_in_q_neg, number_is_in_q_nz, number_is_in_q_pos,
    number_is_in_r_neg, number_is_in_r_nz, number_is_in_r_pos, number_is_in_z, number_is_in_z_neg,
    number_is_in_z_nz, verify_equality_by_builtin_rules::verify_equality_by_they_are_the_same,
    verify_number_in_standard_set::is_integer_after_simplification, VerifyState,
};
fn number_in_set_verified_by_builtin_rules_result(in_fact: &InFact, reason: &str) -> StmtResult {
    StmtResult::FactualStmtSuccess(
        FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
            in_fact.clone().into(),
            reason.to_string(),
            Vec::new(),
        ),
    )
}

fn not_in_fact_verified_by_builtin_rules_result(
    not_in_fact: &NotInFact,
    reason: &str,
) -> StmtResult {
    StmtResult::FactualStmtSuccess(
        FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
            not_in_fact.clone().into(),
            reason.to_string(),
            Vec::new(),
        ),
    )
}

fn arithmetic_obj_in_r_verified_by_builtin_rules_result(in_fact: &InFact) -> StmtResult {
    StmtResult::FactualStmtSuccess(
        FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
            in_fact.clone().into(),
            "arithmetic expression is in R".to_string(),
            Vec::new(),
        ),
    )
}

fn builtin_in_fact_result_for_evaluated_number_in_standard_set(
    in_fact: &InFact,
    evaluated_number: &Number,
    standard_set: &StandardSet,
) -> StmtResult {
    match standard_set {
        StandardSet::R => number_in_set_verified_by_builtin_rules_result(in_fact, "number in R"),
        StandardSet::RPos => {
            if number_is_in_r_pos(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in R_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::RNeg => {
            if number_is_in_r_neg(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in R_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::RNz => {
            if number_is_in_r_nz(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in R_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::Q => number_in_set_verified_by_builtin_rules_result(in_fact, "number in Q"),
        StandardSet::QPos => {
            if number_is_in_q_pos(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Q_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::QNeg => {
            if number_is_in_q_neg(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Q_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::QNz => {
            if number_is_in_q_nz(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Q_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::Z => {
            if number_is_in_z(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Z")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::ZNeg => {
            if number_is_in_z_neg(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Z_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::ZNz => {
            if number_is_in_z_nz(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in Z_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::N => {
            if number_is_in_n(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in N")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::NPos => {
            if number_is_in_n_pos(evaluated_number) {
                number_in_set_verified_by_builtin_rules_result(in_fact, "number in N_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
    }
}

fn builtin_not_in_fact_result_for_evaluated_number_in_standard_set(
    not_in_fact: &NotInFact,
    evaluated_number: &Number,
    standard_set: &StandardSet,
) -> StmtResult {
    match standard_set {
        StandardSet::R | StandardSet::Q => StmtResult::StmtUnknown(StmtUnknown::new()),
        StandardSet::RPos => {
            if !number_is_in_r_pos(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in R_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::RNeg => {
            if !number_is_in_r_neg(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in R_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::RNz => {
            if !number_is_in_r_nz(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in R_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::QPos => {
            if !number_is_in_q_pos(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Q_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::QNeg => {
            if !number_is_in_q_neg(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Q_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::QNz => {
            if !number_is_in_q_nz(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Q_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::Z => {
            if !number_is_in_z(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Z")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::ZNeg => {
            if !number_is_in_z_neg(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Z_neg")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::ZNz => {
            if !number_is_in_z_nz(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in Z_nz")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::N => {
            if !number_is_in_n(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in N")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
        StandardSet::NPos => {
            if !number_is_in_n_pos(evaluated_number) {
                not_in_fact_verified_by_builtin_rules_result(not_in_fact, "number not in N_pos")
            } else {
                StmtResult::StmtUnknown(StmtUnknown::new())
            }
        }
    }
}

impl Runtime {
    pub fn verify_not_in_fact_with_builtin_rules(
        &mut self,
        not_in_fact: &NotInFact,
        _verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Obj::StandardSet(standard_set) = &not_in_fact.set {
            if !matches!(&not_in_fact.element, Obj::Number(_)) {
                if let Some(evaluated_number) =
                    not_in_fact.element.evaluate_to_normalized_decimal_number()
                {
                    return Ok(
                        builtin_not_in_fact_result_for_evaluated_number_in_standard_set(
                            not_in_fact,
                            &evaluated_number,
                            standard_set,
                        ),
                    );
                }
            }
        }
        match (&not_in_fact.element, &not_in_fact.set) {
            (Obj::Number(num), Obj::StandardSet(standard_set)) => Ok(
                builtin_not_in_fact_result_for_evaluated_number_in_standard_set(
                    not_in_fact,
                    num,
                    standard_set,
                ),
            ),
            _ => Ok((StmtUnknown::new()).into()),
        }
    }

    fn maybe_verify_in_fact_max_min_pair_closed_standard_set(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<Option<StmtResult>, RuntimeError> {
        let (left, right, set) = match (&in_fact.element, &in_fact.set) {
            (Obj::Max(m), Obj::StandardSet(s)) => (m.left.as_ref(), m.right.as_ref(), s.clone()),
            (Obj::Min(m), Obj::StandardSet(s)) => (m.left.as_ref(), m.right.as_ref(), s.clone()),
            _ => return Ok(None),
        };
        if !matches!(
            set,
            StandardSet::RPos
                | StandardSet::QPos
                | StandardSet::RNeg
                | StandardSet::QNeg
                | StandardSet::ZNeg
                | StandardSet::N
                | StandardSet::NPos
        ) {
            return Ok(None);
        }
        let reason = format!("max/min: both operands in {}", set);
        let set_obj: Obj = set.into();
        let lf = in_fact.line_file.clone();
        for operand in [left, right] {
            let f: AtomicFact = InFact::new(operand.clone(), set_obj.clone(), lf.clone()).into();
            if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&f, verify_state)? {
                return Ok(Some((StmtUnknown::new()).into()));
            }
        }
        Ok(Some(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            reason.as_str(),
        )))
    }

    // Finite `sum` / `product` over a closed integer range: if the object is well-defined, its value
    // is a real (used e.g. for `+` on real-valued operands).
    fn verify_in_fact_sum_or_product_in_r(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
        reason: &str,
    ) -> Result<StmtResult, RuntimeError> {
        if self
            .verify_obj_well_defined_and_store_cache(&in_fact.element, verify_state)
            .is_ok()
        {
            Ok(number_in_set_verified_by_builtin_rules_result(
                in_fact, reason,
            ))
        } else {
            Ok((StmtUnknown::new()).into())
        }
    }

    fn iterated_op_func_ret_set(&self, func: &Obj) -> Option<Obj> {
        match func {
            Obj::AnonymousFn(anon) => Some((*anon.body.ret_set).clone()),
            Obj::FnObj(fn_obj) if fn_obj.body.is_empty() => match fn_obj.head.as_ref() {
                FnObjHead::AnonymousFnLiteral(anon) => Some((*anon.body.ret_set).clone()),
                _ => {
                    let function_name_obj: Obj = (*fn_obj.head).clone().into();
                    self.get_object_in_fn_set_or_restrict(&function_name_obj)
                        .map(|fn_set_body| (*fn_set_body.ret_set).clone())
                }
            },
            _ => self
                .get_object_in_fn_set_or_restrict(func)
                .map(|fn_set_body| (*fn_set_body.ret_set).clone()),
        }
    }

    // `sum(start, end, f)` / `product(start, end, f)` in `Z` when the iterand's declared return
    // set is `Z` or `N_pos` (positive naturals are integers) and the whole iterated object is
    // well-defined on the integer interval.
    // Example: `sum(1, n, 'Z(x){x}) $in Z`, `product(1, a, 'N_pos(x){x}) $in Z`.
    fn verify_in_fact_sum_or_product_in_z_by_iterand_ret_set(
        &mut self,
        in_fact: &InFact,
        func: &Obj,
        verify_state: &VerifyState,
        op: &str,
    ) -> Result<StmtResult, RuntimeError> {
        if self
            .verify_obj_well_defined_and_store_cache(&in_fact.element, verify_state)
            .is_err()
        {
            return Ok((StmtUnknown::new()).into());
        }
        let Some(ret_set) = self.iterated_op_func_ret_set(func) else {
            return Ok((StmtUnknown::new()).into());
        };
        let z_obj: Obj = StandardSet::Z.into();
        let n_pos_obj: Obj = StandardSet::NPos.into();
        let reason = if verify_equality_by_they_are_the_same(&ret_set, &z_obj) {
            format!("{op}: iterand return set is Z")
        } else if verify_equality_by_they_are_the_same(&ret_set, &n_pos_obj) {
            format!("{op}: iterand return set is N_pos (subset of Z)")
        } else {
            return Ok((StmtUnknown::new()).into());
        };
        Ok(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            reason.as_str(),
        ))
    }

    // `sum(start, end, f)` / `product(start, end, f)` in `Q` when the iterand's declared return
    // set is `Q` and the whole iterated object is well-defined on the integer interval.
    fn verify_in_fact_sum_or_product_in_q_by_iterand_ret_set(
        &mut self,
        in_fact: &InFact,
        func: &Obj,
        verify_state: &VerifyState,
        op: &str,
    ) -> Result<StmtResult, RuntimeError> {
        if self
            .verify_obj_well_defined_and_store_cache(&in_fact.element, verify_state)
            .is_err()
        {
            return Ok((StmtUnknown::new()).into());
        }
        let Some(ret_set) = self.iterated_op_func_ret_set(func) else {
            return Ok((StmtUnknown::new()).into());
        };
        let q_obj: Obj = StandardSet::Q.into();
        if !verify_equality_by_they_are_the_same(&ret_set, &q_obj) {
            return Ok((StmtUnknown::new()).into());
        }
        let reason = format!("{op}: iterand return set is Q");
        Ok(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            reason.as_str(),
        ))
    }

    // `sum(start, end, f)` / `product(start, end, f)` in `N_pos` when the iterand's declared
    // return set is `N_pos` and the whole iterated object is well-defined on the integer interval.
    // Example: `product(1, a, 'N_pos(x){x}) $in N_pos`.
    fn verify_in_fact_sum_or_product_in_n_pos_by_iterand_ret_set(
        &mut self,
        in_fact: &InFact,
        func: &Obj,
        verify_state: &VerifyState,
        op: &str,
    ) -> Result<StmtResult, RuntimeError> {
        if self
            .verify_obj_well_defined_and_store_cache(&in_fact.element, verify_state)
            .is_err()
        {
            return Ok((StmtUnknown::new()).into());
        }
        let Some(ret_set) = self.iterated_op_func_ret_set(func) else {
            return Ok((StmtUnknown::new()).into());
        };
        let n_pos_obj: Obj = StandardSet::NPos.into();
        if !verify_equality_by_they_are_the_same(&ret_set, &n_pos_obj) {
            return Ok((StmtUnknown::new()).into());
        }
        let reason = format!("{op}: iterand return set is N_pos");
        Ok(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            reason.as_str(),
        ))
    }

    /// `f(args) $in S` when `S` agrees with the head's typing return set and the application is
    /// well-defined in the current environment (e.g. domain facts already assumed).
    fn verify_in_fact_fn_application_in_typed_return_set(
        &mut self,
        fn_obj: &FnObj,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let typed_ret = match fn_obj.head.as_ref() {
            FnObjHead::AnonymousFnLiteral(a) => (*a.body.ret_set).clone(),
            _ => {
                let head_obj: Obj = (*fn_obj.head.clone()).into();
                let Some(fn_set) = self.get_cloned_object_in_fn_set(&head_obj) else {
                    return Ok((StmtUnknown::new()).into());
                };
                (*fn_set.ret_set).clone()
            }
        };
        let target = &in_fact.set;
        let ret_matches = verify_equality_by_they_are_the_same(target, &typed_ret)
            || self
                .verify_equal_fact(
                    &EqualFact::new(target.clone(), typed_ret.clone(), in_fact.line_file.clone()),
                    verify_state,
                )?
                .is_true();
        if !ret_matches {
            return Ok((StmtUnknown::new()).into());
        }
        if self
            .verify_obj_well_defined_and_store_cache(&Obj::FnObj(fn_obj.clone()), verify_state)
            .is_err()
        {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(
            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "fn application in declared return set (well-defined under typing)".to_string(),
                Vec::new(),
            )
            .into(),
        )
    }

    pub fn verify_in_fact_with_builtin_rules(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Obj::StandardSet(standard_set) = &in_fact.set {
            if !matches!(&in_fact.element, Obj::Number(_)) {
                if let Some(evaluated_number) =
                    in_fact.element.evaluate_to_normalized_decimal_number()
                {
                    let evaluation_membership_result =
                        builtin_in_fact_result_for_evaluated_number_in_standard_set(
                            in_fact,
                            &evaluated_number,
                            standard_set,
                        );
                    return Ok(evaluation_membership_result);
                }
            }
        }
        if let Some(result) =
            self.maybe_verify_in_fact_max_min_pair_closed_standard_set(in_fact, verify_state)?
        {
            return Ok(result);
        }
        match (&in_fact.element, &in_fact.set) {
            (Obj::Tuple(tuple), Obj::Cart(cart)) => {
                return self.verify_in_fact_by_left_is_tuple_right_is_cart(
                    in_fact,
                    tuple,
                    cart,
                    verify_state,
                );
            }
            (Obj::Number(num), Obj::StandardSet(standard_set)) => {
                Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                    in_fact,
                    num,
                    standard_set,
                ))
            }
            (Obj::Sum(sum), Obj::StandardSet(StandardSet::NPos)) => self
                .verify_in_fact_sum_or_product_in_n_pos_by_iterand_ret_set(
                    in_fact,
                    sum.func.as_ref(),
                    verify_state,
                    "sum",
                ),
            (Obj::Product(product), Obj::StandardSet(StandardSet::NPos)) => self
                .verify_in_fact_sum_or_product_in_n_pos_by_iterand_ret_set(
                    in_fact,
                    product.func.as_ref(),
                    verify_state,
                    "product",
                ),
            (Obj::Add(add), Obj::StandardSet(StandardSet::N)) => {
                self.verify_in_fact_add_in_n_from_summands_in_n(in_fact, add, verify_state)
            }
            (Obj::Mul(mul), Obj::StandardSet(StandardSet::N)) => {
                self.verify_in_fact_mul_in_n_from_factors_in_n(in_fact, mul, verify_state)
            }
            (Obj::Add(add), Obj::StandardSet(StandardSet::NPos)) => {
                self.verify_in_fact_add_in_n_pos_from_n_pos_and_n(in_fact, add, verify_state)
            }
            (Obj::Mul(mul), Obj::StandardSet(StandardSet::NPos)) => {
                self.verify_in_fact_mul_in_n_pos_from_factors_in_n_pos(in_fact, mul, verify_state)
            }
            (_, Obj::StandardSet(StandardSet::NPos)) => {
                self.verify_in_fact_n_pos_by_zero_less_and_in_z_or_n(in_fact, verify_state)
            }
            (_, Obj::ClosedRange(closed_range)) => self
                .verify_in_fact_closed_range_by_order_bounds(in_fact, closed_range, verify_state),
            (_, Obj::Range(range)) => {
                self.verify_in_fact_open_range_by_order_bounds(in_fact, range, verify_state)
            }
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Mod(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_)
                | Obj::Abs(_),
                Obj::StandardSet(StandardSet::Z),
            ) => self.verify_in_fact_arithmetic_expression_in_z(in_fact, verify_state),
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Div(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_)
                | Obj::Abs(_),
                Obj::StandardSet(StandardSet::Q),
            ) => self.verify_in_fact_arithmetic_expression_in_q(in_fact, verify_state),
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Div(_)
                | Obj::Mod(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_),
                Obj::StandardSet(StandardSet::RNeg),
            ) => self.verify_in_fact_arithmetic_expression_in_standard_negative_set(
                in_fact,
                verify_state,
                StandardSet::RNeg,
            ),
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Div(_)
                | Obj::Mod(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_),
                Obj::StandardSet(StandardSet::QNeg),
            ) => self.verify_in_fact_arithmetic_expression_in_standard_negative_set(
                in_fact,
                verify_state,
                StandardSet::QNeg,
            ),
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Div(_)
                | Obj::Mod(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_),
                Obj::StandardSet(StandardSet::ZNeg),
            ) => self.verify_in_fact_arithmetic_expression_in_standard_negative_set(
                in_fact,
                verify_state,
                StandardSet::ZNeg,
            ),
            (
                Obj::Add(_)
                | Obj::Sub(_)
                | Obj::Mul(_)
                | Obj::Div(_)
                | Obj::Mod(_)
                | Obj::Pow(_)
                | Obj::Max(_)
                | Obj::Min(_)
                | Obj::Abs(_)
                | Obj::Log(_),
                Obj::StandardSet(StandardSet::R),
            ) => Ok(arithmetic_obj_in_r_verified_by_builtin_rules_result(
                in_fact,
            )),
            (Obj::Sum(_), Obj::StandardSet(StandardSet::R)) => self
                .verify_in_fact_sum_or_product_in_r(
                    in_fact,
                    verify_state,
                    "sum: well-defined on an integer range, in R",
                ),
            (Obj::Product(_), Obj::StandardSet(StandardSet::R)) => self
                .verify_in_fact_sum_or_product_in_r(
                    in_fact,
                    verify_state,
                    "product: well-defined on an integer range, in R",
                ),
            (Obj::Sum(sum), Obj::StandardSet(StandardSet::Z)) => self
                .verify_in_fact_sum_or_product_in_z_by_iterand_ret_set(
                    in_fact,
                    sum.func.as_ref(),
                    verify_state,
                    "sum",
                ),
            (Obj::Product(product), Obj::StandardSet(StandardSet::Z)) => self
                .verify_in_fact_sum_or_product_in_z_by_iterand_ret_set(
                    in_fact,
                    product.func.as_ref(),
                    verify_state,
                    "product",
                ),
            (Obj::Sum(sum), Obj::StandardSet(StandardSet::Q)) => self
                .verify_in_fact_sum_or_product_in_q_by_iterand_ret_set(
                    in_fact,
                    sum.func.as_ref(),
                    verify_state,
                    "sum",
                ),
            (Obj::Product(product), Obj::StandardSet(StandardSet::Q)) => self
                .verify_in_fact_sum_or_product_in_q_by_iterand_ret_set(
                    in_fact,
                    product.func.as_ref(),
                    verify_state,
                    "product",
                ),
            (Obj::ListSet(list_set), Obj::PowerSet(power_set)) => self
                .verify_in_fact_list_set_in_power_set_defines_membership(
                    in_fact,
                    list_set,
                    power_set,
                    verify_state,
                ),
            (Obj::SetBuilder(set_builder), Obj::PowerSet(power_set)) => self
                .verify_in_fact_set_builder_in_power_set_via_param_subset(
                    in_fact,
                    set_builder,
                    power_set,
                    verify_state,
                ),
            (Obj::Choose(choose), where_is_obj) => {
                let choose_from = choose.set.clone();
                let equal_fact = EqualFact::new(
                    *choose_from,
                    where_is_obj.clone(),
                    in_fact.line_file.clone(),
                )
                .into();
                let equal_fact_verify_result =
                    self.verify_atomic_fact(&equal_fact, verify_state)?;
                if equal_fact_verify_result.is_true() {
                    return Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                            in_fact.clone().into(),
                            "By ZFC, we can choose an element from a nonempty set whose elements are all nonempty.".to_string(),
                            Vec::new(),
                        )).into());
                } else {
                    return Ok((StmtUnknown::new()).into());
                }
            }
            (_, Obj::ListSet(list_set)) => self.verify_in_fact_by_equal_to_one_element_in_list_set(
                in_fact,
                list_set,
                verify_state,
            ),
            (Obj::AnonymousFn(anon), Obj::FnSet(expected_fn_set)) => self
                .verify_in_fact_anonymous_fn_signature_matches_fn_set(
                    anon,
                    expected_fn_set,
                    in_fact,
                    verify_state,
                ),
            (element, Obj::FnSet(expected_fn_set))
                if obj_eligible_for_known_objs_in_fn_sets(element) =>
            {
                self.verify_in_fact_element_in_fn_set_by_stored_definition(
                    element,
                    expected_fn_set,
                    in_fact,
                )
            }
            (_, Obj::FamilyObj(family_ty)) => {
                self.verify_obj_satisfies_family(in_fact.element.clone(), family_ty, verify_state)
            }
            (Obj::FiniteSeqListObj(list), Obj::FiniteSeqSet(fs)) => {
                let lf = in_fact.line_file.clone();
                let len_obj: Obj = Number::new(list.objs.len().to_string()).into();
                let len_eq_n: AtomicFact =
                    EqualFact::new(len_obj, (*fs.n).clone(), lf.clone()).into();
                if !self.verify_atomic_fact(&len_eq_n, verify_state)?.is_true() {
                    return Ok((StmtUnknown::new()).into());
                }
                for o in list.objs.iter() {
                    let f: AtomicFact =
                        InFact::new((**o).clone(), (*fs.set).clone(), lf.clone()).into();
                    if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
                        &f,
                        verify_state,
                    )? {
                        return Ok((StmtUnknown::new()).into());
                    }
                }
                Ok(number_in_set_verified_by_builtin_rules_result(
                    in_fact,
                    "finite_seq list: length equals n and each entry in co-domain",
                ))
            }
            (Obj::MatrixListObj(list), Obj::MatrixSet(ms)) => {
                let lf = in_fact.line_file.clone();
                let n_rows_obj: Obj = Number::new(list.rows.len().to_string()).into();
                let row_eq: AtomicFact =
                    EqualFact::new(n_rows_obj, (*ms.row_len).clone(), lf.clone()).into();
                if !self.verify_atomic_fact(&row_eq, verify_state)?.is_true() {
                    return Ok((StmtUnknown::new()).into());
                }
                for row in list.rows.iter() {
                    let n_col_obj: Obj = Number::new(row.len().to_string()).into();
                    let col_eq: AtomicFact =
                        EqualFact::new(n_col_obj, (*ms.col_len).clone(), lf.clone()).into();
                    if !self.verify_atomic_fact(&col_eq, verify_state)?.is_true() {
                        return Ok((StmtUnknown::new()).into());
                    }
                    for o in row.iter() {
                        let f: AtomicFact =
                            InFact::new((**o).clone(), (*ms.set).clone(), lf.clone()).into();
                        if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
                            &f,
                            verify_state,
                        )? {
                            return Ok((StmtUnknown::new()).into());
                        }
                    }
                }
                Ok(number_in_set_verified_by_builtin_rules_result(
                    in_fact,
                    "matrix literal: shape matches matrix(...) and each entry in co-domain",
                ))
            }
            (_, Obj::FiniteSeqSet(fs)) => {
                let fn_set = self.finite_seq_set_to_fn_set(fs, in_fact.line_file.clone());
                let expanded = InFact::new(
                    in_fact.element.clone(),
                    fn_set.into(),
                    in_fact.line_file.clone(),
                );
                self.verify_atomic_fact(&expanded.into(), verify_state)
            }
            (_, Obj::SeqSet(ss)) => {
                let fn_set = self.seq_set_to_fn_set(ss, in_fact.line_file.clone());
                let expanded = InFact::new(
                    in_fact.element.clone(),
                    fn_set.into(),
                    in_fact.line_file.clone(),
                );
                self.verify_atomic_fact(&expanded.into(), verify_state)
            }
            (_, Obj::MatrixSet(ms)) => {
                let fn_set = self.matrix_set_to_fn_set(ms, in_fact.line_file.clone());
                let expanded = InFact::new(
                    in_fact.element.clone(),
                    fn_set.into(),
                    in_fact.line_file.clone(),
                );
                self.verify_atomic_fact(&expanded.into(), verify_state)
            }
            (_, target_set_obj) => {
                if let Obj::FnObj(fn_obj) = &in_fact.element {
                    let fn_try = self.verify_in_fact_fn_application_in_typed_return_set(
                        fn_obj,
                        in_fact,
                        verify_state,
                    )?;
                    if fn_try.is_true() {
                        return Ok(fn_try);
                    }
                }
                self.verify_in_fact_by_known_standard_subset_membership(in_fact, target_set_obj)
            }
        }
    }

    // `a + b $in N` when `a $in N` and `b $in N` (closure under addition).
    // Example: `forall a, b N: a + b $in N`.
    fn verify_in_fact_add_in_n_from_summands_in_n(
        &mut self,
        in_fact: &InFact,
        add: &Add,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::N,
            ));
        }
        let n: Obj = StandardSet::N.into();
        let lf = in_fact.line_file.clone();
        let f_left: AtomicFact =
            InFact::new(add.left.as_ref().clone(), n.clone(), lf.clone()).into();
        let f_right: AtomicFact = InFact::new(add.right.as_ref().clone(), n, lf.clone()).into();
        let r_left = self.verify_non_equational_atomic_fact(&f_left, verify_state, true)?;
        if !r_left.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        let r_right = self.verify_non_equational_atomic_fact(&f_right, verify_state, true)?;
        if !r_right.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(
            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "N: a + b from a in N and b in N".to_string(),
                vec![r_left, r_right],
            )
            .into(),
        )
    }

    // `a * b $in N` when `a $in N` and `b $in N` (closure under multiplication).
    // Example: `forall a, b N: a * b $in N`.
    fn verify_in_fact_mul_in_n_from_factors_in_n(
        &mut self,
        in_fact: &InFact,
        mul: &Mul,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::N,
            ));
        }
        let n: Obj = StandardSet::N.into();
        let lf = in_fact.line_file.clone();
        let f_left: AtomicFact =
            InFact::new(mul.left.as_ref().clone(), n.clone(), lf.clone()).into();
        let f_right: AtomicFact = InFact::new(mul.right.as_ref().clone(), n, lf.clone()).into();
        let r_left = self.verify_non_equational_atomic_fact(&f_left, verify_state, true)?;
        if !r_left.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        let r_right = self.verify_non_equational_atomic_fact(&f_right, verify_state, true)?;
        if !r_right.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(
            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "N: a * b from a in N and b in N".to_string(),
                vec![r_left, r_right],
            )
            .into(),
        )
    }

    // `a + b $in N_pos` when both summands are in `N_pos`, or one summand is in
    // `N_pos` and the other is in `N`.
    // Example: `forall a, b N_pos: a + b $in N_pos`.
    fn verify_in_fact_add_in_n_pos_from_n_pos_and_n(
        &mut self,
        in_fact: &InFact,
        add: &Add,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::NPos,
            ));
        }
        let n_pos: Obj = StandardSet::NPos.into();
        let n: Obj = StandardSet::N.into();
        let lf = in_fact.line_file.clone();

        let left_n_pos: AtomicFact =
            InFact::new(add.left.as_ref().clone(), n_pos.clone(), lf.clone()).into();
        let right_n_pos_for_pair: AtomicFact =
            InFact::new(add.right.as_ref().clone(), n_pos.clone(), lf.clone()).into();
        let r_left_n_pos_for_pair =
            self.verify_non_equational_atomic_fact(&left_n_pos, verify_state, true)?;
        if r_left_n_pos_for_pair.is_true() {
            let r_right_n_pos_for_pair =
                self.verify_non_equational_atomic_fact(&right_n_pos_for_pair, verify_state, true)?;
            if r_right_n_pos_for_pair.is_true() {
                return Ok(
                    FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                        in_fact.clone().into(),
                        "N_pos: a + b from a in N_pos and b in N_pos".to_string(),
                        vec![r_left_n_pos_for_pair, r_right_n_pos_for_pair],
                    )
                    .into(),
                );
            }
        }

        let right_n: AtomicFact =
            InFact::new(add.right.as_ref().clone(), n.clone(), lf.clone()).into();
        let r_left_n_pos =
            self.verify_non_equational_atomic_fact(&left_n_pos, verify_state, true)?;
        if r_left_n_pos.is_true() {
            let r_right_n = self.verify_non_equational_atomic_fact(&right_n, verify_state, true)?;
            if r_right_n.is_true() {
                return Ok(
                    FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                        in_fact.clone().into(),
                        "N_pos: a + b from a in N_pos and b in N".to_string(),
                        vec![r_left_n_pos, r_right_n],
                    )
                    .into(),
                );
            }
        }

        let left_n: AtomicFact =
            InFact::new(add.left.as_ref().clone(), n.clone(), lf.clone()).into();
        let right_n_pos: AtomicFact =
            InFact::new(add.right.as_ref().clone(), n_pos, lf.clone()).into();
        let r_left_n = self.verify_non_equational_atomic_fact(&left_n, verify_state, true)?;
        if !r_left_n.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        let r_right_n_pos =
            self.verify_non_equational_atomic_fact(&right_n_pos, verify_state, true)?;
        if !r_right_n_pos.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(
            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "N_pos: a + b from a in N and b in N_pos".to_string(),
                vec![r_left_n, r_right_n_pos],
            )
            .into(),
        )
    }

    // `a * b $in N_pos` when `a $in N_pos` and `b $in N_pos` (positive naturals are closed under multiplication).
    // Example: `forall a, b N_pos: a * b $in N_pos`.
    fn verify_in_fact_mul_in_n_pos_from_factors_in_n_pos(
        &mut self,
        in_fact: &InFact,
        mul: &Mul,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::NPos,
            ));
        }
        let n_pos: Obj = StandardSet::NPos.into();
        let lf = in_fact.line_file.clone();
        let f_left: AtomicFact =
            InFact::new(mul.left.as_ref().clone(), n_pos.clone(), lf.clone()).into();
        let f_right: AtomicFact = InFact::new(mul.right.as_ref().clone(), n_pos, lf.clone()).into();
        let r_left = self.verify_non_equational_atomic_fact(&f_left, verify_state, true)?;
        if !r_left.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        let r_right = self.verify_non_equational_atomic_fact(&f_right, verify_state, true)?;
        if !r_right.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(
            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "N_pos: a * b from a in N_pos and b in N_pos".to_string(),
                vec![r_left, r_right],
            )
            .into(),
        )
    }

    // `N_pos` = positive integers: from `0 < x` and (`x $in Z` or `x $in N`).
    fn verify_in_fact_n_pos_by_zero_less_and_in_z_or_n(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let elem = &in_fact.element;
        let lf = in_fact.line_file.clone();
        let zero: Obj = Number::new("0".to_string()).into();
        let zero_lt_elem = LessFact::new(zero, elem.clone(), lf.clone()).into();
        if !self
            .non_equational_atomic_fact_holds_by_full_verify_pipeline(&zero_lt_elem, verify_state)?
        {
            return Ok((StmtUnknown::new()).into());
        }

        let in_z = InFact::new(elem.clone(), StandardSet::Z.into(), lf.clone()).into();
        if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&in_z, verify_state)? {
            return Ok(number_in_set_verified_by_builtin_rules_result(
                in_fact,
                "N_pos: 0 < x and x in Z",
            ));
        }

        let in_n = InFact::new(elem.clone(), StandardSet::N.into(), lf.clone()).into();
        if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&in_n, verify_state)? {
            return Ok(number_in_set_verified_by_builtin_rules_result(
                in_fact,
                "N_pos: 0 < x and x in N",
            ));
        }

        Ok((StmtUnknown::new()).into())
    }

    fn verify_in_fact_closed_range_by_order_bounds(
        &mut self,
        in_fact: &InFact,
        closed_range: &ClosedRange,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let elem = &in_fact.element;
        let lf = in_fact.line_file.clone();
        if !self.order_lower_bound_from_literals(
            elem,
            closed_range.start.as_ref(),
            &lf,
            verify_state,
        )? {
            return Ok((StmtUnknown::new()).into());
        }
        if !self.order_upper_bound_closed_from_literals(
            elem,
            closed_range.end.as_ref(),
            &lf,
            verify_state,
        )? {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            "in closed_range: a <= i and i <= b",
        ))
    }

    fn verify_in_fact_open_range_by_order_bounds(
        &mut self,
        in_fact: &InFact,
        range: &Range,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let elem = &in_fact.element;
        let lf = in_fact.line_file.clone();
        if !self.order_lower_bound_from_literals(elem, range.start.as_ref(), &lf, verify_state)? {
            return Ok((StmtUnknown::new()).into());
        }
        if !self.order_upper_bound_open_from_literals(
            elem,
            range.end.as_ref(),
            &lf,
            verify_state,
        )? {
            return Ok((StmtUnknown::new()).into());
        }
        Ok(number_in_set_verified_by_builtin_rules_result(
            in_fact,
            "in range: a <= i and i < b",
        ))
    }

    // When `x $in Z` and endpoints are integer literals: `lo <= x` iff `lo - 1 < x` (discrete lower).
    // Example: dom `1 < i` with `i $in Z` proves the lower side of `i $in range(2, 6)` / `closed_range(2, 5)`.
    fn order_lower_bound_from_literals(
        &mut self,
        elem: &Obj,
        lower: &Obj,
        lf: &LineFile,
        verify_state: &VerifyState,
    ) -> Result<bool, RuntimeError> {
        let weak: AtomicFact = LessEqualFact::new(lower.clone(), elem.clone(), lf.clone()).into();
        if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&weak, verify_state)? {
            return Ok(true);
        }
        let in_z: AtomicFact = InFact::new(elem.clone(), StandardSet::Z.into(), lf.clone()).into();
        if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&in_z, verify_state)? {
            return Ok(false);
        }
        let Some(lower_num) = self.resolve_obj_to_number_resolved(lower) else {
            return Ok(false);
        };
        if !is_integer_after_simplification(&lower_num) {
            return Ok(false);
        }
        let pred = Obj::Sub(Sub::new(lower.clone(), Number::new("1".to_string()).into()));
        let Some(pred_n) = pred.evaluate_to_normalized_decimal_number() else {
            return Ok(false);
        };
        let strict: AtomicFact = LessFact::new(pred_n.into(), elem.clone(), lf.clone()).into();
        self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&strict, verify_state)
    }

    // When `x $in Z` and `hi` is an integer literal: `x < hi` iff `x <= hi - 1`.
    // Example: `i <= 5` and `i $in Z` gives the upper side of `i $in range(2, 6)`.
    fn order_upper_bound_open_from_literals(
        &mut self,
        elem: &Obj,
        upper: &Obj,
        lf: &LineFile,
        verify_state: &VerifyState,
    ) -> Result<bool, RuntimeError> {
        let strict: AtomicFact = LessFact::new(elem.clone(), upper.clone(), lf.clone()).into();
        if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&strict, verify_state)? {
            return Ok(true);
        }
        let in_z: AtomicFact = InFact::new(elem.clone(), StandardSet::Z.into(), lf.clone()).into();
        if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&in_z, verify_state)? {
            return Ok(false);
        }
        let Some(upper_num) = self.resolve_obj_to_number_resolved(upper) else {
            return Ok(false);
        };
        if !is_integer_after_simplification(&upper_num) {
            return Ok(false);
        }
        let upper_minus_one =
            Obj::Sub(Sub::new(upper.clone(), Number::new("1".to_string()).into()));
        let Some(um) = upper_minus_one.evaluate_to_normalized_decimal_number() else {
            return Ok(false);
        };
        let weak: AtomicFact = LessEqualFact::new(elem.clone(), um.into(), lf.clone()).into();
        self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&weak, verify_state)
    }

    // When `x $in Z` and `hi` is an integer literal: `x <= hi` iff `x < hi + 1`.
    fn order_upper_bound_closed_from_literals(
        &mut self,
        elem: &Obj,
        upper: &Obj,
        lf: &LineFile,
        verify_state: &VerifyState,
    ) -> Result<bool, RuntimeError> {
        let weak: AtomicFact = LessEqualFact::new(elem.clone(), upper.clone(), lf.clone()).into();
        if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&weak, verify_state)? {
            return Ok(true);
        }
        let in_z: AtomicFact = InFact::new(elem.clone(), StandardSet::Z.into(), lf.clone()).into();
        if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&in_z, verify_state)? {
            return Ok(false);
        }
        let Some(upper_num) = self.resolve_obj_to_number_resolved(upper) else {
            return Ok(false);
        };
        if !is_integer_after_simplification(&upper_num) {
            return Ok(false);
        }
        let hi_plus_one = Obj::Add(Add::new(upper.clone(), Number::new("1".to_string()).into()));
        let Some(hp) = hi_plus_one.evaluate_to_normalized_decimal_number() else {
            return Ok(false);
        };
        let strict: AtomicFact = LessFact::new(elem.clone(), hp.into(), lf.clone()).into();
        self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&strict, verify_state)
    }

    // Builtin closure of `Z` under `+`, `-`, `*`, `mod`, and `^` when direct operands are in `Z`
    // (`Pow` checks `base` and `exponent`; if the power normalizes to a decimal, the numeric branch above applies).
    fn verify_in_fact_arithmetic_expression_in_z(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::Z,
            ));
        }
        let z_obj: Obj = StandardSet::Z.into();
        let lf = in_fact.line_file.clone();

        let mut require_in_z = |o: &Obj| -> Result<bool, RuntimeError> {
            let f = InFact::new(o.clone(), z_obj.clone(), lf.clone()).into();
            self.non_equational_atomic_fact_holds_by_full_verify_pipeline(&f, verify_state)
        };

        let ok = match &in_fact.element {
            Obj::Add(a) => require_in_z(&a.left)? && require_in_z(&a.right)?,
            Obj::Sub(s) => require_in_z(&s.left)? && require_in_z(&s.right)?,
            Obj::Mul(m) => require_in_z(&m.left)? && require_in_z(&m.right)?,
            Obj::Mod(m) => require_in_z(&m.left)? && require_in_z(&m.right)?,
            Obj::Pow(p) => require_in_z(&p.base)? && require_in_z(&p.exponent)?,
            Obj::Max(m) => require_in_z(&m.left)? && require_in_z(&m.right)?,
            Obj::Min(m) => require_in_z(&m.left)? && require_in_z(&m.right)?,
            Obj::Abs(a) => require_in_z(a.arg.as_ref())?,
            _ => false,
        };

        if !ok {
            return Ok((StmtUnknown::new()).into());
        }

        Ok(
            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "Z closure: operands in Z".to_string(),
                Vec::new(),
            ))
            .into(),
        )
    }

    // Builtin closure of `Q` under `+`, `-`, `*`, `/` when both operands are in `Q`. For `^`, require
    // `base` in `Q` and `exponent` in `Z` (rational base with integer exponent stays in `Q`).
    fn verify_in_fact_arithmetic_expression_in_q(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &StandardSet::Q,
            ));
        }
        let q_obj: Obj = StandardSet::Q.into();
        let z_obj: Obj = StandardSet::Z.into();
        let lf = in_fact.line_file.clone();

        let in_q = |slf: &mut Self, o: &Obj| -> Result<bool, RuntimeError> {
            let f = InFact::new(o.clone(), q_obj.clone(), lf.clone()).into();
            slf.non_equational_atomic_fact_holds_by_full_verify_pipeline(&f, verify_state)
        };
        let in_z = |slf: &mut Self, o: &Obj| -> Result<bool, RuntimeError> {
            let f = InFact::new(o.clone(), z_obj.clone(), lf.clone()).into();
            slf.non_equational_atomic_fact_holds_by_full_verify_pipeline(&f, verify_state)
        };

        let ok = match &in_fact.element {
            Obj::Add(a) => in_q(self, &a.left)? && in_q(self, &a.right)?,
            Obj::Sub(s) => in_q(self, &s.left)? && in_q(self, &s.right)?,
            Obj::Mul(m) => in_q(self, &m.left)? && in_q(self, &m.right)?,
            Obj::Div(d) => in_q(self, &d.left)? && in_q(self, &d.right)?,
            Obj::Pow(p) => in_q(self, &p.base)? && in_z(self, &p.exponent)?,
            Obj::Max(m) => in_q(self, &m.left)? && in_q(self, &m.right)?,
            Obj::Min(m) => in_q(self, &m.left)? && in_q(self, &m.right)?,
            Obj::Abs(a) => in_q(self, a.arg.as_ref())?,
            _ => false,
        };

        if !ok {
            return Ok((StmtUnknown::new()).into());
        }

        Ok(
            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "Q closure: +-*/ operands in Q; pow base in Q and exponent in Z".to_string(),
                Vec::new(),
            ))
            .into(),
        )
    }

    fn verify_in_fact_arithmetic_expression_in_standard_negative_set(
        &mut self,
        in_fact: &InFact,
        verify_state: &VerifyState,
        target_negative_standard_set: StandardSet,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(evaluated_number) = in_fact.element.evaluate_to_normalized_decimal_number() {
            return Ok(builtin_in_fact_result_for_evaluated_number_in_standard_set(
                in_fact,
                &evaluated_number,
                &target_negative_standard_set,
            ));
        }
        let mul = match &in_fact.element {
            Obj::Mul(mul) => mul,
            _ => return Ok((StmtUnknown::new()).into()),
        };
        let product_in_r_fact = InFact::new(
            in_fact.element.clone(),
            StandardSet::R.into(),
            in_fact.line_file.clone(),
        )
        .into();
        if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
            &product_in_r_fact,
            verify_state,
        )? {
            return Ok((StmtUnknown::new()).into());
        }
        if !self
            .mul_product_negative_when_factors_have_strict_opposite_sign_by_non_equational_verify(
                &mul.left,
                &mul.right,
                in_fact.line_file.clone(),
                verify_state,
            )?
        {
            return Ok((StmtUnknown::new()).into());
        }
        match target_negative_standard_set {
            StandardSet::RNeg => Ok(
                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    in_fact.clone().into(),
                    "mul_opposite_signs_product_in_R_neg".to_string(),
                    Vec::new(),
                ))
                .into(),
            ),
            StandardSet::QNeg => {
                let product_in_q_fact = InFact::new(
                    in_fact.element.clone(),
                    StandardSet::Q.into(),
                    in_fact.line_file.clone(),
                )
                .into();
                if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
                    &product_in_q_fact,
                    verify_state,
                )? {
                    Ok(
                        (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                            in_fact.clone().into(),
                            "mul_opposite_signs_product_in_Q_neg".to_string(),
                            Vec::new(),
                        ))
                        .into(),
                    )
                } else {
                    Ok((StmtUnknown::new()).into())
                }
            }
            StandardSet::ZNeg => {
                let product_in_z_fact = InFact::new(
                    in_fact.element.clone(),
                    StandardSet::Z.into(),
                    in_fact.line_file.clone(),
                )
                .into();
                if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
                    &product_in_z_fact,
                    verify_state,
                )? {
                    Ok(
                        (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                            in_fact.clone().into(),
                            "mul_opposite_signs_product_in_Z_neg".to_string(),
                            Vec::new(),
                        ))
                        .into(),
                    )
                } else {
                    Ok((StmtUnknown::new()).into())
                }
            }
            _ => Ok((StmtUnknown::new()).into()),
        }
    }

    // `{x S : …} ⊆ S` always. If `S ⊆ T` then `{x S : …} ⊆ T`, so `{x S : …} ∈ 𝒫(T)`.
    // Example: from `N $subset Z`, deduce `{x N: x = x} $in power_set(Z)` once that subset is known.
    fn verify_in_fact_set_builder_in_power_set_via_param_subset(
        &mut self,
        in_fact: &InFact,
        set_builder: &SetBuilder,
        power_set: &PowerSet,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let base_set = power_set.set.as_ref();
        let subset_fact = SubsetFact::new(
            (*set_builder.param_set).clone(),
            base_set.clone(),
            in_fact.line_file.clone(),
        )
        .into();
        let verify_subset_result = self.verify_atomic_fact(&subset_fact, verify_state)?;
        if !verify_subset_result.is_true() {
            return Ok((StmtUnknown::new()).into());
        }
        let mut infer_result = InferResult::new();
        match verify_subset_result {
            StmtResult::FactualStmtSuccess(factual_success) => {
                infer_result.new_infer_result_inside(factual_success.infers.clone());
            }
            StmtResult::NonFactualStmtSuccess(non_factual_success) => {
                infer_result.new_infer_result_inside(non_factual_success.infers.clone());
            }
            StmtResult::StmtUnknown(_) => {
                return Ok((StmtUnknown::new()).into());
            }
        }
        let stmt = in_fact.clone().into();
        infer_result.new_fact(&stmt);
        Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules(
            stmt,
            infer_result,
            VerifiedByResult::BuiltinRules(
                "set_builder in power_set: param_set subset of base implies builder defines a subset of base"
                    .to_string(),
            ),
        ))
        .into())
    }

    fn verify_in_fact_list_set_in_power_set_defines_membership(
        &mut self,
        in_fact: &InFact,
        list_set: &ListSet,
        power_set: &PowerSet,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let base_set = power_set.set.as_ref();
        let mut infer_result = InferResult::new();
        for element_box in list_set.list.iter() {
            let element_obj = *element_box.clone();
            let element_in_base_fact =
                InFact::new(element_obj, base_set.clone(), in_fact.line_file.clone()).into();
            let verify_one_element_result =
                self.verify_atomic_fact(&element_in_base_fact, verify_state)?;
            if !verify_one_element_result.is_true() {
                return Ok((StmtUnknown::new()).into());
            }
            match verify_one_element_result {
                StmtResult::FactualStmtSuccess(factual_success) => {
                    infer_result.new_infer_result_inside(factual_success.infers.clone());
                }
                StmtResult::NonFactualStmtSuccess(non_factual_success) => {
                    infer_result.new_infer_result_inside(non_factual_success.infers.clone());
                }
                StmtResult::StmtUnknown(_) => {
                    return Ok((StmtUnknown::new()).into());
                }
            }
        }
        let stmt = in_fact.clone().into();
        infer_result.new_fact(&stmt);
        Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules(
            stmt,
            infer_result,
            VerifiedByResult::BuiltinRules(
                "list_set in power_set: each element is in the base set".to_string(),
            ),
        ))
        .into())
    }

    fn verify_in_fact_by_equal_to_one_element_in_list_set(
        &mut self,
        in_fact: &InFact,
        list_set: &ListSet,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        for current_element_in_list_set in list_set.list.iter() {
            let equal_fact = EqualFact::new(
                in_fact.element.clone(),
                *current_element_in_list_set.clone(),
                in_fact.line_file.clone(),
            )
            .into();
            let equal_fact_verify_result = self.verify_atomic_fact(&equal_fact, verify_state)?;
            if equal_fact_verify_result.is_true() {
                return Ok(
                    (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                        in_fact.clone().into(),
                        format!(
                            "{} equals one element in list_set {}",
                            in_fact.element, in_fact.set
                        ),
                        Vec::new(),
                    ))
                    .into(),
                );
            }
        }
        Ok((StmtUnknown::new()).into())
    }

    fn standard_subset_set_objs_for_target_set(target_set_obj: &Obj) -> Option<Vec<Obj>> {
        match target_set_obj {
            Obj::StandardSet(StandardSet::NPos) => Some(vec![]),
            Obj::StandardSet(StandardSet::N) => Some(vec![StandardSet::NPos.into()]),
            Obj::StandardSet(StandardSet::ZNeg) => Some(vec![]),
            Obj::StandardSet(StandardSet::ZNz) => {
                Some(vec![StandardSet::NPos.into(), StandardSet::ZNeg.into()])
            }
            Obj::StandardSet(StandardSet::Z) => Some(vec![
                StandardSet::NPos.into(),
                StandardSet::N.into(),
                StandardSet::ZNeg.into(),
                StandardSet::ZNz.into(),
            ]),
            Obj::StandardSet(StandardSet::QPos) => Some(vec![StandardSet::NPos.into()]),
            Obj::StandardSet(StandardSet::QNeg) => Some(vec![StandardSet::ZNeg.into()]),
            Obj::StandardSet(StandardSet::QNz) => Some(vec![
                StandardSet::NPos.into(),
                StandardSet::ZNeg.into(),
                StandardSet::ZNz.into(),
                StandardSet::QPos.into(),
                StandardSet::QNeg.into(),
            ]),
            Obj::StandardSet(StandardSet::Q) => Some(vec![
                StandardSet::NPos.into(),
                StandardSet::N.into(),
                StandardSet::ZNeg.into(),
                StandardSet::ZNz.into(),
                StandardSet::Z.into(),
                StandardSet::QPos.into(),
                StandardSet::QNeg.into(),
                StandardSet::QNz.into(),
            ]),
            Obj::StandardSet(StandardSet::RPos) => {
                Some(vec![StandardSet::NPos.into(), StandardSet::QPos.into()])
            }
            Obj::StandardSet(StandardSet::RNeg) => {
                Some(vec![StandardSet::ZNeg.into(), StandardSet::QNeg.into()])
            }
            Obj::StandardSet(StandardSet::RNz) => Some(vec![
                StandardSet::NPos.into(),
                StandardSet::ZNeg.into(),
                StandardSet::ZNz.into(),
                StandardSet::QPos.into(),
                StandardSet::QNeg.into(),
                StandardSet::QNz.into(),
                StandardSet::RPos.into(),
                StandardSet::RNeg.into(),
            ]),
            Obj::StandardSet(StandardSet::R) => Some(vec![
                StandardSet::NPos.into(),
                StandardSet::N.into(),
                StandardSet::ZNeg.into(),
                StandardSet::ZNz.into(),
                StandardSet::Z.into(),
                StandardSet::QPos.into(),
                StandardSet::QNeg.into(),
                StandardSet::QNz.into(),
                StandardSet::Q.into(),
                StandardSet::RPos.into(),
                StandardSet::RNeg.into(),
                StandardSet::RNz.into(),
            ]),
            _ => None,
        }
    }

    // If the env already has `element $in fn_def` (from `known_objs_in_fn_sets`), compare to the RHS `fn ...`.
    fn verify_in_fact_element_in_fn_set_by_stored_definition(
        &mut self,
        element: &Obj,
        expected_fn_set: &FnSet,
        in_fact: &InFact,
    ) -> Result<StmtResult, RuntimeError> {
        let Some(stored_fn_set) = self.get_cloned_object_in_fn_set(element) else {
            return Ok((StmtUnknown::new()).into());
        };
        if stored_fn_set.to_string() == expected_fn_set.to_string() {
            return Ok(
                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    in_fact.clone().into(),
                    "fn membership: stored fn signature matches RHS".to_string(),
                    Vec::new(),
                ))
                .into(),
            );
        }
        let flat_stored =
            ParamGroupWithSet::collect_param_names(&stored_fn_set.params_def_with_set);
        let flat_expected =
            ParamGroupWithSet::collect_param_names(&expected_fn_set.body.params_def_with_set);
        if flat_stored.len() != flat_expected.len() {
            return Ok((StmtUnknown::new()).into());
        }
        let shared_names = self.generate_random_unused_names(flat_stored.len());
        let stored_norm =
            self.fn_set_alpha_renamed_for_display_compare(&stored_fn_set, &shared_names)?;
        let expected_norm =
            self.fn_set_alpha_renamed_for_display_compare(&expected_fn_set.body, &shared_names)?;
        if stored_norm.to_string() == expected_norm.to_string() {
            return Ok(
                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    in_fact.clone().into(),
                    "fn membership: stored fn signature matches RHS (alpha-renamed parameters)"
                        .to_string(),
                    Vec::new(),
                ))
                .into(),
            );
        }
        Ok((StmtUnknown::new()).into())
    }

    /// `anon $in S` when `S` is a function space [`FnSet`] and the anonymous function's
    /// [`FnSetBody`] (params, dom facts, return set) matches `S` (same as comparing `S` to a
    /// [`FnSet`] built from the anon's body without the braced `equal_to`).
    fn verify_in_fact_anonymous_fn_signature_matches_fn_set(
        &mut self,
        anon: &AnonymousFn,
        expected_fn_set: &FnSet,
        in_fact: &InFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let _ = verify_state;
        let signature_from_anon = FnSet::new(
            anon.body.params_def_with_set.clone(),
            anon.body.dom_facts.clone(),
            (*anon.body.ret_set).clone(),
        )?;
        if signature_from_anon.to_string() == expected_fn_set.to_string() {
            return Ok(
                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    in_fact.clone().into(),
                    "anonymous function: signature (params, dom, co-domain) matches `fn` set"
                        .to_string(),
                    Vec::new(),
                ))
                .into(),
            );
        }
        let flat_a =
            ParamGroupWithSet::collect_param_names(&signature_from_anon.body.params_def_with_set);
        let flat_e =
            ParamGroupWithSet::collect_param_names(&expected_fn_set.body.params_def_with_set);
        if flat_a.len() != flat_e.len() {
            return Ok((StmtUnknown::new()).into());
        }
        let shared_names = self.generate_random_unused_names(flat_a.len());
        let a_norm = self
            .fn_set_alpha_renamed_for_display_compare(&signature_from_anon.body, &shared_names)?;
        let e_norm =
            self.fn_set_alpha_renamed_for_display_compare(&expected_fn_set.body, &shared_names)?;
        if a_norm.to_string() == e_norm.to_string() {
            return Ok(
                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    in_fact.clone().into(),
                    "anonymous function: signature matches `fn` set (alpha-renamed parameters)"
                        .to_string(),
                    Vec::new(),
                ))
                .into(),
            );
        }
        Ok((StmtUnknown::new()).into())
    }

    fn verify_in_fact_by_known_standard_subset_membership(
        &mut self,
        in_fact: &InFact,
        target_set_obj: &Obj,
    ) -> Result<StmtResult, RuntimeError> {
        let standard_subset_set_objs =
            match Self::standard_subset_set_objs_for_target_set(target_set_obj) {
                Some(standard_subset_set_objs) => standard_subset_set_objs,
                None => return Ok((StmtUnknown::new()).into()),
            };
        for standard_subset_set_obj in standard_subset_set_objs.iter() {
            let in_fact_into_standard_subset = InFact::new(
                in_fact.element.clone(),
                standard_subset_set_obj.clone(),
                in_fact.line_file.clone(),
            )
            .into();
            let verify_result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(
                &in_fact_into_standard_subset,
            )?;
            if verify_result.is_true() {
                return Ok(
                    (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                        in_fact.clone().into(),
                        format!(
                            "{} in {} implies in {} (standard subset relation)",
                            in_fact.element, standard_subset_set_obj, target_set_obj
                        ),
                        Vec::new(),
                    ))
                    .into(),
                );
            }
        }
        Ok((StmtUnknown::new()).into())
    }

    fn verify_in_fact_by_left_is_tuple_right_is_cart(
        &mut self,
        in_fact: &InFact,
        tuple: &Tuple,
        cart: &Cart,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if tuple.args.len() < 2 {
            return Ok((StmtUnknown::new()).into());
        }
        if tuple.args.len() != cart.args.len() {
            return Ok((StmtUnknown::new()).into());
        }

        for component_index in 0..tuple.args.len() {
            let tuple_component_obj = (*tuple.args[component_index]).clone();
            let cart_component_obj = (*cart.args[component_index]).clone();
            let component_in_fact = InFact::new(
                tuple_component_obj,
                cart_component_obj,
                in_fact.line_file.clone(),
            )
            .into();
            let component_verify_result =
                self.verify_atomic_fact(&component_in_fact, verify_state)?;
            if !component_verify_result.is_true() {
                return Ok((StmtUnknown::new()).into());
            }
        }

        Ok(
            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                in_fact.clone().into(),
                "tuple in cart: each component is in the corresponding cart factor".to_string(),
                Vec::new(),
            ))
            .into(),
        )
    }
}