### Nuprl Lemma : remove-combine-cons

`∀[T:Type]. ∀[cmp:T ⟶ ℤ]. ∀[x:T]. ∀[l:T List].`
`  (remove-combine(cmp;[x / l]) ~ if (cmp x =z 0) then l`
`  if 0 <z cmp x then [x / l]`
`  else [x / remove-combine(cmp;l)]`
`  fi )`

Proof

Definitions occuring in Statement :  remove-combine: `remove-combine(cmp;l)` cons: `[a / b]` list: `T List` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` remove-combine: `remove-combine(cmp;l)` all: `∀x:A. B[x]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` has-value: `(a)↓` uimplies: `b supposing a`
Lemmas referenced :  list_ind_cons_lemma value-type-has-value int-value-type list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis callbyvalueReduce isectElimination intEquality independent_isectElimination applyEquality hypothesisEquality sqequalAxiom because_Cache functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[x:T].  \mforall{}[l:T  List].
(remove-combine(cmp;[x  /  l])  \msim{}  if  (cmp  x  =\msubz{}  0)  then  l
if  0  <z  cmp  x  then  [x  /  l]
else  [x  /  remove-combine(cmp;l)]
fi  )

Date html generated: 2016_05_14-PM-02_42_23
Last ObjectModification: 2015_12_26-PM-02_42_34

Theory : list_1

Home Index