nx_prover_a1.nx

nx_prover_a1.nx -- Phase A1 extended-rule forward-chaining prover. Phase A0 (in nx_prover.nx) handled modus ponens only. Phase A1 adds four more rule families, dispatched per cycle: substitution (a = b) + P(a) -> P(b) conjunction intro A + B -> A^B conjunction elim A^B -> A (and A^B -> B) disjunction intro A -> A v B (for declared OR-targets) All rules are declared as TABLES. The caller supplies: subst_table[i*3] = "lhs" stmt subst_table[i*3+1] = "rhs" stmt (an equality A=B implies a=b) subst_table[i*3+2] = "carrier" P(*) stmt conj_table[i*3] = A stmt conj_table[i*3+1] = B stmt conj_table[i*3+2] = A^B stmt The forward-chaining loop applies each rule family per cycle until target found or no progress. Phase A1 still uses opaque i64 stmt_ids -- no internal structure reasoning. Phase A2 will add typed terms + unification. genealogy_id: prawitz_natural_deduction_1965 + gentzen_sequent_1935 lineage_id: substitution + intro_elim_rules + forward_chaining axioms: NX_AX_LOGIC_MODUS_PONENS_RULE + NX_DRULE_SUBSTITUTION + NX_DRULE_CONJ_INTRO + NX_DRULE_CONJ_ELIM + NX_DRULE_DISJ_INTRO