### Nuprl Lemma : sparse-signed-rep-lemma1-ext

`∀m:ℤ. (∃p:ℤ × {-2..3-} [let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) `` (↑isEven(k)))])`

Proof

Definitions occuring in Statement :  isEven: `isEven(n)` absval: `|i|` int_seg: `{i..j-}` assert: `↑b` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` implies: `P `` Q` and: `P ∧ Q` spread: spread def product: `x:A × B[x]` multiply: `n * m` add: `n + m` minus: `-n` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` subtract: `n - m` isEven: `isEven(n)` eq_int: `(i =z j)` modulus: `a mod n` absval: `|i|` btrue: `tt` it: `⋅` bfalse: `ff` sparse-signed-rep-lemma1 decidable__equal_int decidable__assert decidable__int_equal uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` or: `P ∨ Q` squash: `↓T`
Lemmas referenced :  sparse-signed-rep-lemma1 lifting-strict-int_eq istype-void strict4-decide lifting-strict-decide lifting-strict-callbyvalue value-type-has-value int-value-type has-value_wf_base istype-base is-exception_wf istype-universe lifting-strict-less decidable__equal_int decidable__assert decidable__int_equal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination independent_pairFormation lambdaFormation_alt callbyvalueIntEq baseApply closedConclusion hypothesisEquality productElimination intEquality universeIsType int_eqExceptionCases inrFormation_alt imageMemberEquality imageElimination exceptionSqequal inlFormation_alt

Latex:
\mforall{}m:\mBbbZ{}.  (\mexists{}p:\mBbbZ{}  \mtimes{}  \{-2..3\msupminus{}\}  [let  k,b  =  p  in  (m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))])

Date html generated: 2019_10_15-AM-11_26_33
Last ObjectModification: 2019_06_26-PM-04_35_33

Theory : general

Home Index