Nuprl Lemma : cut-list-maximal-exists
∀[Info:Type]
∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀a:E(X) List.
((¬(a = {} ∈ fset(E(X))))
⇒ (∃e:E(X)
((e ∈ a)
∧ (∀e':E(X). ((e' ∈ a) ⇒ (e = (X-pred e') ∈ E(X)) ⇒ (e' = e ∈ E(X))))
∧ (∀e':E(X). ((e' ∈ a) ⇒ (e = (f e') ∈ E(X)) ⇒ (e' = e ∈ E(X)))))))
Proof
Definitions occuring in Statement :
es-interface-pred: X-pred,
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
empty-fset: {},
fset: fset(T),
l_member: (x ∈ l),
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
universe: Type,
equal: s = t ∈ T
Lemmas :
es-E-interface_wf,
list-cases,
product_subtype_list,
not_wf,
equal-wf-T-base,
fset_wf,
subtype_rel_quotient_trivial,
list_wf,
set-equal_wf,
set-equal-equiv,
sys-antecedent_wf,
eclass_wf,
top_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
empty-fset_wf,
l_exists_iff,
cons_wf,
l_member_wf,
l_all_wf2,
es-interface-pred_wf2,
decidable__l_exists_better-extract,
decidable__cand,
decidable__l_all-better-extract,
decidable__implies_better,
equal_wf,
decidable__equal_es-E-interface,
set_wf,
l_all_iff,
all_wf,
exists_wf,
or_wf,
l_exists_wf,
not-l_exists,
l_all_functionality,
not_over_and,
not-l_all-dec,
l_exists_functionality,
not_over_implies,
not_over_not,
l_exists_or,
es-causl-max-list,
subtype_rel_list,
length_wf,
non_neg_length,
length_wf_nat,
length_cons,
sq_stable__l_member,
decidable__es-E-equal,
assert_wf,
in-eclass_wf,
es-E-interface-property,
select_wf,
sq_stable__le,
less_than_wf,
member_wf,
l_member_subtype,
es-causl_wf,
squash_wf,
true_wf,
event_ordering_wf,
iff_weakening_equal,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
es-prior-interface_wf0,
eqtt_to_assert,
eqff_to_assert,
es-interface-subtype_rel2,
subtype_top,
bool_cases_sqequal,
assert-bnot,
es-causle_weakening_eq,
es-causle_wf,
es-prior-interface-causl,
eclass-val_wf2,
es-prior-interface_wf,
sq_stable__es-causle
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:sys-antecedent(es;X). \mforall{}a:E(X) List.
((\mneg{}(a = \{\}))
{}\mRightarrow{} (\mexists{}e:E(X)
((e \mmember{} a)
\mwedge{} (\mforall{}e':E(X). ((e' \mmember{} a) {}\mRightarrow{} (e = (X-pred e')) {}\mRightarrow{} (e' = e)))
\mwedge{} (\mforall{}e':E(X). ((e' \mmember{} a) {}\mRightarrow{} (e = (f e')) {}\mRightarrow{} (e' = e))))))
Date html generated:
2015_07_21-PM-04_01_59
Last ObjectModification:
2015_02_04-PM-06_09_43
Home
Index