/* Lean 4 → C transpilation: SupportIsSearch.Contextual.Context
 * Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: SupportIsSearch/Contextual/Context.lean (23 lines)
 * Theorem preserved: baseExtends_refl
 *
 * The Base type and BaseExtends relation. This is where the paper-to-code
 * gap lives: the paper defines bases as arbitrary programs, but this
 * formalization uses atomic bases (lists of atoms). BaseExtends only checks
 * atom inclusion, not arbitrary clause inclusion.
 */

#include "syntax.c"

/* Base: an atomic base (list of atoms) */
typedef struct {
    Atom *atoms;
    size_t count;
} Base;

/* BaseExtends: B extends to C iff every atom in B is also in C */
bool base_extends(Base B, Base C) {
    for (size_t i = 0; i < B.count; i++) {
        bool found = false;
        for (size_t j = 0; j < C.count; j++) {
            if (B.atoms[i].id == C.atoms[j].id) { found = true; break; }
        }
        if (!found) return false;
    }
    return true;
}

/* Theorem preserved: baseExtends_refl — every base extends itself */
/* Proof: trivially, every atom in B is in B. */