Nuprl Lemma : before-reverse
∀[T:Type]. ∀L:T List. ∀x,y:T. (x before y ∈ rev(L) ⇐⇒ y before x ∈ L)
Proof
Definitions occuring in Statement :
l_before: x before y ∈ l,
reverse: rev(as),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
universe: Type
Definitions unfolded in proof :
prop: ℙ,
top: Top,
implies: P ⇒ Q,
so_apply: x[s],
so_lambda: λ2x.t[x],
member: t ∈ T,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
false: False,
and: P ∧ Q,
iff: P ⇐⇒ Q,
or: P ∨ Q,
cand: A c∧ B,
guard: {T}
Lemmas referenced :
reverse-cons,
reverse_nil_lemma,
list_wf,
reverse_wf,
l_before_wf,
iff_wf,
all_wf,
list_induction,
nil_wf,
nil_before,
append_wf,
cons_before,
l_before_append_iff,
equal_wf,
l_member_wf,
cons_wf,
or_wf,
singleton_before,
member_singleton,
member-reverse,
cons_member
Rules used in proof :
universeEquality,
dependent_functionElimination,
because_Cache,
voidEquality,
voidElimination,
isect_memberEquality,
rename,
independent_functionElimination,
hypothesis,
cumulativity,
lambdaEquality,
sqequalRule,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
thin,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
productElimination,
independent_pairFormation,
impliesFunctionality,
addLevel,
productEquality,
unionElimination,
Error :inrFormation_alt,
Error :productIsType,
Error :equalityIstype,
Error :inhabitedIsType,
Error :universeIsType,
Error :inlFormation_alt,
hyp_replacement,
equalitySymmetry,
applyLambdaEquality,
Error :unionIsType
Latex:
\mforall{}[T:Type]. \mforall{}L:T List. \mforall{}x,y:T. (x before y \mmember{} rev(L) \mLeftarrow{}{}\mRightarrow{} y before x \mmember{} L)
Date html generated:
2019_06_20-PM-01_47_00
Last ObjectModification:
2019_01_15-PM-02_56_20
Theory : list_1
Home
Index