### Nuprl Lemma : count_functionality

`∀s:DSet. ∀a,a':|s|. ∀bs,bs':|s| List.  ((a = a' ∈ |s|) `` (bs ≡(|s|) bs') `` ((a #∈ bs) = (a' #∈ bs') ∈ ℤ))`

Proof

Definitions occuring in Statement :  count: `a #∈ as` permr: `as ≡(T) bs` list: `T List` all: `∀x:A. B[x]` implies: `P `` Q` int: `ℤ` equal: `s = t ∈ T` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` count: `a #∈ as` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` dset: `DSet` subtype_rel: `A ⊆r B` abgrp: `AbGrp` grp: `Group{i}` mon: `Mon` iabmonoid: `IAbMonoid` imon: `IMonoid` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` infix_ap: `x f y` grp_car: `|g|` pi1: `fst(t)` int_add_grp: `<ℤ+>` guard: `{T}` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  permr_wf set_car_wf equal_wf int_add_grp_wf subtype_rel_sets grp_sig_wf monoid_p_wf grp_car_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf comm_wf set_wf b2i_wf set_eq_wf subtype_rel_self mon_subtype_grp_sig grp_subtype_mon abgrp_subtype_grp subtype_rel_transitivity abgrp_wf grp_wf mon_wf mem_f_wf mon_for_wf squash_wf true_wf mon_for_functionality_wrt_permr bool_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination setElimination rename because_Cache hypothesisEquality intEquality applyEquality sqequalRule instantiate setEquality cumulativity lambdaEquality independent_isectElimination natural_numberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality independent_functionElimination imageMemberEquality baseClosed productElimination

Latex:
\mforall{}s:DSet.  \mforall{}a,a':|s|.  \mforall{}bs,bs':|s|  List.    ((a  =  a')  {}\mRightarrow{}  (bs  \mequiv{}(|s|)  bs')  {}\mRightarrow{}  ((a  \#\mmember{}  bs)  =  (a'  \#\mmember{}  bs')))

Date html generated: 2018_05_22-AM-07_45_20
Last ObjectModification: 2018_05_19-AM-08_32_28

Theory : list_2

Home Index