Nuprl Lemma : insert-int-1-1

∀[T:Type]
  ∀[as,bs:T List].
    (∀[x:T]. as = bs ∈ (T List) supposing insert-int(x;as) = insert-int(x;bs) ∈ (T List)) supposing 
       (sorted(bs) and 
       sorted(as)) 
  supposing T ⊆r ℤ


Proof



Definitions occuring in Statement :  sorted: sorted(L),  insert-int: insert-int(x;l),  list: T List,  uimplies: b supposing a,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  int: ℤ,  universe: Type,  equal: s = t ∈ T
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,  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  nat: ℕ,  iff: P ⇐⇒ Q,  squash: ↓T,  sq_type: SQType(T),  false: False,  less_than': less_than'(a;b),  not: ¬A,  le: A ≤ B,  subtract: n - m,  guard: {T},  and: P ∧ Q,  uiff: uiff(P;Q),  ge: i ≥ j ,  exists: ∃x:A. B[x],  top: Top,  true: True,  label: ...$L... t,  or: P ∨ Q,  ifthenelse: if b then t else f fi ,  btrue: tt,  rev_implies: P ⇐ Q,  bfalse: ff
Lemmas referenced :  list_induction,  uall_wf,  list_wf,  isect_wf,  sorted_wf,  equal_wf,  insert-int_wf,  nil_wf,  equal-wf-base-T,  cons_wf,  subtype_rel_wf,  nat_properties,  iff_weakening_equal,  length-insert-int,  true_wf,  squash_wf,  int_subtype_base,  subtype_base_sq,  one-mul,  zero-add,  zero-mul,  mul-distributes-right,  two-mul,  add-mul-special,  subtract_wf,  le-add-cancel2,  add-zero,  add_functionality_wrt_le,  add-commutes,  add-associates,  minus-one-mul-top,  add-swap,  minus-one-mul,  minus-add,  condition-implies-le,  le_antisymmetry_iff,  base_wf,  subtype_rel-equal,  nat_wf,  length_wf_nat,  non_neg_length,  length_of_cons_lemma,  length_of_nil_lemma,  length_wf,  subtype_rel_list,  lt_int_wf,  cons_one_one,  assert_wf,  bnot_wf,  not_wf,  less_than_wf,  less_than_transitivity1,  le_weakening,  less_than_irreflexivity,  insert-int-cons,  bool_cases,  bool_wf,  bool_subtype_base,  eqtt_to_assert,  assert_of_lt_int,  eqff_to_assert,  iff_transitivity,  iff_weakening_uiff,  assert_of_bnot,  sorted-cons
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,  voidEquality,  voidElimination,  baseClosed,  isect_memberEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  lambdaFormation,  rename,  dependent_functionElimination,  intEquality,  universeEquality,  setElimination,  imageMemberEquality,  imageElimination,  instantiate,  multiplyEquality,  promote_hyp,  minusEquality,  productElimination,  addEquality,  applyEquality,  sqequalIntensionalEquality,  dependent_pairFormation,  natural_numberEquality,  applyLambdaEquality,  unionElimination,  independent_pairFormation,  impliesFunctionality
Latex:
\mforall{}[T:Type]
    \mforall{}[as,bs:T  List].
        (\mforall{}[x:T].  as  =  bs  supposing  insert-int(x;as)  =  insert-int(x;bs))  supposing 
              (sorted(bs)  and 
              sorted(as)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


Date html generated: 2017_09_29-PM-05_50_06
Last ObjectModification: 2017_07_26-PM-01_39_03

Theory : list_0


Home Index