Nuprl Lemma : rec-class-val

{

[Info,T:Type].

[G:es:EO+(Info)

E

bag(T)].

[F:es:EO+(Info)

e':E

T

{e:E| (e' <loc e)}

bag(T)].

[es:EO+(Info)].

[e:E].
    RecClass(first e
               G[es;e]
             or next e after e' with value v
                 F[es;e';v;e])(e)
    = if e

prior(RecClass(first e
                               G[es;e]
                             or next e after e' with value v
                                 F[es;e';v;e]))
      then let e' = prior(RecClass(first e
                                     G[es;e]
                                   or next e after e' with value v
                                       F[es;e';v;e]))(e) in
               only(F[es;e';RecClass(first e
                                       G[es;e]
                                     or next e after e' with value v
                                         F[es;e';v;e])(e');e])
      else only(G[es;e])
      fi
    supposing

e

RecClass(first e
                               G[es;e]
                             or next e after e' with value v
                                 F[es;e';v;e]) }

{ Proof }

Definitions occuring in Statement : es-rec-class: es-rec-class, es-prior-interface: prior(X), eclass-val: X(e), in-eclass: e

X, event-ordering+: EO+(Info), es-locl: (e <loc e'), es-E: E, assert:

b, ifthenelse: if b then t else f fi , let: let, uimplies: b supposing a, uall:

[x:A]. B[x], so_apply: x[s1;s2;s3;s4], so_apply: x[s1;s2], set: {x:A| B[x]} , function: x:A

B[x], universe: Type, equal: s = t, bag-only: only(bs), bag: bag(T)
Definitions : cond-class: [X?Y], eq_knd: a = b, fpf-dom: x

dom(f), axiom: Ax, bag-only: only(bs), let: let, es-prior-interface: prior(X), eclass-val: X(e), es-loc: loc(e), pair: <a, b>, Id: Id, tag-by: z

T, rev_implies: P

Q, iff: P

Q, record: record(x.T[x]), fset: FSet{T}, dataflow: dataflow(A;B), isect2: T1

T2, b-union: A

B, true: True, fpf-cap: f(x)?z, so_apply: x[s], implies: P

Q, or: P

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

l), filter: filter(P;l), void: Void, map: map(f;as), union: left + right, bool:

, intensional-universe: IType, infix_ap: x f y, es-causl: (e < e'), strong-subtype: strong-subtype(A;B), le: A

B, ge: i

j , not:

A, less_than: a < b, product: x:A

B[x], and: P

Q, uiff: uiff(P;Q), fpf: a:A fp-> B[a], es-E-interface: E(X), decide: case b of inl(x) => s[x] | inr(y) => t[y], permutation: permutation(T;L1;L2), list: type List, quotient: x,y:A//B[x; y], lambda:

x.A[x], so_lambda:

x y.t[x; y], so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]), in-eclass: e

X, assert:

b, uimplies: b supposing a, prop:

, es-locl: (e <loc e'), set: {x:A| B[x]} , subtype: S

T, subtype_rel: A

r B, eq_atom: eq_atom$n(x;y), atom: Atom, apply: f a, top: Top, es-base-E: es-base-E(es), token: "$token", eq_atom: x =a y, ifthenelse: if b then t else f fi , record-select: r.x, dep-isect: Error :dep-isect, record+: record+, isect:

x:A. B[x], all:

x:A. B[x], uall:

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

B[x], bag: bag(T), es-E: E, event_ordering: EO, event-ordering+: EO+(Info), member: t

T, universe: Type, so_apply: x[s1;s2;s3;s4], so_apply: x[s1;s2], es-rec-class: es-rec-class, eclass: EClass(A[eo; e]), equal: s = t, false: False, lt_int: i <z j, le_int: i

z j, bfalse: ff, real:

, grp_car: |g|, nat:

, limited-type: LimitedType, btrue: tt, null: null(as), set_blt: a <

b, grp_blt: a <

b, 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'), 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, natural_number: $n, bag-size: bag-size(bs), eq_int: (i =

j), bnot:

b, int:

, unit: Unit, sq_type: SQType(T), Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, THENM: Error :THENM, CollapseTHENA: Error :CollapseTHENA, AssertBY: Error :AssertBY, tactic: Error :tactic
Lemmas : es-prior-interface-val, eq_int_eq_true, bool_subtype_base, subtype_base_sq, eclass-val_wf2, assert_elim, es-prior-interface_wf1, bool_wf, nat_wf, bag-size_wf, es-E-interface_wf, eq_int_wf, not_wf, bnot_wf, assert_of_eq_int, not_functionality_wrt_uiff, assert_of_bnot, uiff_transitivity, eqff_to_assert, eqtt_to_assert, es-interface-top, es-prior-interface_wf, es-causl_wf, Id_wf, false_wf, true_wf, assert_wf, subtype_rel_wf, bag_wf, top_wf, member_wf, permutation_wf, es-E_wf, es-locl_wf, event-ordering+_wf, es-rec-class_wf, in-eclass_wf, event-ordering+_inc, subtype_rel_self, es-base-E_wf, intensional-universe_wf, bag-subtype-list, eclass-val_wf, bag-only_wf, ifthenelse_wf, eclass_wf, es-interface-subtype_rel

\mforall{}[Info,T:Type]. \mforall{}[G:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} bag(T)]. \mforall{}[F:es:EO+(Info) {}\mrightarrow{} e':E {}\mrightarrow{} T {}\mrightarrow{} \{e:E| (e' <loc e)\} {}\mrightarrow{} bag(T)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. RecClass(first e G[es;e] or next e after e' with value v F[es;e';v;e])(e) = if e \mmember{}\msubb{} prior(RecClass(first e G[es;e] or next e after e' with value v F[es;e';v;e])) then let e' = prior(RecClass(first e G[es;e] or next e after e' with value v F[es;e';v;e]))(e) in only(F[es;e';RecClass(first e G[es;e] or next e after e' with value v F[es;e';v;e])(e');e]) else only(G[es;e]) fi supposing \muparrow{}e \mmember{}\msubb{} RecClass(first e G[es;e] or next e after e' with value v F[es;e';v;e]) Date html generated: 2011_08_16-PM-05_03_10 Last ObjectModification: 2011_06_20-AM-01_09_27 Home Index