Nuprl Lemma : aa_kleene_fan_contra_partial
(
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 :
implies: P Q,
exists: x:A. B[x],
bool: ,
and: P Q,
all: x:A. B[x],
prop: ,
member: t 
T,
so_lambda: 
x.t[x],
nat: ,
le: A B,
not: A,
false: False,
subtype: S 
T,
suptype: suptype(S; T),
iff: P 
Q,
int_seg: {i..j
},
lelt: i j < k,
rev_implies: P Q,
has-value: (a),
cand: A c B,
top: Top,
squash: T,
true: True,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
bnot: 
b,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
surject: Surj(A;B;f),
unit: Unit,
uiff: uiff(P;Q),
it: 
,
guard: {T}
Lemmas :
exists_wf,
nat_wf,
Error :bar_wf,
bool_wf,
union-value-type,
unit_wf2,
surject_wf,
all_wf,
assert_wf,
Error :has-value_wf,
le_wf,
less_than_wf,
length_wf,
length_wf_nat,
bfalse_wf,
select_wf,
btrue_wf,
Error :list_wf,
append_wf,
not_wf,
mklist_wf,
int_seg_wf,
non_neg_length,
length_append,
subtype_rel_list,
top_wf,
subtype_top,
select_append_front,
lelt_wf,
Error :subtype_bar,
subtype_rel_weakening,
ext-eq_weakening,
equal_wf,
and_wf,
has-value_wf_base,
bool_subtype_base,
mklist_length,
subtype_rel_set_simple,
mklist_select,
eqtt_to_assert,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
btrue_neq_bfalse,
assert_elim,
not_assert_elim,
subtype_rel_dep_function,
subtype_rel_sets,
ifthenelse_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{} (\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_50_42
Last ObjectModification:
2012_11_27-AM-10_32_06
Home
Index