Nuprl Definition : fan_wo_dec_27

Nuprl Definition : fan_wo_dec_27_9

This is exactly fan_26_6a , w/o the decidability hyp.
(also, for now, a set type is used instead of in_fin_spr)

fan_wo_dec_27_9{i:l}() ==

B:

List

.

R:

List

.
((

f:

. ((f

fspr(B))

(

x:

. (R mklist(x;f)))))

(

z:

.

f:

. ((f

fspr(B))

(

x:

. ((x

z)

(R mklist(x;f)))))))

Definitions occuring in Statement : in_fin_spr: (f

fspr(B)), nat:

, prop:

, le: A

B, all:

x:A. B[x], exists:

x:A. B[x], implies: P

Q, and: P

Q, apply: f a, function: x:A

B[x], mklist: mklist(n;f)
FDL editor aliases : fan_wo_dec_27_9
fan\_wo\_dec\_27\_9\{i:l\}() == \mforall{}B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}R:\mBbbN{} List {}\mrightarrow{} \mBbbP{}. ((\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f \mmember{} fspr(B)) {}\mRightarrow{} (\mexists{}x:\mBbbN{}. (R mklist(x;f))))) {}\mRightarrow{} (\mexists{}z:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f \mmember{} fspr(B)) {}\mRightarrow{} (\mexists{}x:\mBbbN{}. ((x \mleq{} z) \mwedge{} (R mklist(x;f))))))) Date html generated: 2013_03_20-AM-10_39_22 Last ObjectModification: 2013_03_17-PM-11_31_42 Home Index