Nuprl Lemma : decidable__existse-causl

{

es:EO

[P:E

]

j:E. ((

e:E. ((e < j)

Dec(P[e])))

Dec(

k:E. ((k < j)

P[k]))) }

{ Proof }

Definitions occuring in Statement : es-causl: (e < e'), es-E: E, event_ordering: EO, decidable: Dec(P), uall:

[x:A]. B[x], prop:

, so_apply: x[s], all:

x:A. B[x], exists:

x:A. B[x], implies: P

Q, and: P

Q, function: x:A

B[x]
Definitions : rel_finite: rel_finite(T;R), member: t

T, strong-subtype: strong-subtype(A;B), eq_atom: x =a y, eq_atom: eq_atom$n(x;y), record-select: r.x, set: {x:A| B[x]} , dep-isect: Error :dep-isect, record+: record+, ge: i

j , uimplies: b supposing a, uiff: uiff(P;Q), subtype_rel: A

r B, false: False, iff: P

Q, less_than: a < b, le: A

B, assert:

b, int_seg: {i..j

}, divides: b | a, assoced: a ~ b, set_leq: a

b, set_lt: a <p b, grp_lt: a < b, cand: A c

B, l_member: (x

l), l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), fun-connected: y is f*(x), qle: r

s, qless: r < s, q-rel: q-rel(r;x), list: type List, i-finite: i-finite(I), i-closed: i-closed(I), p-outcome: Outcome, fset-member: a

s, f-subset: xs

ys, fset-closed: (s closed under fs), l_disjoint: l_disjoint(T;l1;l2), cs-not-completed: in state s, a has not completed inning i, cs-archived: by state s, a archived v in inning i, cs-passed: by state s, a passed inning i without archiving a value, cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-precondition: state s may consider v in inning i, cs-inning-committed: in state s, inning i has committed v, not:

A, cs-inning-committable: in state s, inning i could commit v , nat:

, infix_ap: x f y, equal: s = t, es-locl: (e <loc e'), es-le: e

loc e' , es-causle: e c

e', uall:

[x:A]. B[x], isect:

x:A. B[x], universe: Type, implies: P

Q, prop:

, or: P

Q, union: left + right, all:

x:A. B[x], function: x:A

B[x], event_ordering: EO, decidable: Dec(P), exists:

x:A. B[x], and: P

Q, product: x:A

B[x], so_apply: x[s], apply: f a, Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, Complete: Error :Complete, Try: Error :Try, es-causl: (e < e'), lambda:

x.A[x], es-E: E, THENM: Error :THENM
Lemmas : not_wf, event_ordering_wf, decidable__exists-rel_finite, rel_finite_wf, l_member_wf, es-causl-rel_finite, es-E_wf, es-causl_wf, decidable_wf, decidable__es-causl

\mforall{}es:EO. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}]. \mforall{}j:E. ((\mforall{}e:E. ((e < j) {}\mRightarrow{} Dec(P[e]))) {}\mRightarrow{} Dec(\mexists{}k:E. ((k < j) \mwedge{} P[k]))) Date html generated: 2011_08_16-AM-10_35_33 Last ObjectModification: 2011_06_18-AM-09_15_26 Home Index