Nuprl Lemma : merge-int-sorted
∀[T:Type]. ∀[as,bs:T List]. sorted(merge-int(bs;as)) supposing sorted(bs) supposing T ⊆r ℤ
Proof
Definitions occuring in Statement :
sorted: sorted(L),
merge-int: merge-int(as;bs),
list: T List,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
merge-int: merge-int(as;bs),
all: ∀x:A. B[x],
top: Top,
sorted: sorted(L),
le: A ≤ B,
and: P ∧ Q,
not: ¬A,
false: False,
int_seg: {i..j-},
sq_stable: SqStable(P),
lelt: i ≤ j < k,
squash: ↓T,
subtype_rel: A ⊆r B,
guard: {T}
Lemmas referenced :
subtype_rel_wf,
insert-int_wf,
insert-int-sorted,
reduce_cons_lemma,
int_seg_wf,
le_weakening2,
length_wf,
less_than_transitivity2,
sq_stable__le,
select_wf,
less_than'_wf,
reduce_nil_lemma,
merge-int_wf,
sorted_wf,
isect_wf,
list_wf,
uall_wf,
list_induction
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
thin,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
sqequalRule,
lambdaEquality,
hypothesis,
independent_isectElimination,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
productElimination,
independent_pairEquality,
because_Cache,
cumulativity,
setElimination,
rename,
natural_numberEquality,
imageMemberEquality,
baseClosed,
imageElimination,
applyEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
lambdaFormation,
intEquality,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[as,bs:T List]. sorted(merge-int(bs;as)) supposing sorted(bs) supposing T \msubseteq{}r \mBbbZ{}
Date html generated:
2016_05_14-AM-06_45_57
Last ObjectModification:
2016_01_14-PM-08_16_50
Theory : list_0
Home
Index