Nuprl Lemma : aa_kleene_fan_contra

Nuprl Lemma : aa_kleene_fan_contra_total

(

f:

. Surj(

;

;f))

(

R:

List

((

l1,l2:

List. ((R (l1 @ l2))

(R l1)))

(

A:

.

x:

. (

(R mklist(x;A))))

(

x:

.

l:

List. ((x = ||l||)

(R l)))))

Proof not projected

Error : references
(\mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbB{}. Surj(\mBbbN{};\mBbbN{} {}\mrightarrow{} \mBbbB{};f)) {}\mRightarrow{} (\mexists{}R:\mBbbB{} List {}\mrightarrow{} \mBbbP{} ((\mforall{}l1,l2:\mBbbB{} List. ((R (l1 @ l2)) {}\mRightarrow{} (R l1))) \mwedge{} (\mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}x:\mBbbN{}. (\mneg{}(R mklist(x;A)))) \mwedge{} (\mforall{}x:\mBbbN{}. \mexists{}l:\mBbbB{} List. ((x = ||l||) \mwedge{} (R l))))) Date html generated: 2013_03_20-AM-11_02_18 Last ObjectModification: 2012_11_27-AM-10_32_03 Home Index