Nuprl Definition : bar_26_4a
bar_26_4a{i:l}() ==
g:
List 
. R,A: List 
.
(spr(g)
((g []) = 0)
(a: List. (((g a) = 0) Dec(R a)))
(f: . ((x:. ((g mklist(x;f)) = 0)) (
x:. (R mklist(x;f)))))
(a: List. (((g a) = 0) (R a) (A a)))
(a: List. (((g a) = 0) (s:. (((g (a @ [s])) = 0) (A (a @ [s])))) (A a)))
(A []))
Definitions occuring in Statement :
append: as @ bs,
nat: ,
decidable: Dec(P),
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
FDL editor aliases :
bar_26_4a
bar\_26\_4a\{i:l\}() ==
\mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}R,A:\mBbbN{} List {}\mrightarrow{} \mBbbP{}.
(spr(g)
{}\mRightarrow{} ((g []) = 0)
{}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} Dec(R a)))
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}x:\mBbbN{}. ((g mklist(x;f)) = 0)) {}\mRightarrow{} (\mexists{}x:\mBbbN{}. (R mklist(x;f)))))
{}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} (R a) {}\mRightarrow{} (A a)))
{}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} (\mforall{}s:\mBbbN{}. (((g (a @ [s])) = 0) {}\mRightarrow{} (A (a @ [s])))) {}\mRightarrow{} (A a)))
{}\mRightarrow{} (A []))
Date html generated:
2013_03_20-AM-10_32_42
Last ObjectModification:
2013_03_01-PM-05_19_35
Home
Index