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