Nuprl Lemma : nat_plus_inc_int_nzero
ℕ+ ⊆r ℤ-o
Proof
Definitions occuring in Statement :
int_nzero: ℤ-o,
nat_plus: ℕ+,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
nat_plus: ℕ+,
int_nzero: ℤ-o,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
nequal: a ≠ b ∈ T ,
not: ¬A,
false: False,
guard: {T}
Lemmas referenced :
subtype_rel_sets,
less_than_wf,
nequal_wf,
less_than_transitivity1,
le_weakening,
less_than_irreflexivity,
equal_wf,
equal-wf-base,
int_subtype_base,
nat_plus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
hypothesisEquality,
applyEquality,
thin,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
intEquality,
because_Cache,
natural_numberEquality,
hypothesis,
independent_isectElimination,
setElimination,
rename,
setEquality,
lambdaFormation,
dependent_functionElimination,
independent_functionElimination,
voidElimination,
baseClosed
Latex:
\mBbbN{}\msupplus{} \msubseteq{}r \mBbbZ{}\msupminus{}\msupzero{}
Date html generated:
2019_06_20-AM-11_33_34
Last ObjectModification:
2018_09_17-PM-05_37_06
Theory : int_1
Home
Index