Nuprl Lemma : merge-int-1-1

  ∀[cs,as,bs:T List].
    (as bs ∈ (T List)) supposing ((merge-int(as;cs) merge-int(bs;cs) ∈ (T List)) and sorted(bs) and sorted(as)) 
  supposing T ⊆r ℤ


Definitions occuring in Statement :  sorted: sorted(L) merge-int: merge-int(as;bs) list: List uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] int: universe: Type equal: t ∈ T
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-int: merge-int(as;bs) all: x:A. B[x] top: Top guard: {T}
Lemmas referenced :  list_induction uall_wf list_wf isect_wf sorted_wf equal_wf merge-int_wf reduce_nil_lemma reduce_cons_lemma insert-int_wf subtype_rel_wf insert-int-1-1 merge-int-sorted
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis because_Cache independent_isectElimination independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality axiomEquality equalityTransitivity equalitySymmetry lambdaFormation rename intEquality universeEquality

    \mforall{}[cs,as,bs:T  List].
        (as  =  bs)  supposing  ((merge-int(as;cs)  =  merge-int(bs;cs))  and  sorted(bs)  and  sorted(as)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}

Date html generated: 2017_04_14-AM-08_49_48
Last ObjectModification: 2017_02_27-PM-03_35_39

Theory : list_0

Home Index