Nuprl Lemma : bag-maximal?-cons
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,v:T]. uiff(↑bag-maximal?(v.b;x;R);(↑bag-maximal?(b;x;R)) ∧ (↑(R x v)))
Proof
Definitions occuring in Statement :
bag-maximal?: bag-maximal?(bg;x;R)
,
cons-bag: x.b
,
bag: bag(T)
,
assert: ↑b
,
bool: 𝔹
,
uiff: uiff(P;Q)
,
uall: ∀[x:A]. B[x]
,
and: P ∧ Q
,
apply: f a
,
function: x:A ⟶ B[x]
,
universe: Type
Definitions unfolded in proof :
single-bag: {x}
,
bag-append: as + bs
,
cons-bag: x.b
,
append: as @ bs
,
all: ∀x:A. B[x]
,
so_lambda: so_lambda(x,y,z.t[x; y; z])
,
member: t ∈ T
,
top: Top
,
so_apply: x[s1;s2;s3]
,
uiff: uiff(P;Q)
,
and: P ∧ Q
,
uimplies: b supposing a
,
uall: ∀[x:A]. B[x]
,
implies: P
⇒ Q
,
prop: ℙ
,
rev_uimplies: rev_uimplies(P;Q)
,
iff: P
⇐⇒ Q
,
rev_implies: P
⇐ Q
Lemmas referenced :
list_ind_cons_lemma,
list_ind_nil_lemma,
bag-maximal?-single,
assert_witness,
bag-maximal?_wf,
single-bag_wf,
and_wf,
assert_wf,
iff_weakening_uiff,
bag-append_wf,
bag-maximal?-append,
uiff_wf,
cons-bag_wf,
bool_wf,
bag_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
independent_pairFormation,
isect_memberFormation,
introduction,
productElimination,
isectElimination,
hypothesisEquality,
independent_isectElimination,
independent_pairEquality,
independent_functionElimination,
applyEquality,
because_Cache,
addLevel,
cumulativity,
functionEquality,
universeEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T:Type]. \mforall{}[b:bag(T)]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}]. \mforall{}[x,v:T].
uiff(\muparrow{}bag-maximal?(v.b;x;R);(\muparrow{}bag-maximal?(b;x;R)) \mwedge{} (\muparrow{}(R x v)))
Date html generated:
2016_05_15-PM-02_30_36
Last ObjectModification:
2015_12_27-AM-09_48_48
Theory : bags
Home
Index