Nuprl Lemma : aa_kleene_fan_contra_partial_imax
(
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 @ l2)) (R l1)))
(A: . x:. (
(R mklist(x;A))))
(x:. l: List. ((x = ||l||) (R l)))))
Proof
Definitions occuring in Statement :
length: ||as||,
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],
equal: s = t,
mklist: mklist(n;f),
has-value: (a)
Definitions :
so_lambda: 
x.t[x],
member: t 
T,
prop: ,
all: x:A. B[x],
and: P Q,
bool: ,
exists: x:A. B[x],
implies: P Q,
suptype: suptype(S; T),
subtype: S 
T,
false: False,
not: A,
le: A B,
nat: ,
rev_implies: P 
Q,
lelt: i j < k,
int_seg: {i..j
},
iff: P Q,
has-value: (a),
or: P 
Q,
cand: A c B,
imax: imax(a;b),
top: Top,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
squash: T,
bnot: 
b,
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
surject: Surj(A;B;f),
unit: Unit,
uiff: uiff(P;Q),
guard: {T},
it: 
Lemmas :
le_wf,
Error :has-value_wf,
assert_wf,
all_wf,
surject_wf,
unit_wf2,
union-value-type,
bool_wf,
Error :bar_wf,
nat_wf,
exists_wf,
int_seg_wf,
mklist_wf,
not_wf,
append_wf,
Error :list_wf,
btrue_wf,
select_wf,
bfalse_wf,
length_wf_nat,
length_wf,
less_than_wf,
subtype_top,
top_wf,
subtype_rel_list,
length_append,
non_neg_length,
lelt_wf,
select_append_front,
Error :subtype_bar,
ext-eq_weakening,
subtype_rel_weakening,
equal_wf,
bool_subtype_base,
has-value_wf_base,
and_wf,
add-nat,
imax_ub,
ifthenelse_wf,
imax_wf,
mklist_length,
le_int_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_le_int,
lt_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_le_int,
assert_of_lt_int,
mklist_select,
subtype_rel_set_simple,
assert_of_bnot,
btrue_neq_bfalse,
assert_elim,
not_assert_elim,
subtype_rel_sets,
subtype_rel_dep_function
(\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{} (\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-09_51_31
Last ObjectModification:
2012_11_27-AM-10_32_09
Home
Index