### Nuprl Lemma : strict-bag-function_wf

`∀[L:Type List]. ∀[B:Type]. ∀[G:tuple-type(map(λT.bag(T);L)) ⟶ bag(B)]. ∀[S:ℕ||L|| List].`
`  (strict-bag-function(G;L;B;S) ∈ ℙ)`

Proof

Definitions occuring in Statement :  strict-bag-function: `strict-bag-function(G;L;B;S)` bag: `bag(T)` tuple-type: `tuple-type(L)` length: `||as||` map: `map(f;as)` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` strict-bag-function: `strict-bag-function(G;L;B;S)` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` uimplies: `b supposing a` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` less_than: `a < b` squash: `↓T` so_apply: `x[s]` subtype_rel: `A ⊆r B` cand: `A c∧ B`
Lemmas referenced :  subtype_rel_self top_wf subtype_rel_list select-map map_length map-length int_seg_subtype_nat select-tuple_wf list_wf equal-wf-T-base empty-bag_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le int_seg_properties select_wf equal_wf l_member_wf length_wf int_seg_wf l_all_wf bag_wf map_wf tuple-type_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin instantiate universeEquality because_Cache lambdaEquality cumulativity hypothesisEquality hypothesis functionEquality natural_numberEquality lambdaFormation setElimination rename independent_isectElimination productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination setEquality applyEquality baseClosed axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[L:Type  List].  \mforall{}[B:Type].  \mforall{}[G:tuple-type(map(\mlambda{}T.bag(T);L))  {}\mrightarrow{}  bag(B)].  \mforall{}[S:\mBbbN{}||L||  List].
(strict-bag-function(G;L;B;S)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_15-PM-02_58_46
Last ObjectModification: 2016_01_16-AM-08_39_33

Theory : bags

Home Index