### Nuprl Lemma : bag_remove1_aux_property

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

Proof

Definitions occuring in Statement :  bag_remove1_aux: `bag_remove1_aux(eq;checked;a;as)` 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]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` top: `Top` so_apply: `x[s]` implies: `P `` Q` bag_remove1_aux: `bag_remove1_aux(eq;checked;a;as)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` deq: `EqDecider(T)` exposed-bfalse: `exposed-bfalse` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` eqof: `eqof(d)` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` cand: `A c∧ B` append: `as @ bs` list_ind: list_ind reverse: `rev(as)` rev-append: `rev(as) + bs` list_accum: list_accum nil: `[]` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction all_wf list_wf or_wf exists_wf equal_wf append_wf cons_wf nil_wf length_wf length-append not_wf l_member_wf equal-wf-T-base unit_wf2 bag_remove1_aux_wf list_ind_nil_lemma list_ind_cons_lemma bool_wf eqtt_to_assert safe-assert-deq eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot deq_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse it_wf equal-wf-base-T length_of_nil_lemma reverse_wf and_wf length_of_cons_lemma squash_wf true_wf iff_weakening_equal reverse-cons append_assoc cons_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality cumulativity hypothesisEquality hypothesis productEquality applyLambdaEquality isect_memberEquality voidElimination voidEquality unionEquality baseClosed independent_functionElimination dependent_functionElimination rename applyEquality setElimination unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation promote_hyp instantiate universeEquality inrFormation independent_pairFormation inrEquality inlEquality inlFormation dependent_set_memberEquality imageElimination natural_numberEquality imageMemberEquality hyp_replacement

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

Date html generated: 2018_05_21-PM-09_48_03
Last ObjectModification: 2017_07_26-PM-06_30_31

Theory : bags_2

Home Index