Nuprl Lemma : exact-reduce-constraints_wf2
∀[n:ℕ]. ∀[w:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ} ]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ} List].
(exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
Proof
Definitions occuring in Statement :
exact-reduce-constraints: exact-reduce-constraints(w;j;L),
length: ||as||,
list: T List,
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
uimplies: b supposing a,
nat: ℕ,
so_apply: x[s],
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
sq_stable: SqStable(P),
decidable: Dec(P),
or: P ∨ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
not: ¬A,
rev_implies: P ⇐ Q,
false: False,
uiff: uiff(P;Q),
guard: {T},
subtract: n - m,
le: A ≤ B,
less_than': less_than'(a;b),
true: True,
squash: ↓T
Lemmas referenced :
exact-reduce-constraints_wf,
subtype_rel_list_set,
list_wf,
equal-wf-base,
list_subtype_base,
int_subtype_base,
set_subtype_base,
le_wf,
istype-int,
equal_wf,
length_wf,
sq_stable__subtype_rel,
decidable__equal_int,
subtract_wf,
istype-false,
not-equal-2,
le_antisymmetry_iff,
condition-implies-le,
minus-add,
minus-minus,
minus-one-mul,
add-swap,
minus-one-mul-top,
add-commutes,
add-associates,
add_functionality_wrt_le,
le-add-cancel,
zero-add,
int_seg_wf,
istype-nat
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis,
applyEquality,
intEquality,
because_Cache,
sqequalRule,
lambdaEquality_alt,
baseApply,
closedConclusion,
baseClosed,
independent_isectElimination,
natural_numberEquality,
universeIsType,
addEquality,
inhabitedIsType,
lambdaFormation_alt,
equalityTransitivity,
equalitySymmetry,
equalityIstype,
sqequalBase,
setEquality,
independent_functionElimination,
setIsType,
dependent_functionElimination,
unionElimination,
independent_pairFormation,
voidElimination,
productElimination,
minusEquality,
Error :memTop,
imageMemberEquality,
imageElimination,
axiomEquality,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[w:\{l:\mBbbZ{} List| ||l|| = (n + 1)\} ]. \mforall{}[j:\mBbbN{}||w||]. \mforall{}[L:\{l:\mBbbZ{} List| ||l|| = (n + 1)\} List].
(exact-reduce-constraints(w;j;L) \mmember{} \{l:\mBbbZ{} List| ||l|| = ((n - 1) + 1)\} List)
Date html generated:
2020_05_19-PM-09_39_32
Last ObjectModification:
2020_01_04-PM-07_58_48
Theory : omega
Home
Index