Nuprl Definition : bar_fwd_fim

Nuprl Definition : bar_fwd_fim_classical

bar_fwd_fim_classical(R) ==

f:

. (

x:

. (

R mklist(x;f)))

Definitions occuring in Statement : nat:

, all:

x:A. B[x], exists:

x:A. B[x], squash:

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

B[x], mklist: mklist(n;f)
bar\_fwd\_fim\_classical(R) == \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (\mdownarrow{}\mexists{}x:\mBbbN{}. (\mdownarrow{}R mklist(x;f))) Date html generated: 2013_03_20-AM-10_31_33 Last ObjectModification: 2013_02_25-PM-05_11_54 Home Index