### Nuprl Lemma : mon_reduce_functionality_wrt_permr

`∀g:IAbMonoid. ∀xs,ys:|g| List.  ((xs ≡(|g|) ys) `` ((Π xs) = (Π ys) ∈ |g|))`

Proof

Definitions occuring in Statement :  mon_reduce: mon_reduce permr: `as ≡(T) bs` list: `T List` all: `∀x:A. B[x]` implies: `P `` Q` equal: `s = t ∈ T` iabmonoid: `IAbMonoid` grp_car: `|g|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` iabmonoid: `IAbMonoid` imon: `IMonoid` prop: `ℙ` permr: `as ≡(T) bs` cand: `A c∧ B` exists: `∃x:A. B[x]` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` so_apply: `x[s]` sym_grp: `Sym(n)` perm: `Perm(T)` ge: `i ≥ j ` nat: `ℕ` less_than: `a < b`
Lemmas referenced :  permr_wf grp_car_wf list_wf iabmonoid_wf equal_wf squash_wf true_wf istype-universe mon_reduce_eq_itop subtype_rel_self iff_weakening_equal mon_itop_wf select_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf length_wf intformeq_wf int_formula_prop_eq_lemma le_wf less_than_wf imon_wf length_wf_nat perm_f_wf non_neg_length nat_properties mon_itop_perm_invar
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut hypothesis universeIsType introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination setElimination rename because_Cache hypothesisEquality inhabitedIsType productElimination natural_numberEquality applyEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry universeEquality sqequalRule imageMemberEquality baseClosed instantiate independent_isectElimination independent_functionElimination unionElimination approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation dependent_set_memberEquality_alt productIsType functionIsType applyLambdaEquality

Latex:
\mforall{}g:IAbMonoid.  \mforall{}xs,ys:|g|  List.    ((xs  \mequiv{}(|g|)  ys)  {}\mRightarrow{}  ((\mPi{}  xs)  =  (\mPi{}  ys)))

Date html generated: 2019_10_16-PM-01_02_26
Last ObjectModification: 2018_10_08-AM-11_42_17

Theory : list_2

Home Index