Nuprl Lemma : mset_ind_a
∀s:DSet. ∀Q:MSet{s} ⟶ ℙ.
((∀w:MSet{s}. SqStable(Q[w]))
⇒ Q[0{s}]
⇒ (∀x:|s|. Q[mset_inj{s}(x)])
⇒ (∀ys,ys':MSet{s}. (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys']))
⇒ {∀zs:MSet{s}. Q[zs]})
Proof
Definitions occuring in Statement :
mset_sum: a + b,
mset_inj: mset_inj{s}(x),
null_mset: 0{s},
mset: MSet{s},
sq_stable: SqStable(P),
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
dset: DSet,
sq_stable: SqStable(P),
mset: MSet{s},
quotient: x,y:A//B[x; y],
and: P ∧ Q,
squash: ↓T,
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
null_mset: 0{s},
mset_inj: mset_inj{s}(x),
mset_sum: a + b,
mk_mset: mk_mset(as),
append: as @ bs,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3]
Lemmas referenced :
mset_wf,
all_wf,
mset_sum_wf,
set_car_wf,
mset_inj_wf,
null_mset_wf,
sq_stable_wf,
dset_wf,
squash_wf,
list_wf,
permr_wf,
equal_wf,
equal-wf-base,
list_induction,
subtype_quotient,
permr_equiv_rel,
list_ind_cons_lemma,
list_ind_nil_lemma
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
isectElimination,
lambdaEquality,
functionEquality,
applyEquality,
functionExtensionality,
setElimination,
rename,
because_Cache,
cumulativity,
universeEquality,
independent_functionElimination,
pointwiseFunctionalityForEquality,
pertypeElimination,
productElimination,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
baseClosed,
productEquality,
independent_isectElimination,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}s:DSet. \mforall{}Q:MSet\{s\} {}\mrightarrow{} \mBbbP{}.
((\mforall{}w:MSet\{s\}. SqStable(Q[w]))
{}\mRightarrow{} Q[0\{s\}]
{}\mRightarrow{} (\mforall{}x:|s|. Q[mset\_inj\{s\}(x)])
{}\mRightarrow{} (\mforall{}ys,ys':MSet\{s\}. (Q[ys] {}\mRightarrow{} Q[ys'] {}\mRightarrow{} Q[ys + ys']))
{}\mRightarrow{} \{\mforall{}zs:MSet\{s\}. Q[zs]\})
Date html generated:
2017_10_01-AM-10_00_13
Last ObjectModification:
2017_03_03-PM-01_01_53
Theory : mset
Home
Index