Nuprl Lemma : sorted-by-strict-unique
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[sa,sb:T List].
(sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))) supposing
((∀a:T. (¬(R a a))) and
AntiSym(T;a,b.R a b) and
Trans(T;a,b.R a b))
Proof
Definitions occuring in Statement :
sorted-by: sorted-by(R;L),
set-equal: set-equal(T;x;y),
list: T List,
anti_sym: AntiSym(T;x,y.R[x; y]),
trans: Trans(T;x,y.E[x; y]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
not: ¬A,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2]
Lemmas referenced :
sorted-by-unique,
sorted-by_wf,
subtype_rel_dep_function,
l_member_wf,
subtype_rel_self,
set_wf,
set-equal_wf,
list_wf,
all_wf,
not_wf,
anti_sym_wf,
trans_wf,
sorted-by-strict-no_repeats
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
introduction,
independent_isectElimination,
cumulativity,
applyEquality,
instantiate,
sqequalRule,
lambdaEquality,
functionEquality,
universeEquality,
setEquality,
setElimination,
rename,
lambdaFormation,
because_Cache,
isect_memberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
(\mforall{}[sa,sb:T List].
(sa = sb) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))) supposing
((\mforall{}a:T. (\mneg{}(R a a))) and
AntiSym(T;a,b.R a b) and
Trans(T;a,b.R a b))
Date html generated:
2016_05_14-PM-01_48_04
Last ObjectModification:
2015_12_26-PM-05_35_11
Theory : list_1
Home
Index