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 s 
X*(f,init,pred(e)) (v:T. (v X(e) P[v;s])))))
Proof not projected
Definitions occuring in Statement :
iterated_classrel: v X*(f,init,e),
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)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
prop: ,
implies: P Q,
so_apply: x[s1;s2],
member: t T,
nat: 
,
ge: i 
j ,
le: A B,
not: 
A,
false: False,
squash: 
T,
true: True,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
decidable: Dec(P),
exists: x:A. B[x],
and: P Q,
assert: 
b,
or: P 
Q,
btrue: tt,
bfalse: ff,
cand: A c B,
ifthenelse: if b then t else f fi ,
es-le: e loc e' ,
classrel: v X(e),
guard: {T},
bag-member: x bs,
iff: P 
Q,
rev_implies: P Q,
strongwellfounded: SWellFounded(R[x; y]),
so_apply: x[s],
uimplies: b supposing a,
sq_type: SQType(T),
single-valued-classrel: single-valued-classrel(es;X;T),
es-locl: (e <loc e'),
subtype: S 
T
Lemmas :
es-causl-swellfnd,
nat_properties,
ge_wf,
less_than_wf,
nat_wf,
le_wf,
es-causl_wf,
decidable__equal_Id,
es-loc_wf,
decidable__exists-single-valued-classrel,
equal_wf,
all_wf,
decidable_wf,
single-valued-bag_wf,
event-ordering+_inc,
single-valued-classrel_wf,
es-E_wf,
event-ordering+_wf,
eclass_wf,
Id_wf,
bag_wf,
decidable__assert,
es-first_wf,
btrue_neq_bfalse,
exists_wf,
es-locl_wf,
es-le_wf,
iterated_classrel_wf,
es-pred_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
false_wf,
classrel_wf,
es-locl-first,
assert_elim,
es-le-first,
and_wf,
ifthenelse_wf,
es-pred-causl,
es-pred-locl,
es-locl_transitivity1,
es-le_weakening,
not_wf,
not_assert_elim,
assert_wf,
decidable__exists_iterated_classrel,
es-loc-pred,
es-locl-trichotomy,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
implies-es-le-pred,
squash_wf,
true_wf,
event_ordering_wf,
iterated_classrel-single-val,
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{} s \mmember{} X*(f,init,pred(e)) \mwedge{} (\mexists{}v:T. (v \mmember{} X(e) \mwedge{} P[v;s])))))
Date html generated:
2012_01_23-PM-12_20_17
Last ObjectModification:
2012_01_18-AM-10_20_57
Home
Index