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

[Info,A,B:Type].

[es:EO+(Info)].

[F:Id

A

B

B].

[X:EClass(A)].

[init:Id

bag(B)].
  (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], 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 y.t[x; y], so_lambda:

x.t[x], member: t

T, rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|, ycomb: Y, and: P

Q, lelt: i

j < k, top: Top, length: ||as||, false: False, not:

A, implies: P

Q, int_seg: {i..j

}, nat:

, le: A

B, all:

x:A. B[x], btrue: tt, bfalse: ff, lt_int: i <z j, bnot:

b, le_int: i

z j, ifthenelse: if b then t else f fi , select: l[i], eq_int: (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), lifting-loc-2: lifting-loc-2(f), so_apply: x[s1;s2], so_apply: x[s], uall:

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

, uimplies: b supposing a, guard: {T}, sq_type: SQType(T), or: P

Q, subtype: S

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

\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[F:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[X:EClass(A)]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. (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_20 Last ObjectModification: 2012_02_07-PM-01_10_30 Home Index