Nuprl Lemma : rec-class-unique

{

[Info,T:Type].

[G:es:EO+(Info)

E

bag(T)].

[F:es:EO+(Info)

e':E

T

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

bag(T)].

[X:EClass(T)].
    X
    = RecClass(first e
                 G[es;e]
               or next e after e' with value v
                   F[es;e';v;e])
    supposing

es:EO+(Info).

e:E.
((X es e)
= if e

prior(X)
                  then let e' = prior(X)(e) in
                           F[es;e';X(e');e]
                  else G[es;e]
                  fi ) }

{ Proof }

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

X, eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-locl: (e <loc e'), es-E: E, 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], all:

x:A. B[x], set: {x:A| B[x]} , apply: f a, function: x:A

B[x], universe: Type, equal: s = t, bag: bag(T)
Definitions : fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), record-select: r.x, eq_atom: x =a y, eq_atom: eq_atom$n(x;y), decide: case b of inl(x) => s[x] | inr(y) => t[y], assert:

b, dep-isect: Error :dep-isect, record+: record+, le: A

B, ge: i

j , not:

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

B[x], and: P

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

r B, so_apply: x[s1;s2], so_apply: x[s1;s2;s3;s4], eclass-val: X(e), let: let, es-E-interface: E(X), top: Top, es-prior-interface: prior(X), in-eclass: e

X, ifthenelse: if b then t else f fi , apply: f a, limited-type: LimitedType, uimplies: b supposing a, lambda:

x.A[x], so_lambda:

x y.t[x; y], eclass: EClass(A[eo; e]), prop:

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

T, universe: Type, bag: bag(T), es-E: E, event_ordering: EO, event-ordering+: EO+(Info), member: t

T, equal: s = t, all:

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

B[x], uall:

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

x:A. B[x], pair: <a, b>, true: True, squash:

T, es-causl: (e < e'), real:

, grp_car: |g|, minus: -n, add: n + m, subtract: n - m, void: Void, false: False, natural_number: $n, int:

, nat:

, exists:

x:A. B[x], strongwellfounded: SWellFounded(R[x; y]), guard: {T}, implies: P

Q, so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]), es-rec-class: es-rec-class, es-pred: pred(e), intensional-universe: IType, es-loc: loc(e), fpf-cap: f(x)?z, filter: filter(P;l), permutation: permutation(T;L1;L2), list: type List, atom: Atom, es-base-E: es-base-E(es), token: "$token", quotient: x,y:A//B[x; y], cond-class: [X?Y], so_apply: x[s], or: P

Q, eq_knd: a = b, l_member: (x

l), fpf-dom: x

dom(f), bfalse: ff, btrue: tt, 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'), 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, unit: Unit, union: left + right, bool:

, Id: Id, rev_implies: P

Q, iff: P

Q, RepUR: Error :RepUR, MaAuto: Error :MaAuto, CollapseTHENA: Error :CollapseTHENA, CollapseTHEN: Error :CollapseTHEN, RepeatFor: Error :RepeatFor, tactic: Error :tactic, bag-size: bag-size(bs), es-interface-at: X@i, so_lambda:

x.t[x], tag-by: z

T, fset: FSet{T}, dataflow: dataflow(A;B), isect2: T1

T2, b-union: A

B, record: record(x.T[x]), 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), fpf-sub: f

g, sq_stable: SqStable(P), Auto: Error :Auto, sq_type: SQType(T), suptype: suptype(S; T), sqequal: s ~ t, bag-only: only(bs), es-le: e

loc e' , es-p-le: e p

e', es-causle: e c

e', es-p-locl: e p< e', causal-predecessor: causal-predecessor(es;p), BHyp: Error :BHyp, rev_uimplies: rev_uimplies(P;Q), set_car: |p|, rng_car: |r|, atom: Atom$n, rationals:

, IdLnk: IdLnk, l_disjoint: l_disjoint(T;l1;l2), qle: r

s, qless: r < s, nequal: a

b

T , l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), grp_lt: a < b, set_lt: a <p b, set_leq: a

b, Try: Error :Try, cand: A c

B, ParallelOp: Error :ParallelOp, Knd: Knd
Lemmas : is-prior-interface, bool_subtype_base, assert_elim, uiff_wf, assert_of_eq_int, es-prior-interface-causl, bag-only_wf, subtype_base_sq, es-prior-interface-equal, sq_stable__assert, assert_functionality_wrt_uiff, eq_int_wf, bag-size_wf, Id_wf, eclass-val_wf, rev_implies_wf, iff_wf, assert_wf, false_wf, true_wf, subtype_rel_wf, bool_wf, eqtt_to_assert, not_wf, uiff_transitivity, eqff_to_assert, assert_of_bnot, bnot_wf, es-prior-interface_wf, es-interface-top, es-interface-subtype_rel2, es-E-interface_wf, es-base-E_wf, subtype_rel_self, top_wf, permutation_wf, eclass-val_wf2, es-interface-val_wf2, event_ordering_wf, squash_wf, es-loc_wf, intensional-universe_wf, es-prior-interface-locl, nat_wf, es-causl-swellfnd, es-rec-class_wf, nat_properties, ge_wf, le_wf, es-causl_wf, member_wf, bag_wf, eclass_wf, es-prior-interface_wf1, event-ordering+_wf, es-E_wf, in-eclass_wf, ifthenelse_wf, event-ordering+_inc, es-locl_wf

\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{}[X:EClass(T)]. X = RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) supposing \mforall{}es:EO+(Info). \mforall{}e:E. ((X es e) = if e \mmember{}\msubb{} prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ) Date html generated: 2011_08_16-PM-05_07_30 Last ObjectModification: 2011_06_20-AM-01_11_11 Home Index