Nuprl Lemma : add-wf-partial-nat
∀[x,y:partial(ℕ)]. (x + y ∈ partial(ℕ))
Proof
Definitions occuring in Statement :
partial: partial(T),
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
add: n + m
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
nat: ℕ,
so_lambda: λ2x.t[x],
so_apply: x[s],
and: P ∧ Q,
cand: A c∧ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
sq_stable: SqStable(P),
squash: ↓T,
prop: ℙ,
not: ¬A,
false: False,
subtype_rel: A ⊆r B,
has-value: (a)↓
Lemmas referenced :
partial-base,
subtype_rel_partial,
nat_wf,
base_wf,
set_subtype_base,
le_wf,
istype-int,
int_subtype_base,
subtype_rel_transitivity,
partial_wf,
set-value-type,
int-value-type,
inclusion-partial,
add_nat_wf,
sq_stable__le,
is-exception_wf,
not_wf,
value-type-has-value,
has-value_wf_base,
apply-2-partial
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
independent_isectElimination,
sqequalRule,
intEquality,
Error :lambdaEquality_alt,
natural_numberEquality,
hypothesisEquality,
because_Cache,
independent_pairFormation,
baseClosed,
Error :dependent_set_memberEquality_alt,
addEquality,
setElimination,
rename,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
independent_functionElimination,
imageMemberEquality,
imageElimination,
Error :equalityIsType1,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
Error :universeIsType,
productElimination,
voidElimination,
baseApply,
closedConclusion,
applyEquality,
Error :productIsType,
callbyvalueAdd,
addExceptionCases
Latex:
\mforall{}[x,y:partial(\mBbbN{})]. (x + y \mmember{} partial(\mBbbN{}))
Date html generated:
2019_06_20-PM-00_34_19
Last ObjectModification:
2018_10_06-PM-05_12_59
Theory : partial_1
Home
Index