Nuprl Lemma : l_before_l_index
∀[T:Type]
∀dT:EqDecider(T). ∀L:T List. ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ x before y ∈ L supposing index(L;x) < index(L;y))
Proof
Definitions occuring in Statement :
l_index: index(L;x),
l_before: x before y ∈ l,
l_member: (x ∈ l),
list: T List,
deq: EqDecider(T),
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
member: t ∈ T,
subtype_rel: A ⊆r B,
int_seg: {i..j-},
prop: ℙ,
squash: ↓T,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
member-less_than,
l_index_wf,
int_seg_wf,
length_wf,
less_than_wf,
l_member_wf,
list_wf,
deq_wf,
l_before_select,
l_before_wf,
squash_wf,
true_wf,
equal_wf,
select_l_index,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
independent_isectElimination,
hypothesis,
applyEquality,
lambdaEquality,
setElimination,
rename,
natural_numberEquality,
sqequalRule,
universeEquality,
dependent_functionElimination,
hyp_replacement,
equalitySymmetry,
imageElimination,
equalityTransitivity,
because_Cache,
imageMemberEquality,
baseClosed,
productElimination,
independent_functionElimination
Latex:
\mforall{}[T:Type]
\mforall{}dT:EqDecider(T). \mforall{}L:T List. \mforall{}x,y:T.
((x \mmember{} L) {}\mRightarrow{} (y \mmember{} L) {}\mRightarrow{} x before y \mmember{} L supposing index(L;x) < index(L;y))
Date html generated:
2017_04_17-AM-09_16_02
Last ObjectModification:
2017_02_27-PM-05_21_10
Theory : decidable!equality
Home
Index