nx_proof_sqrt2_v2_test.nx source
↩ module page · 33 lines · 1546 B
1// nx_proof_sqrt2_v2_test.nx -- exercise the sqrt(2) proof using the
2// SEMANTIC kernel (nx_kernel_v2).
3
4import "nx_syscalls.nx"
5import "nx_runtime.nx"
6import "nx_tier.nx"
7import "nx_kernel_v2.nx"
8import "nx_proof_sqrt2_v2.nx"
9
10func main() -> nx_exit {
11 println("=== sqrt(2) irrational -- SEMANTIC kernel verification ===" as *u8)
12 let v: nx_int = nx_proof_sqrt2_v2()
13 print("nx_k2_verify -> " as *u8); print_i64(v); println("" as *u8)
14 if v == NX_K2_OK {
15 println("VERIFIED OK -- every step semantically checked at emit time." as *u8)
16 println("" as *u8)
17 println("Chain shape (15 nodes):" as *u8)
18 println(" axioms 0..5: 6 implications + def-lowest-terms" as *u8)
19 println(" axiom 6: the assumption sqrt(2) = p/q in lowest terms" as *u8)
20 println(" step 7: MP(0, 6) |- p^2 even" as *u8)
21 println(" step 8: MP(1, 7) |- p even" as *u8)
22 println(" step 9: MP(2, 8) |- q^2 even" as *u8)
23 println(" step 10: MP(3, 9) |- q even" as *u8)
24 println(" step 11: AND_INTRO(8, 10) |- p_even & q_even" as *u8)
25 println(" step 12: MP(4, 11) |- gcd(p,q) >= 2" as *u8)
26 println(" step 13: MP(5, 6) |- NOT (gcd(p,q) >= 2)" as *u8)
27 println(" step 14: CONTRADICTION(12, 13) |- false" as *u8)
28 println("Each MP/CONTRADICTION premise was Term-checked by the kernel." as *u8)
29 return 0
30 }
31 print("VERIFY FAILED with code " as *u8); print_i64(v); println("" as *u8)
32 return 1
33}