Nuprl Lemma : not-pair-member-int

`∀[a,b:Base].  (¬(<a, b> ∈ ℤ))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` not: `¬A` member: `t ∈ T` pair: `<a, b>` int: `ℤ` base: `Base`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` not: `¬A` implies: `P `` Q` uimplies: `b supposing a` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` false: `False` all: `∀x:A. B[x]`
Lemmas referenced :  base_wf ispair-implies-not-isint value-type-has-value int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :inhabitedIsType,  hypothesisEquality Error :universeIsType,  cut introduction extract_by_obid hypothesis Error :lambdaFormation_alt,  sqequalRule Error :equalityIsType4,  intEquality baseApply closedConclusion baseClosed because_Cache sqequalHypSubstitution isectElimination thin independent_isectElimination equalityTransitivity equalitySymmetry natural_numberEquality independent_functionElimination isintReduceTrue Error :equalityIsType1,  dependent_functionElimination voidElimination

Latex:
\mforall{}[a,b:Base].    (\mneg{}(<a,  b>  \mmember{}  \mBbbZ{}))

Date html generated: 2019_06_20-AM-11_21_38
Last ObjectModification: 2018_09_27-PM-07_01_32

Theory : call!by!value_1

Home Index