Nuprl Lemma : bag-remove1-property1

`∀[T:Type]`
`  ∀eq:EqDecider(T). ∀x:T. ∀L:T List.`
`    ((∃as,bs:T List. ((L = ((as @ [x]) @ bs) ∈ (T List)) ∧ (bag-remove1(eq;L;x) = (inl (rev(as) @ bs)) ∈ (T List?))))`
`    ∨ ((¬(x ∈ L)) ∧ (bag-remove1(eq;L;x) = (inr ⋅ ) ∈ (T List?))))`

Proof

Definitions occuring in Statement :  bag-remove1: `bag-remove1(eq;bs;a)` l_member: `(x ∈ l)` reverse: `rev(as)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` deq: `EqDecider(T)` it: `⋅` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` unit: `Unit` inr: `inr x ` inl: `inl x` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` bag-remove1: `bag-remove1(eq;bs;a)` or: `P ∨ Q` exists: `∃x:A. B[x]` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top` prop: `ℙ` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}`
Lemmas referenced :  bag_remove1_aux_property nil_wf append-nil reverse_wf subtype_rel_list top_wf equal_wf list_wf append_wf cons_wf length_wf length-append exists_wf not_wf l_member_wf equal-wf-T-base unit_wf2 bag_remove1_aux_wf deq_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination cumulativity unionElimination inlFormation productElimination dependent_pairFormation independent_pairFormation promote_hyp sqequalRule applyEquality independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache productEquality applyLambdaEquality unionEquality baseClosed inrFormation universeEquality

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.
((\mexists{}as,bs:T  List.  ((L  =  ((as  @  [x])  @  bs))  \mwedge{}  (bag-remove1(eq;L;x)  =  (inl  (rev(as)  @  bs)))))
\mvee{}  ((\mneg{}(x  \mmember{}  L))  \mwedge{}  (bag-remove1(eq;L;x)  =  (inr  \mcdot{}  ))))

Date html generated: 2018_05_21-PM-09_48_06
Last ObjectModification: 2017_07_26-PM-06_30_33

Theory : bags_2

Home Index