### Nuprl Lemma : mon_for_when_unique

`∀s:DSet. ∀g:IMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.`
`  ((↑b[u])`
`  `` (∀as:|s| List`
`        ((↑distinct{s}(as))`
`        `` (↑(u ∈b as))`
`        `` (∀v:|s|. ((↑b[v]) `` (↑(v ∈b as)) `` (v = u ∈ |s|)))`
`        `` ((For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|))))`

Proof

Definitions occuring in Statement :  distinct: `distinct{s}(ps)` mem: `a ∈b as` mon_for: `For{g} x ∈ as. f[x]` list: `T List` assert: `↑b` bool: `𝔹` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` equal: `s = t ∈ T` mon_when: `when b. p` imon: `IMonoid` grp_car: `|g|` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` dset: `DSet` so_apply: `x[s]` imon: `IMonoid` top: `Top` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` false: `False` infix_ap: `x f y` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` band: `p ∧b q` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ball: ball squash: `↓T` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` mon_when: `when b. p` not: `¬A`
Lemmas referenced :  list_induction assert_wf distinct_wf mem_wf all_wf set_car_wf equal_wf grp_car_wf mon_for_wf mon_when_wf distinct_nil_lemma istype-void mem_nil_lemma mon_for_nil_lemma true_wf distinct_cons_lemma mem_cons_lemma mon_for_cons_lemma bor_wf set_eq_wf ball_wf bnot_wf infix_ap_wf bool_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bfalse_wf list_wf imon_wf dset_wf or_wf equal-wf-T-base not_wf squash_wf istype-universe mon_ident subtype_rel_self iff_weakening_equal uiff_transitivity assert_of_bnot assert_of_band iff_transitivity iff_weakening_uiff assert_of_bor assert_of_dset_eq grp_op_wf mon_for_when_none ball_char grp_id_wf member_wf assert_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality_alt functionEquality dependent_functionElimination hypothesisEquality hypothesis setElimination rename applyEquality inhabitedIsType universeIsType independent_functionElimination isect_memberEquality_alt voidElimination functionIsType equalityIsType1 unionElimination equalityElimination productElimination independent_isectElimination dependent_pairFormation_alt equalityTransitivity equalitySymmetry promote_hyp instantiate unionIsType baseClosed imageElimination universeEquality natural_numberEquality imageMemberEquality independent_pairFormation inlFormation_alt inrFormation_alt

Latex:
\mforall{}s:DSet.  \mforall{}g:IMonoid.  \mforall{}f:|s|  {}\mrightarrow{}  |g|.  \mforall{}b:|s|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}u:|s|.
((\muparrow{}b[u])
{}\mRightarrow{}  (\mforall{}as:|s|  List
((\muparrow{}distinct\{s\}(as))
{}\mRightarrow{}  (\muparrow{}(u  \mmember{}\msubb{}  as))
{}\mRightarrow{}  (\mforall{}v:|s|.  ((\muparrow{}b[v])  {}\mRightarrow{}  (\muparrow{}(v  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (v  =  u)))
{}\mRightarrow{}  ((For\{g\}  x  \mmember{}  as.  (when  b[x].  f[x]))  =  f[u]))))

Date html generated: 2019_10_16-PM-01_02_59
Last ObjectModification: 2018_10_08-AM-11_32_18

Theory : list_2

Home Index