Nuprl Lemma : rec-combined-loc-class-opt-1-es-sv

[Info,A:Type].

[es:EO+(Info)].

[F:Top].

[X:EClass(A)].

[init:Id

bag(Top)].
  (es-sv-class(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|)) supposing
     (es-sv-class(es;X) and
     (

l:Id. (bag-size(init l)

1)))

Proof not projected

Definitions occuring in Statement : lifting-loc-2: lifting-loc-2(f), rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|, es-sv-class: es-sv-class(es;X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, uimplies: b supposing a, uall:

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

B, all:

x:A. B[x], apply: f a, function: x:A

B[x], natural_number: $n, universe: Type, bag-size: bag-size(bs), bag: bag(T)
Definitions : so_lambda:

x.t[x], lt_int: i <z j, bnot:

b, le_int: i

z j, bfalse: ff, btrue: tt, eq_int: (i =

j), ifthenelse: if b then t else f fi , ycomb: Y, and: P

Q, lelt: i

j < k, so_lambda:

x y.t[x; y], length: ||as||, implies: P

Q, not:

A, int_seg: {i..j

}, lifting-gen-list-rev: lifting-gen-list-rev(n;bags), lifting-gen-rev: lifting-gen-rev(n;f;bags), lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f), lifting2-loc: lifting2-loc(f;loc;abag;bbag), select: l[i], nat:

, member: t

T, false: False, lifting-loc-2: lifting-loc-2(f), rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|, le: A

B, top: Top, all:

x:A. B[x], so_apply: x[s], so_apply: x[s1;s2], uimplies: b supposing a, prop:

, uall:

[x:A]. B[x], guard: {T}, sq_type: SQType(T), or: P

Q, subtype: S

T, eclass: EClass(A[eo; e])
Lemmas : event-ordering+_wf, all_wf, es-sv-class_wf, nat_wf, Id_wf, bag_wf, single-bag_wf, lelt_wf, bag-combine_wf, event-ordering+_inc, es-E_wf, eclass_wf, select_wf, int_seg_wf, le_wf, rec-comb_wf, top_wf, bag-size_wf, rec-comb-es-sv, int_subtype_base, subtype_base_sq, bag-combine-empty-left, bag-size-zero, bag-size-one, single-valued-bag-if-le1, bag-only_wf2, bag-combine-single-left, equal_wf, and_wf

\mforall{}[Info,A:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[F:Top]. \mforall{}[X:EClass(A)]. \mforall{}[init:Id {}\mrightarrow{} bag(Top)]. (es-sv-class(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|)) supposing (es-sv-class(es;X) and (\mforall{}l:Id. (bag-size(init l) \mleq{} 1))) Date html generated: 2012_02_20-PM-02_58_37 Last ObjectModification: 2012_02_07-PM-01_16_05 Home Index