Nuprl Lemma : mon_for_of_op

g:IAbMonoid. ∀A:Type. ∀e,f:A ⟶ |g|. ∀as:A List.
  ((For{g} x ∈ as. (e[x] f[x])) ((For{g} x ∈ as. e[x]) (For{g} x ∈ as. f[x])) ∈ |g|)


Proof




Definitions occuring in Statement :  mon_for: For{g} x ∈ as. f[x] list: List infix_ap: y so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T iabmonoid: IAbMonoid grp_op: * grp_car: |g|
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: or: P ∨ Q so_lambda: λ2x.t[x] so_apply: x[s] cons: [a b] le: A ≤ B less_than': less_than'(a;b) colength: colength(L) nil: [] it: guard: {T} sq_type: SQType(T) less_than: a < b squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] decidable: Dec(P) subtype_rel: A ⊆B iabmonoid: IAbMonoid imon: IMonoid true: True iff: ⇐⇒ Q rev_implies:  Q infix_ap: y
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf list-cases mon_for_nil_lemma product_subtype_list colength-cons-not-zero colength_wf_list istype-false le_wf list_wf subtract-1-ge-0 subtype_base_sq intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf intformnot_wf itermSubtract_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_subtract_lemma int_term_value_add_lemma decidable__le mon_for_cons_lemma nat_wf istype-universe grp_car_wf iabmonoid_wf grp_id_wf equal_wf squash_wf true_wf mon_ident subtype_rel_self iff_weakening_equal grp_op_wf infix_ap_wf mon_for_wf mon_assoc abmonoid_ac_1 abmonoid_comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType axiomEquality functionIsTypeImplies inhabitedIsType unionElimination promote_hyp hypothesis_subsumption productElimination equalityIsType1 because_Cache dependent_set_memberEquality_alt instantiate equalityTransitivity equalitySymmetry applyLambdaEquality imageElimination equalityIsType4 baseApply closedConclusion baseClosed applyEquality intEquality functionIsType universeEquality imageMemberEquality

Latex:
\mforall{}g:IAbMonoid.  \mforall{}A:Type.  \mforall{}e,f:A  {}\mrightarrow{}  |g|.  \mforall{}as:A  List.
    ((For\{g\}  x  \mmember{}  as.  (e[x]  *  f[x]))  =  ((For\{g\}  x  \mmember{}  as.  e[x])  *  (For\{g\}  x  \mmember{}  as.  f[x])))



Date html generated: 2019_10_16-PM-01_02_44
Last ObjectModification: 2018_10_08-PM-00_29_16

Theory : list_2


Home Index