/* Lean 4 → C transpilation: SupportIsSearch.Refutation
 * Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: SupportIsSearch/Refutation.lean (209 lines)
 *
 * Theorem preserved: imp_forward_axiom_refuted
 *
 * This file demonstrates the refutation witness computationally:
 * for B = {}, phi = (p -> q), psi = q with distinct atoms p != q,
 * the premise of ImpForwardSchema holds but the conclusion is false.
 */

#include "encoding.c"
#include "kernel.c"

/*
 * Computational verification of the refutation witness.
 *
 * ImpForwardSchema states:
 *   forall B phi psi,
 *     (forall C >= B, SearchSupports (encodeBase C) (encode phi)
 *                   -> SearchSupports (encodeBase C) (encode psi))
 *     -> SearchSupports (encodeBase B) (encode (imp phi psi))
 *
 * Witness: B = {}, phi = (p -> q), psi = q for p = Atom(0), q = Atom(1).
 *
 * The premise holds because:
 *   SearchSupports (encodeBase C) (encode (p -> q))
 *   implies SearchSupports (encodeBase C) (encode q)
 *   for ANY atomic base C (proved as imp_atom_search_implies_rhs_search).
 *
 * The conclusion is false because:
 *   NOT SearchSupports (encodeBase {}) (encode ((p -> q) -> q))
 *   (proved as double_imp_not_searchable_from_empty).
 *
 * Therefore ImpForwardSchema is false.
 */

bool verify_refutation(unsigned int max_fuel) {
    Atom p = { .id = 0 };
    Atom q = { .id = 1 };

    /* Construct encode((p -> q) -> q) */
    IPL p_atom = { .tag = IPL_ATOM, .atom = p };
    IPL q_atom = { .tag = IPL_ATOM, .atom = q };
    IPL p_imp_q = { .tag = IPL_IMP, .binary = { &p_atom, &q_atom } };
    IPL double_imp = { .tag = IPL_IMP, .binary = { &p_imp_q, &q_atom } };

    Goal *encoded = encode(&double_imp);

    /* encodeBase({}) = empty program */
    Program empty = NULL;

    /* The conclusion MUST be false */
    bool conclusion = search_supports(empty, encoded, max_fuel);

    /* Return true iff the refutation holds (conclusion is false) */
    return !conclusion;
}