code wiki / (root) / nx_derive_test.nx

nx_derive_test.nx

buildroot/runtime/nx_derive_test.nx

3127 B75 linesdepth 4pulls 5 transitivereach 0 importersview sourcekind gate/proof
docsdependenciesstructsconstsfunctions

about

nx_derive_test.nx -- smoke for axiom + derivation primitives. Concrete derivation: from Peano PA1 (zero exists) + PA2 (successor) + PA5 (induction) we derive a trivial theorem "1 exists" by universal-instantiation-style application of PA2 to PA1. (The substrate doesn't interpret the statements -- it verifies the STRUCTURE: axioms cited are valid; rules match arity; theorem marked.)

dependencies 3 imports · 0 importers

syscalls.nx nx_axioms.nx nx_derive.nx nx_derive_test.nx

imports: syscalls.nxnx_axioms.nxnx_derive.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main nx_deriv_chain_alloc nx_deriv_add_axiom nx_axiom_is_valid nx_deriv_node_at nx_deriv_add_step nx_drule_arity nx_deriv_node_at ↻ nx_deriv_mark_theorem nx_deriv_node_at ↻ nx_deriv_verify nx_deriv_node_at ↻ nx_axiom_is_valid ↻ nx_drule_arity ↻ nx_deriv_node_at ↻

structs

none

consts

13const STMT_ZERO_EXISTS: i64 = 1
14const STMT_SUCCESSOR_OF_ZERO_EXISTS: i64 = 2

functions

16func main() -> i64 {
calls 6: nx_deriv_chain_allocnx_deriv_add_axiomnx_deriv_add_stepnx_deriv_mark_theoremnx_deriv_verifynx_deriv_node_at