code wiki / (root) / nx_prove_propositional_test.nx

nx_prove_propositional_test.nx

buildroot/runtime/nx_prove_propositional_test.nx

10066 B240 linesdepth 7pulls 7 transitivereach 0 importersview sourcekind gate/proof

docs dependencies structs consts functions

about

nx_prove_propositional_test.nx Exercises the auto-prover engine across every Wikipedia-documented propositional proof method. Per user 2026-05-15: "make sure it exceeds or matches everything wikipedia called out on proofs that are required".

dependencies 1 imports · 0 importers

imports: nx_prove_propositional.nx

imported by: nobody (leaf or entry point)

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

structs

none

consts

10	const SYM_A: nx_int = 1001
11	const SYM_B: nx_int = 1002
12	const SYM_C: nx_int = 1003

functions

14	func two_axioms(a: nx_int, b: nx_int) -> *nx_int called by 3: test_construction_and test_hyp_syllogism test_modus_tollens
21	func three_axioms(a: nx_int, b: nx_int, c: nx_int) -> *nx_int called by 1: test_direct
29	func one_axiom(a: nx_int) -> *nx_int called by 4: test_and_comm test_contraposition test_or_intro test_double_negation
35	func empty_axioms() -> *nx_int called by 2: test_identity test_k_combinator
40	func attempt(ch: *K2Chain, idx: nx_int) -> nx_int called by 10: test_direct test_construction_and test_and_comm test_identity test_k_combinator test_hyp_syllogism+4 calls 3: nx_k2_at nx_k2_mark_theorem nx_k2_verify
49	func report(name: *u8, ok: nx_int, chain_len: nx_int) -> nx_int called by 10: test_direct test_construction_and test_and_comm test_identity test_k_combinator test_hyp_syllogism+4
63	func test_direct() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom nx_k2_imp three_axioms nx_prove+2
77	func test_construction_and() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom two_axioms nx_k2_and nx_prove+2
90	func test_and_comm() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom nx_k2_and one_axiom nx_prove+2
102	func test_identity() -> nx_int called by 1: main calls 7: nx_k2_chain_new nx_term_const empty_axioms nx_k2_imp nx_prove attempt+1
112	func test_k_combinator() -> nx_int called by 1: main calls 7: nx_k2_chain_new nx_term_const empty_axioms nx_k2_imp nx_prove attempt+1
123	func test_hyp_syllogism() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom nx_k2_imp two_axioms nx_prove+2
137	func test_modus_tollens() -> nx_int called by 1: main calls 9: nx_k2_chain_new nx_term_const nx_k2_axiom nx_k2_imp nx_k2_not two_axioms+3
150	func test_contraposition() -> nx_int called by 1: main calls 9: nx_k2_chain_new nx_term_const nx_k2_axiom nx_k2_imp one_axiom nx_k2_not+3
162	func test_or_intro() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom one_axiom nx_k2_or nx_prove+2
174	func test_double_negation() -> nx_int called by 1: main calls 8: nx_k2_chain_new nx_term_const nx_k2_axiom one_axiom nx_k2_not nx_prove+2
185	func main() -> nx_exit calls 10: test_direct test_construction_and test_and_comm test_identity test_k_combinator test_hyp_syllogism+4