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: 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 subtype_rel: A ⊆B all: x:A. B[x] nat: iff: ⇐⇒ Q squash: T sq_type: SQType(T) false: False less_than': less_than'(a;b) not: ¬A le: A ≤ B subtract: m guard: {T} and: P ∧ Q uiff: uiff(P;Q) ge: i ≥  exists: x:A. B[x] top: Top true: True label: ...$L... t or: P ∨ Q ifthenelse: if then else fi  btrue: tt rev_implies:  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