Nuprl Lemma : cut-of-singleton
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[e:E(X)].
(cut(X;f;{e})
= if e ∈b prior(X) then if f e = e then {e} else {e} ∪ cut(X;f;{f e}) fi ∪ cut(X;f;{prior(X)(e)})
if f e = e then {e}
else {e} ∪ cut(X;f;{f e})
fi
∈ Cut(X;f))
Proof
Definitions occuring in Statement :
cut-of: cut(X;f;s),
es-cut: Cut(X;f),
es-prior-interface: prior(X),
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
eclass-val: X(e),
in-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-eq-E: e = e',
es-eq: es-eq(es),
fset-singleton: {x},
fset-union: x ∪ y,
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
universe: Type,
equal: s = t ∈ T
Lemmas :
fset-closed_wf,
es-eq_wf-interface,
cons_wf,
es-interface-pred_wf2,
nil_wf,
es-E-interface_wf,
sys-antecedent_wf,
eclass_wf,
top_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
cut-of-property,
fset-singleton_wf,
in-eclass_wf,
es-prior-interface_wf0,
es-interface-subtype_rel2,
subtype_top,
bool_wf,
eqtt_to_assert,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
equal_wf,
assert-es-eq-E-2,
iff_transitivity,
bnot_wf,
not_wf,
iff_weakening_uiff,
eqff_to_assert,
assert_of_bnot,
eclass-val_wf2,
es-prior-interface_wf,
f-subset_antisymmetry,
cut-of_wf,
es-cut_wf,
fset-union_wf,
es-cut-add_wf,
member-fset-singleton,
and_wf,
assert_elim,
subtype_base_sq,
bool_subtype_base,
f-singleton-subset,
member-cut-add,
fset-member_wf-cut,
f-union-subset,
cut-of-closed,
fset_wf,
fset-union-associative,
iff_weakening_equal,
es-cut-union,
member-fset-union,
f-subset-union,
empty-fset_wf-cut,
fset-member_wf,
empty-fset_wf,
f-subset_wf,
squash_wf,
true_wf,
deq_wf,
sq_stable_from_decidable,
decidable__fset-closed
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(Top)]. \mforall{}[f:sys-antecedent(es;X)]. \mforall{}[e:E(X)].
(cut(X;f;\{e\})
= if e \mmember{}\msubb{} prior(X) then if f e = e then \{e\} else \{e\} \mcup{} cut(X;f;\{f e\}) fi \mcup{} cut(X;f;\{prior(X)(e)\})
if f e = e then \{e\}
else \{e\} \mcup{} cut(X;f;\{f e\})
fi )
Date html generated:
2015_07_21-PM-04_04_02
Last ObjectModification:
2015_02_04-PM-06_10_20
Home
Index