Nuprl Lemma : sq_stable_

{

[Info,T:Type].

[X:EClass(T)].

[es:EO+(Info)].

[e:E].

[v:T].
SqStable(v

X(e)) }

{ Proof }

Definitions occuring in Statement : classrel: v

X(e), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, sq_stable: SqStable(P), uall:

[x:A]. B[x], universe: Type
Definitions : lambda:

x.A[x], subtype: S

T, member: t

T, union: left + right, or: P

Q, false: False, less_than: a < b, le: A

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, cmp-le: cmp-le(cmp;x;y), reducible: reducible(a), prime: prime(a), 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), sq_exists:

x:{A| B[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], es-fset-loc: i

locs(s), 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'), decidable: Dec(P), uimplies: b supposing a, iff: P

Q, product: x:A

B[x], and: P

Q, uiff: uiff(P;Q), equal: s = t, not:

A, uni_sat: a = !x:T. Q[x], inv_funs: InvFuns(A;B;f;g), inject: Inj(A;B;f), eqfun_p: IsEqFun(T;eq), refl: Refl(T;x,y.E[x; y]), urefl: UniformlyRefl(T;x,y.E[x; y]), sym: Sym(T;x,y.E[x; y]), usym: UniformlySym(T;x,y.E[x; y]), trans: Trans(T;x,y.E[x; y]), utrans: UniformlyTrans(T;x,y.E[x; y]), anti_sym: AntiSym(T;x,y.R[x; y]), uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]), connex: Connex(T;x,y.R[x; y]), uconnex: uconnex(T; x,y.R[x; y]), coprime: CoPrime(a,b), ident: Ident(T;op;id), assoc: Assoc(T;op), comm: Comm(T;op), inverse: Inverse(T;op;id;inv), bilinear: BiLinear(T;pl;tm), bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f), action_p: IsAction(A;x;e;S;f), dist_1op_2op_lr: Dist1op2opLR(A;1op;2op), fun_thru_1op: fun_thru_1op(A;B;opa;opb;f), fun_thru_2op: FunThru2op(A;B;opa;opb;f), cancel: Cancel(T;S;op), monot: monot(T;x,y.R[x; y];f), monoid_p: IsMonoid(T;op;id), group_p: IsGroup(T;op;id;inv), monoid_hom_p: IsMonHom{M1,M2}(f), grp_leq: a

b, integ_dom_p: IsIntegDom(r), prime_ideal_p: IsPrimeIdeal(R;P), no_repeats: no_repeats(T;l), value-type: value-type(T), valueall-type: valueall-type(T), assert:

b, is_list_splitting: is_list_splitting(T;L;LL;L2;f), is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x), req: x = y, rnonneg: rnonneg(r), rleq: x

y, i-member: r

I, partitions: partitions(I;p), modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f), subtype_rel: A

r B, strong-subtype: strong-subtype(A;B), fpf-sub: f

g, all:

x:A. B[x], event_ordering: EO, universe: Type, so_lambda:

x y.t[x; y], eclass: EClass(A[eo; e]), bag: bag(T), quotient: x,y:A//B[x; y], sq_stable: SqStable(P), implies: P

Q, function: x:A

B[x], classrel: v

X(e), bag-member: bag-member(T;x;bs), squash:

T, set: {x:A| B[x]} , event-ordering+: EO+(Info), record+: record+, dep-isect: Error :dep-isect, uall:

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

x:A. B[x], es-E: E, Auto: Error :Auto, Unfold: Error :Unfold, CollapseTHEN: Error :CollapseTHEN, tactic: Error :tactic
Lemmas : classrel_wf, sq_stable_from_decidable, eclass_wf, event-ordering+_inc, bag-member_wf, sq_stable_wf, sq_stable__bag-member, member_wf, bag_wf, es-E_wf, event-ordering+_wf

\mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:T]. SqStable(v \mmember{} X(e)) Date html generated: 2011_08_16-AM-11_29_31 Last ObjectModification: 2011_05_23-PM-07_35_02 Home Index