Nuprl Lemma : no_repeats-merge

[T:Type]. ∀[bs,as:T List].  (no_repeats(T;merge(as;bs))) supposing (sorted(as) and no_repeats(T;as)) supposing T ⊆r ℤ


Definitions occuring in Statement :  merge: merge(as;bs) no_repeats: no_repeats(T;l) sorted: sorted(L) list: List uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] prop: so_apply: x[s] implies:  Q merge: merge(as;bs) all: x:A. B[x] top: Top guard: {T}
Lemmas referenced :  list_induction uall_wf list_wf isect_wf no_repeats_wf sorted_wf merge_wf reduce_nil_lemma no_repeats_witness reduce_cons_lemma s-insert-no-repeats sorted-merge s-insert_wf subtype_rel_wf
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 because_Cache equalityTransitivity equalitySymmetry lambdaFormation rename intEquality universeEquality

    \mforall{}[bs,as:T  List].    (no\_repeats(T;merge(as;bs)))  supposing  (sorted(as)  and  no\_repeats(T;as)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}

Date html generated: 2016_05_15-PM-03_52_45
Last ObjectModification: 2015_12_27-PM-01_23_53

Theory : general

Home Index