Nuprl Lemma : es-threshold-val2

{

[Info:Type].

[es:EO+(Info)].

[A:Type].

[X:EClass(A)].

[S:Type].

[init:S].

[f:S

A

S].

[test:S

A

].

[nxt:S

A

S].

[e:E].
(

e

X)

(Threshold(init;f;test;nxt;X)(e)
= <if e

prior(Threshold(init;f;test;nxt;X))
         then let e' = prior(Threshold(init;f;test;nxt;X))(e) in
                  list_accum(s,v.f s v;
                             nxt Threshold(init;f;test;nxt;X)(e');
                             X(e', e))
         else list_accum(s,v.f s v;init;X(<e))
         fi
        , X(e)
        >)
    supposing

e

Threshold(init;f;test;nxt;X) }

{ Proof }

Definitions occuring in Statement : es-threshold: Threshold(init;f;test;nxt;X), es-prior-interface: prior(X), es-prior-interval-vals: X(e1, e2), es-prior-interface-vals: X(<e), eclass-val: X(e), in-eclass: e

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

b, ifthenelse: if b then t else f fi , bool:

, let: let, uimplies: b supposing a, uall:

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

Q, apply: f a, function: x:A

B[x], pair: <a, b>, product: x:A

B[x], universe: Type, equal: s = t, list_accum: list_accum(x,a.f[x; a];y;l)
Definitions : rev_implies: P

Q, iff: P

Q, pi1: fst(t), cand: A c

B, intensional-universe: IType, IdLnk: IdLnk, rationals:

, append: as @ bs, locl: locl(a), Knd: Knd, sq_type: SQType(T), es-local-pred: last(P), es-rec-class: es-rec-class, fpf-cap: f(x)?z, filter: filter(P;l), list: type List, bag_only_single: bag_only_single{bag_only_single_compseq_tag_def:o}(x), set_eq: =

, set_le:

, grp_eq: =

, rng_eq: =

, bag_size_empty: bag_size_empty{bag_size_empty_compseq_tag_def:o}, natural_number: $n, bag-size: bag-size(bs), bag-only: only(bs), fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), le: A

B, ge: i

j , less_than: a < b, es-loc: loc(e), Id: Id, es-causl: (e < e'), es-locl: (e <loc e'), cond-class: [X?Y], eq_knd: a = b, fpf-dom: x

dom(f), limited-type: LimitedType, bfalse: ff, btrue: tt, uiff: uiff(P;Q), eq_bool: p =b q, lt_int: i <z j, le_int: i

z j, eq_int: (i =

j), null: null(as), set_blt: a <

b, grp_blt: a <

b, infix_ap: x f y, dcdr-to-bool: [d]

, bl-all: (

x

L.P[x])_b, bl-exists: (

x

L.P[x])_b, b-exists: (

i<n.P[i])_b, eq_type: eq_type(T;T'), not:

A, qeq: qeq(r;s), q_less: q_less(r;s), q_le: q_le(r;s), deq-member: deq-member(eq;x;L), deq-disjoint: deq-disjoint(eq;as;bs), deq-all-disjoint: deq-all-disjoint(eq;ass;bs), eq_id: a = b, eq_lnk: a = b, es-eq-E: e = e', es-bless: e <loc e', es-ble: e

loc e', bimplies: p

q, band: p

q, bor: p

q, bnot:

b, int:

, unit: Unit, so_apply: x[s], union: left + right, or: P

Q, guard: {T}, l_member: (x

l), subtype: S

T, atom: Atom, es-base-E: es-base-E(es), token: "$token", es-E-interface: E(X), subtype_rel: A

r B, quotient: x,y:A//B[x; y], top: Top, all:

x:A. B[x], dep-isect: Error :dep-isect, eq_atom: x =a y, eq_atom: eq_atom$n(x;y), record+: record+, bag: bag(T), set: {x:A| B[x]} , record-select: r.x, axiom: Ax, lambda:

x.A[x], es-prior-interface: prior(X), es-threshold: Threshold(init;f;test;nxt;X), implies: P

Q, prop:

, event_ordering: EO, es-E: E, bool:

, function: x:A

B[x], uimplies: b supposing a, and: P

Q, assert:

b, decide: case b of inl(x) => s[x] | inr(y) => t[y], true: True, false: False, void: Void, equal: s = t, event-ordering+: EO+(Info), eclass: EClass(A[eo; e]), uall:

[x:A]. B[x], universe: Type, member: t

T, isect:

x:A. B[x], sqequal: s ~ t, squash:

T, record: record(x.T[x]), so_lambda:

x.t[x], in-eclass: e

X, empty-bag: {}, pair: <a, b>, single-bag: {x}, apply: f a, ifthenelse: if b then t else f fi , es-prior-interval-vals: X(e1, e2), list_accum: list_accum(x,a.f[x; a];y;l), let: let, eclass-val: X(e), so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]), es-prior-interface-vals: X(<e), so_lambda:

x y.t[x; y], product: x:A

B[x]
Lemmas : set_subtype_base, squash_wf, top_wf, subtype_rel_wf, event-ordering+_wf, event-ordering+_inc, subtype_rel_self, es-base-E_wf, es-E_wf, es-threshold_wf, es-interface-subtype_rel2, es-interface-top, member_wf, eclass_wf, in-eclass_wf, assert_wf, assert_witness, bool_wf, rec-class-val, bag_wf, ifthenelse_wf, single-bag_wf, empty-bag_wf, es-prior-interface-vals_wf, list_accum_wf, eclass-val_wf, eqtt_to_assert, not_wf, uiff_transitivity, eqff_to_assert, assert_of_bnot, bnot_wf, es-locl_wf, es-prior-interval-vals_wf, es-prior-interface_wf1, bag-only_wf, false_wf, true_wf, bag-size_wf, es-prior-interface_wf, es-E-interface_wf, list-subtype, l_member_wf, eclass-val_wf2, es-interface-val_wf2, es-interface-val_wf, assert_elim, subtype_base_sq, bool_subtype_base, intensional-universe_wf, is-threshold, bool_cases, btrue_neq_bfalse, not_assert_elim

\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A:Type]. \mforall{}[X:EClass(A)]. \mforall{}[S:Type]. \mforall{}[init:S]. \mforall{}[f:S {}\mrightarrow{} A {}\mrightarrow{} S]. \mforall{}[test:S {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{}]. \mforall{}[nxt:S \mtimes{} A {}\mrightarrow{} S]. \mforall{}[e:E]. (\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (Threshold(init;f;test;nxt;X)(e) = <if e \mmember{}\msubb{} prior(Threshold(init;f;test;nxt;X)) then let e' = prior(Threshold(init;f;test;nxt;X))(e) in list\_accum(s,v.f s v;nxt Threshold(init;f;test;nxt;X)(e');X(e', e)) else list\_accum(s,v.f s v;init;X(<e)) fi , X(e) >) supposing \muparrow{}e \mmember{}\msubb{} Threshold(init;f;test;nxt;X) Date html generated: 2011_08_16-PM-05_11_29 Last ObjectModification: 2011_06_20-AM-01_13_30 Home Index