Nuprl Lemma : rec-combined-loc-class-locally-programmable2

[Info:{Info:Type|

Info} ]

B:{B:Type| valueall-type(B)} .

n:

.

[A:

n

Type].

[Xs:k:

n

EClass(A k)].
((

k:

n. NormalLProgrammable(A k;Xs k))

(

F:Id

k:

n

bag(A k)

bag(B)

bag(B)
NormalLProgrammable(B;F|Loc, Xs, Prior(self)|)
supposing

x:Id.

b:bag(B).

f:k:

n

bag(A k). ((

k:

n. ((f k) = {}))

((F x f b) = {}))))

Proof not projected

Definitions occuring in Statement : normal-locally-programmable: NormalLProgrammable(A;X), rec-combined-loc-class: f|Loc, X, Prior(self)|, eclass: EClass(A[eo; e]), Id: Id, int_seg: {i..j

}, nat:

, uimplies: b supposing a, uall:

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

x:A. B[x], exists:

x:A. B[x], squash:

T, implies: P

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

B[x], natural_number: $n, universe: Type, equal: s = t, empty-bag: {}, bag: bag(T), valueall-type: valueall-type(T)
Definitions : so_lambda:

x y.t[x; y], so_lambda:

x.t[x], prop:

, member: t

T, exists:

x:A. B[x], uimplies: b supposing a, implies: P

Q, all:

x:A. B[x], uall:

[x:A]. B[x], primed-class-opt: Prior(X)?b, primed-class: Prior(X), rec-comb: rec-comb(X;f;init), rec-combined-loc-class: f|Loc, X, Prior(self)|, true: True, or: P

Q, squash:

T, so_apply: x[s1;s2], so_apply: x[s], nat:

, subtype: S

T
Lemmas : squash_wf, valueall-type_wf, nat_wf, event-ordering+_wf, event-ordering+_inc, es-E_wf, eclass_wf, normal-locally-programmable_wf, all_wf, Id_wf, empty-bag_wf, bag_wf, equal_wf, int_seg_wf, exists_wf, rec-comb-locally-programmable1

\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ] \mforall{}B:\{B:Type| valueall-type(B)\} . \mforall{}n:\mBbbN{}. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[Xs:k:\mBbbN{}n {}\mrightarrow{} EClass(A k)]. ((\mforall{}k:\mBbbN{}n. NormalLProgrammable(A k;Xs k)) {}\mRightarrow{} (\mforall{}F:Id {}\mrightarrow{} k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B) NormalLProgrammable(B;F|Loc, Xs, Prior(self)|) supposing \mforall{}x:Id. \mforall{}b:bag(B). \mforall{}f:k:\mBbbN{}n {}\mrightarrow{} bag(A k). ((\mexists{}k:\mBbbN{}n. ((f k) = \{\})) {}\mRightarrow{} ((F x f b) = \{\})))) Date html generated: 2012_01_23-PM-12_31_59 Last ObjectModification: 2011_12_14-PM-10_44_28 Home Index