Nuprl Lemma : ml_merge_int-sq
∀[bs,as:ℤ List]. (ml_merge_int(as;bs) ~ merge-int(as;bs))
Proof
Definitions occuring in Statement :
ml_merge_int: ml_merge_int(as;bs),
merge-int: merge-int(as;bs),
list: T List,
uall: ∀[x:A]. B[x],
int: ℤ,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
merge-int: merge-int(as;bs),
ml_merge_int: ml_merge_int(as;bs),
ml_apply: f(x),
callbyvalueall: callbyvalueall,
has-value: (a)↓,
has-valueall: has-valueall(a),
sq_type: SQType(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
guard: {T},
ml_insert_int: ml_insert_int(x;l),
and: P ∧ Q,
cand: A c∧ B,
true: True,
squash: ↓T,
prop: ℙ,
subtype_rel: A ⊆r B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
subtype_base_sq,
list_wf,
list_subtype_base,
int_subtype_base,
valueall-type-has-valueall,
list-valueall-type,
int-valueall-type,
evalall-reduce,
ml_insert_int-sq,
insert-int_wf,
subtype_rel_self,
reduce_wf,
ml-reduce-sq,
equal_wf,
squash_wf,
true_wf,
ml-reduce_wf,
valueall-type_wf,
iff_weakening_equal
Rules used in proof :
cut,
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
natural_numberEquality,
isect_memberFormation,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
cumulativity,
intEquality,
hypothesis,
independent_isectElimination,
sqequalRule,
hypothesisEquality,
callbyvalueReduce,
because_Cache,
axiomEquality,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
sqequalAxiom,
isect_memberEquality,
functionExtensionality,
independent_pairFormation,
applyEquality,
lambdaEquality,
imageElimination,
universeEquality,
productElimination,
productEquality,
functionEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[bs,as:\mBbbZ{} List]. (ml\_merge\_int(as;bs) \msim{} merge-int(as;bs))
Date html generated:
2017_09_29-PM-05_51_23
Last ObjectModification:
2017_05_11-PM-05_13_35
Theory : ML
Home
Index