nx_proof_sqrt2_v3.nx
buildroot/runtime/nx_proof_sqrt2_v3.nx
about
nx_proof_sqrt2_v3.nx -- sqrt(2) is irrational, RESULT IS A CLOSED
THEOREM (no open hypotheses).
Difference vs v2: v2 stopped at "ASSUME |- false". v3 properly
DISCHARGES the assumption via NOT_INTRO to produce the actual
theorem "|- NOT (sqrt(2) = p/q in lowest terms)" with zero open
hypotheses. This is what HOL Light publishes as a theorem; v2 was
only an intermediate sequent.
dependencies 5 imports · 2 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_unify.nxnx_kernel_v2.nx
imported by: nx_proof_sqrt2_v3_test.nxnx_world_demo_test.nx
structs
| none |
consts
| 22 | const SYM_ASSUME: nx_int = 2001 |
| 23 | const SYM_PSQ_EVEN: nx_int = 2002 |
| 24 | const SYM_P_EVEN: nx_int = 2003 |
| 25 | const SYM_QSQ_EVEN: nx_int = 2004 |
| 26 | const SYM_Q_EVEN: nx_int = 2005 |
| 27 | const SYM_GCD_GE2: nx_int = 2006 |
functions
| 29 | func nx_proof_sqrt2_v3() -> nx_int called by 2: maindemo5_sqrt2 calls 13: nx_k2_chain_newnx_term_constnx_k2_notnx_k2_axiomnx_k2_impnx_k2_and+7 |