Nuprl Lemma : index-of-min_wf
∀[zs:ℤ List+]. (index-of-min(zs) ∈ {i:ℕ||zs||| ∀x:ℤ. ((x ∈ zs) ⇒ (zs[i] ≤ x))} )
Proof
Definitions occuring in Statement :
index-of-min: index-of-min(zs),
l_member: (x ∈ l),
select: L[n],
listp: A List+,
length: ||as||,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
index-of-min: index-of-min(zs),
all: ∀x:A. B[x],
implies: P ⇒ Q,
pi1: fst(t),
and: P ∧ Q,
prop: ℙ,
listp: A List+,
so_lambda: λ2x.t[x],
le: A ≤ B,
int_seg: {i..j-},
uimplies: b supposing a,
sq_stable: SqStable(P),
lelt: i ≤ j < k,
squash: ↓T,
so_apply: x[s],
guard: {T}
Lemmas referenced :
l_member_wf,
all_wf,
le_wf,
select_wf,
sq_stable__le,
select_member,
equal_wf,
listp_wf,
and_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
because_Cache,
thin,
lambdaFormation,
productElimination,
setElimination,
rename,
dependent_set_memberEquality,
hypothesisEquality,
sqequalHypSubstitution,
extract_by_obid,
isectElimination,
intEquality,
hypothesis,
lambdaEquality,
functionEquality,
dependent_functionElimination,
independent_isectElimination,
natural_numberEquality,
independent_functionElimination,
imageMemberEquality,
baseClosed,
imageElimination,
equalityTransitivity,
equalitySymmetry,
axiomEquality,
hyp_replacement,
independent_pairFormation,
applyEquality,
setEquality
Latex:
\mforall{}[zs:\mBbbZ{} List\msupplus{}]. (index-of-min(zs) \mmember{} \{i:\mBbbN{}||zs||| \mforall{}x:\mBbbZ{}. ((x \mmember{} zs) {}\mRightarrow{} (zs[i] \mleq{} x))\} )
Date html generated:
2016_10_21-AM-09_52_07
Last ObjectModification:
2016_07_12-AM-05_10_52
Theory : omega
Home
Index