Nuprl Lemma : enum_not_fan
(
f:
bar(
)
(Surj(; bar();f)
(T:
indx,input:.
((nsteps:. ((
(T indx input nsteps)) 
(f indx input)
))
((f indx input) (nsteps:. ((T indx input nsteps))))
(n1,n2:. (((n1 
n2) ((T indx input n1))) ((T indx input n2))))))))
(
(R: List 
(((l1,l2: List. ((R l1) (R (l1 @ l2)))) (A: . n:. (R mklist(n;A))))
(n:. A: . (R mklist(n;A))))))
Proof
Definitions occuring in Statement :
append: as @ bs,
surject: Surj(A;B;f),
assert: b,
bool: ,
nat: ,
prop: ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
mklist: mklist(n;f),
has-value: (a)
Definitions :
implies: P Q,
exists: x:A. B[x],
nat: ,
bool: ,
and: P Q,
surject: Surj(A;B;f),
all: x:A. B[x],
not: A,
prop: ,
false: False,
member: t 
T,
so_lambda: 
x.t[x],
le: A B,
ifthenelse: if b then t else f fi ,
btrue: tt,
squash: T,
true: True,
bfalse: ff,
top: Top,
int_seg: {i..j
},
lelt: i j < k,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
cand: A c B,
guard: {T},
unit: Unit,
uiff: uiff(P;Q),
it: 
Lemmas :
aa_kleene_fan_contra_partial,
all_wf,
Error :list_wf,
bool_wf,
append_wf,
nat_wf,
exists_wf,
mklist_wf,
subtype_rel_dep_function,
int_seg_wf,
le_wf,
subtype_rel_weakening,
ext-eq_weakening,
Error :bar_wf,
union-value-type,
unit_wf2,
equal_wf,
assert_wf,
Error :has-value_wf,
subtype_rel_product,
surject_wf,
not_wf,
lt_int_wf,
uiff_transitivity,
less_than_wf,
eqtt_to_assert,
assert_of_lt_int,
select_wf,
le_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
btrue_wf,
and_wf,
mklist_length,
list_extensionality,
length_wf,
mklist_select,
lelt_wf
(\mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} bar(\mBbbB{})
(Surj(\mBbbN{};\mBbbN{} {}\mrightarrow{} bar(\mBbbB{});f)
\mwedge{} (\mexists{}T:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
\mforall{}indx,input:\mBbbN{}.
((\mforall{}nsteps:\mBbbN{}. ((\muparrow{}(T indx input nsteps)) {}\mRightarrow{} (f indx input)\mdownarrow{}))
\mwedge{} ((f indx input)\mdownarrow{} {}\mRightarrow{} (\mexists{}nsteps:\mBbbN{}. (\muparrow{}(T indx input nsteps))))
\mwedge{} (\mforall{}n1,n2:\mBbbN{}. (((n1 \mleq{} n2) \mwedge{} (\muparrow{}(T indx input n1))) {}\mRightarrow{} (\muparrow{}(T indx input n2))))))))
{}\mRightarrow{} (\mneg{}(\mforall{}R:\mBbbB{} List {}\mrightarrow{} \mBbbP{}
(((\mforall{}l1,l2:\mBbbB{} List. ((R l1) {}\mRightarrow{} (R (l1 @ l2)))) \mwedge{} (\mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}. (R mklist(n;A))))
{}\mRightarrow{} (\mexists{}n:\mBbbN{}. \mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbB{}. (R mklist(n;A))))))
Date html generated:
2013_03_20-AM-09_50_59
Last ObjectModification:
2012_11_27-AM-10_32_08
Home
Index