Nuprl Lemma : decidable__cut-order

{

[Info:Type]

es:EO+(Info).

X:EClass(Top).

f:sys-antecedent(es;X).

a,b:E(X).
Dec(a

(X;f) b) }

{ Proof }

Definitions occuring in Statement : cut-order: a

(X;f) b, sys-antecedent: sys-antecedent(es;Sys), es-E-interface: E(X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), decidable: Dec(P), uall:

[x:A]. B[x], top: Top, all:

x:A. B[x], universe: Type
Definitions : list: type List, nil: [], es-interface-pred: X-pred, cons: [car / cdr], fpf-cap: f(x)?z, fpf: a:A fp-> B[a], quotient: x,y:A//B[x; y], fset-singleton: {x}, es-eq: es-eq(es), es-cut: Cut(X;f), fset: FSet{T}, cut-of: cut(X;f;s), subtype: S

T, top: Top, event_ordering: EO, es-E: E, lambda:

x.A[x], member: t

T, strong-subtype: strong-subtype(A;B), eq_atom: x =a y, eq_atom: eq_atom$n(x;y), decide: case b of inl(x) => s[x] | inr(y) => t[y], ifthenelse: if b then t else f fi , set: {x:A| B[x]} , dep-isect: Error :dep-isect, record+: record+, ge: i

j , uiff: uiff(P;Q), subtype_rel: A

r B, prop:

, false: False, not:

A, and: P

Q, iff: P

Q, less_than: a < b, le: A

B, assert:

b, 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), 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-inning-committed: in state s, inning i has committed v, cs-inning-committable: in state s, inning i could commit v , 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, infix_ap: x f y, es-causl: (e < e'), es-locl: (e <loc e'), es-le: e

loc e' , es-causle: e c

e', existse-before:

e<e'.P[e], existse-le:

e

e'.P[e], alle-lt:

e<e'.P[e], alle-le:

e

e'.P[e], alle-between1:

e

[e1,e2).P[e], existse-between1:

e

[e1,e2).P[e], alle-between2:

e

[e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], existse-between3:

e

(e1,e2].P[e], uimplies: b supposing a, es-fset-loc: i

locs(s), product: x:A

B[x], exists:

x:A. B[x], apply: f a, es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), implies: P

Q, equal: s = t, collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), so_lambda:

x y.t[x; y], or: P

Q, union: left + right, es-E-interface: E(X), sys-antecedent: sys-antecedent(es;Sys), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), universe: Type, cut-order: a

(X;f) b, decidable: Dec(P), uall:

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

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

B[x], all:

x:A. B[x], MaAuto: Error :MaAuto, CollapseTHEN: Error :CollapseTHEN, Auto: Error :Auto, Unfold: Error :Unfold, tactic: Error :tactic
Lemmas : es-E-interface_wf, subtype_rel_wf, es-cut_wf, fset_wf, fset-singleton_wf, cut-of_wf, member_wf, es-eq_wf-interface, decidable__fset-member, decidable_wf, fset-member_wf, event-ordering+_wf, event-ordering+_inc, es-E_wf, top_wf, eclass_wf, sys-antecedent_wf, cut-order_wf, not_wf, fset-closed_wf, es-interface-pred_wf2

\mforall{}[Info:Type]. \mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:sys-antecedent(es;X). \mforall{}a,b:E(X). Dec(a \mleq{}(X;f) b) Date html generated: 2011_08_16-PM-05_50_49 Last ObjectModification: 2011_06_20-AM-01_36_14 Home Index