Nuprl Lemma : decidable__exists-iterated-classrel-between3-sv
∀[Info,T,S:Type].
∀init:Id ─→ bag(S). ∀f:T ─→ S ─→ S. ∀X:EClass(T). ∀es:EO+(Info). ∀P:T ─→ S ─→ ℙ. ∀e1,e2:E.
(single-valued-classrel(es;X;T)
⇒ single-valued-bag(init loc(e1);S)
⇒ (∀v:T. ∀s:S. Dec(P[v;s]))
⇒ Dec(∃e:E
∃s:S
((e1 <loc e) ∧ e ≤loc e2 ∧ iterated_classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s])))))
Proof
Definitions occuring in Statement :
iterated_classrel: iterated_classrel(es;S;A;f;init;X;e;v),
single-valued-classrel: single-valued-classrel(es;X;T),
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
Id: Id,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
single-valued-bag: single-valued-bag(b;T),
bag: bag(T)
Lemmas :
decidable__assert,
es-first_wf2,
event-ordering+_subtype,
es-locl-first,
assert_elim,
and_wf,
equal_wf,
bool_wf,
ifthenelse_wf,
es-E_wf,
es-le-first,
btrue_neq_bfalse,
exists_wf,
es-locl_wf,
es-le_wf,
iterated_classrel_wf,
es-pred_wf,
classrel_wf,
es-pred-locl,
es-causl_weakening,
es-locl_transitivity1,
es-le_weakening,
assert_wf,
not_wf,
decidable__exists_iterated_classrel,
es-loc-pred,
Id_wf,
bag_wf,
single-valued-bag_wf,
es-locl-trichotomy,
es-le-self,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
es-le-pred,
squash_wf,
true_wf,
event-ordering+_wf,
eclass_wf,
not_assert_elim,
iff_weakening_equal,
iterated_classrel-single-val,
subtype_base_sq,
bool_subtype_base,
false_wf,
event_ordering_wf,
es-le-loc
\mforall{}[Info,T,S:Type].
\mforall{}init:Id {}\mrightarrow{} bag(S). \mforall{}f:T {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}X:EClass(T). \mforall{}es:EO+(Info). \mforall{}P:T {}\mrightarrow{} S {}\mrightarrow{} \mBbbP{}. \mforall{}e1,e2:E.
(single-valued-classrel(es;X;T)
{}\mRightarrow{} single-valued-bag(init loc(e1);S)
{}\mRightarrow{} (\mforall{}v:T. \mforall{}s:S. Dec(P[v;s]))
{}\mRightarrow{} Dec(\mexists{}e:E
\mexists{}s:S
((e1 <loc e)
\mwedge{} e \mleq{}loc e2
\mwedge{} iterated\_classrel(es;S;T;f;init;X;pred(e);s)
\mwedge{} (\mexists{}v:T. (v \mmember{} X(e) \mwedge{} P[v;s])))))
Date html generated:
2015_07_17-PM-00_23_42
Last ObjectModification:
2015_02_04-PM-05_36_54
Home
Index