nx_arith.nx

buildroot/runtime/nx_arith.nx

5984 B149 linesdepth 6pulls 6 transitivereach 14 importersview sourcekind library

docs dependencies structs consts functions

about

nx_arith.nx -- arithmetic Term substrate. Closes the named blocker for proof-by-induction / combinatorial / arithmetic Wiedijk theorems. Per user 2026-05-15: "no losses". Provides: - nat constructors: zero, succ(n), plus(a,b), mult(a,b) - nat literal builder for any concrete N - Peano axioms emitted as v2 kernel axioms with REAL Term shapes - finite induction engine: given P(0) + step axiom, auto-derive P(n) by emitting N modus-ponens applications through the v2 kernel Sym IDs reserved 410001..410010 (arith family; distinct from kernel 400xxx, user 1xxx, FMB 5xxxxx, AVATAR 6xxxxx, etc.)

dependencies 1 imports · 3 importers

imports: nx_kernel_v2.nx

imported by: nx_autoformalize_lib.nxnx_world_class_test.nxnx_world_demo_test.nx

structs

none

consts

24	const NX_ARITH_SYM_ZERO: nx_int = 410001
25	const NX_ARITH_SYM_SUCC: nx_int = 410002
26	const NX_ARITH_SYM_PLUS: nx_int = 410003
27	const NX_ARITH_SYM_MULT: nx_int = 410004
28	const NX_ARITH_SYM_LE: nx_int = 410005
29	const NX_ARITH_SYM_LT: nx_int = 410006
33	const NX_ARITH_AX_PA1_ZERO_NOT_SUCC: nx_int = 411001
34	const NX_ARITH_AX_PA2_SUCC_INJECT: nx_int = 411002
35	const NX_ARITH_AX_PA3_PLUS_ZERO: nx_int = 411003
36	const NX_ARITH_AX_PA4_PLUS_SUCC: nx_int = 411004
37	const NX_ARITH_AX_PA5_INDUCTION: nx_int = 411005

functions

40	func nx_arith_zero() -> *Term called by 4: nx_arith_nat nx_arith_axiom_plus_zero nx_arith_axiom_zero_not_succ af_derive_mult calls 1: nx_term_const
44	func nx_arith_succ(n: Term) -> Term called by 4: nx_arith_nat nx_arith_axiom_plus_succ nx_arith_axiom_zero_not_succ af_derive_sum calls 1: nx_term_app
50	func nx_arith_plus(a: Term, b: Term) -> *Term called by 7: nx_arith_axiom_plus_zero nx_arith_axiom_plus_succ af_derive_lt af_derive_sum af_derive_mult af_decide+1 calls 1: nx_term_app
59	func nx_arith_mult(a: Term, b: Term) -> *Term called by 2: af_derive_mult af_decide calls 1: nx_term_app
69	func nx_arith_nat(n: nx_int) -> *Term called by 10: af_derive_lt af_derive_le af_derive_sum af_derive_mult af_decide t1_nat_literal+4 calls 2: nx_arith_zero nx_arith_succ
103	func nx_arith_finite_induction( called by 2: t3_finite_induction demo4_induction calls 1: nx_k2_modus_ponens
135	func nx_arith_axiom_plus_zero(ch: K2Chain, n: Term) -> nx_int called by 2: af_derive_sum t2_peano_axioms calls 4: nx_k2_axiom nx_k2_eq nx_arith_plus nx_arith_zero
140	func nx_arith_axiom_plus_succ(ch: K2Chain, n: Term, m: *Term) -> nx_int called by 2: af_derive_sum t2_peano_axioms calls 4: nx_arith_plus nx_arith_succ nx_k2_axiom nx_k2_eq
147	func nx_arith_axiom_zero_not_succ(ch: K2Chain, n: Term) -> nx_int called by 1: t2_peano_axioms calls 5: nx_k2_axiom nx_k2_not nx_k2_eq nx_arith_zero nx_arith_succ