code wiki / (root) / nx_proofs_comprehensive.nx

nx_proofs_comprehensive.nx

buildroot/runtime/nx_proofs_comprehensive.nx

12234 B232 linesdepth 5pulls 10 transitivereach 0 importersview sourcekind tooltopic proofs
docsdependenciesstructsconstsfunctions

about

nx_proofs_comprehensive.nx -- one worked example per proof method from the Wikipedia "Mathematical proof" taxonomy. Each is a real nx_derive chain verified by the kernel. All 14 methods covered.

dependencies 8 imports · 0 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_axioms.nx nx_derive.nx nx_proof_methods.nx nx_classical_unpatented.nx nx_classical_unpatented_2.nx nx_proofs_comprehensive.nx

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_axioms.nxnx_derive.nxnx_proof_methods.nxnx_classical_unpatented.nxnx_classical_unpatented_2.nx

imported by: nobody (leaf or entry point)

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

main sys_mmap nxa_die sys_write sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ println sys_write ↻ strlen sys_mmap ↻ nx_deriv_chain_alloc nx_deriv_add_axiom nx_axiom_is_valid nx_deriv_node_at nx_deriv_mark_theorem nx_deriv_node_at ↻ nx_method_report print sys_write ↻ strlen ↻ nx_proof_method_name nx_proof_qed println ↻ print_i64 sys_mmap ↻ itoa sys_mmap ↻ sys_write ↻ nx_deriv_verify nx_deriv_node_at ↻

structs

none

consts

none

functions

20func nx_method_report(method_code: nx_int, theorem_label: *u8, status: nx_int,
called by 1: main calls 5: printnx_proof_method_namenx_proof_qedprintlnprint_i64
32func main() -> nx_exit
calls 11: sys_mmapprintlnnx_deriv_chain_allocnx_deriv_add_axiomnx_deriv_mark_theoremnx_method_report+5