Nuprl Lemma : state-class2-inv
∀[Info,B,A1,A2:Type].
∀init:Id ─→ B. ∀tr1:Id ─→ A1 ─→ B ─→ B. ∀tr2:Id ─→ A2 ─→ B ─→ B. ∀X1:EClass(A1). ∀X2:EClass(A2). ∀es:EO+(Info). ∀e:E.
∀P:E ─→ B ─→ ℙ. ∀v:B.
(single-valued-classrel(es;X1;A1)
⇒ single-valued-classrel(es;X2;A2)
⇒ disjoint-classrel(es;A1;X1;A2;X2)
⇒ (∀s:B. ∀e':E.
(e' ≤loc e
⇒ if first(e')
then s = (init loc(e')) ∈ B
else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
fi
⇒ if e' ∈b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
if e' ∈b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
else P[e';s]
fi ))
⇒ v ∈ state-class2(init;tr1;X1;tr2;X2)(e)
⇒ P[e;v])
Proof
Definitions occuring in Statement :
state-class2: state-class2(init;tr1;X1;tr2;X2),
single-valued-classrel: single-valued-classrel(es;X;T),
disjoint-classrel: disjoint-classrel(es;A;X;B;Y),
classrel: v ∈ X(e),
member-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-first: first(e),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
Id: Id,
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
es-causl-swellfnd,
event-ordering+_subtype,
less_than_transitivity1,
less_than_irreflexivity,
int_seg_wf,
decidable__equal_int,
subtype_rel-int_seg,
false_wf,
le_weakening,
subtract_wf,
int_seg_properties,
le_wf,
nat_wf,
zero-le-nat,
lelt_wf,
es-causl_wf,
classrel-classfun,
loop-class-state-functional,
single-bag_wf,
Id_wf,
parallel-class_wf,
eclass1_wf,
bag_size_single_lemma,
parallel-class-single-val,
eclass1-disjoint-classrel,
disjoint-classrel-symm,
eclass1-single-val,
single-valued-bag-single,
iff_weakening_equal,
state-class2-fun-eq,
member-eclass_wf,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
classrel_wf,
state-class2_wf,
all_wf,
es-E_wf,
es-le_wf,
es-first_wf2,
es-loc_wf,
es-pred_wf,
int_seg_subtype-nat,
decidable__lt,
not-equal-2,
condition-implies-le,
minus-add,
minus-minus,
minus-one-mul,
add-swap,
add-commutes,
add-associates,
add_functionality_wrt_le,
zero-add,
le-add-cancel-alt,
less-iff-le,
le-add-cancel,
set_wf,
less_than_wf,
primrec-wf2,
decidable__le,
not-le-2,
sq_stable__le,
add-zero,
add-mul-special,
zero-mul,
es-le-self,
bool_cases,
classfun-res_wf,
classrel-classfun-res-alt2,
assert_of_bnot,
classfun_wf,
es-pred-locl,
es-causl_weakening,
es-locl_transitivity1,
es-le_weakening,
classrel-classfun-res,
not_assert_elim,
and_wf,
ifthenelse_wf,
iff_imp_equal_bool,
bfalse_wf,
assert_wf
Latex:
\mforall{}[Info,B,A1,A2:Type].
\mforall{}init:Id {}\mrightarrow{} B. \mforall{}tr1:Id {}\mrightarrow{} A1 {}\mrightarrow{} B {}\mrightarrow{} B. \mforall{}tr2:Id {}\mrightarrow{} A2 {}\mrightarrow{} B {}\mrightarrow{} B. \mforall{}X1:EClass(A1). \mforall{}X2:EClass(A2).
\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}P:E {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}. \mforall{}v:B.
(single-valued-classrel(es;X1;A1)
{}\mRightarrow{} single-valued-classrel(es;X2;A2)
{}\mRightarrow{} disjoint-classrel(es;A1;X1;A2;X2)
{}\mRightarrow{} (\mforall{}s:B. \mforall{}e':E.
(e' \mleq{}loc e
{}\mRightarrow{} if first(e')
then s = (init loc(e'))
else s \mmember{} state-class2(init;tr1;X1;tr2;X2)(pred(e')) \mwedge{} P[pred(e');s]
fi
{}\mRightarrow{} if e' \mmember{}\msubb{} X1 then \mforall{}a:A1. (a \mmember{} X1(e') {}\mRightarrow{} P[e';tr1 loc(e') a s])
if e' \mmember{}\msubb{} X2 then \mforall{}a:A2. (a \mmember{} X2(e') {}\mRightarrow{} P[e';tr2 loc(e') a s])
else P[e';s]
fi ))
{}\mRightarrow{} v \mmember{} state-class2(init;tr1;X1;tr2;X2)(e)
{}\mRightarrow{} P[e;v])
Date html generated:
2015_07_23-AM-11_30_34
Last ObjectModification:
2015_02_04-PM-04_46_54
Home
Index