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