Nuprl Lemma : aa_kleene_fan_contra4
(
f:
bar(
)
(Surj(; bar();f)
(T:
((
i,nsteps:. ((
(T i nsteps)) 
(f i i)
)) (i:. ((f i i) (nsteps:. ((T i nsteps)))))))))
(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: ,
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,
le: A 
B,
not: A,
nat: ,
rev_implies: P 
Q,
lelt: i j < k,
int_seg: {i..j
},
iff: P Q,
cand: A c B,
has-value: (a),
top: Top,
true: True,
squash: T,
assert: b,
isl: isl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
bnot: 
b,
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
surject: Surj(A;B;f),
uiff: uiff(P;Q),
unit: Unit,
decidable: Dec(P),
or: P 
Q,
it: 
,
guard: {T}
Lemmas :
Error :has-value_wf,
assert_wf,
all_wf,
surject_wf,
unit_wf2,
union-value-type,
bool_wf,
Error :bar_wf,
nat_wf,
exists_wf,
length_wf_nat,
int_seg_wf,
le_wf,
mklist_wf,
not_wf,
append_wf,
Error :list_wf,
btrue_wf,
select_wf,
bfalse_wf,
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,
subtype_rel_weakening,
ext-eq_weakening,
equal_wf,
and_wf,
has-value_wf_base,
bool_subtype_base,
mklist_length,
subtype_rel_set_simple,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
uiff_transitivity,
eqtt_to_assert,
assert_elim,
btrue_neq_bfalse,
mklist_select,
not_assert_elim,
decidable__ex_int_seg,
decidable__assert,
isl_wf,
iff_wf,
true_wf,
false_wf,
subtype_rel_dep_function,
subtype_rel_sets
(\mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} bar(\mBbbB{})
(Surj(\mBbbN{};\mBbbN{} {}\mrightarrow{} bar(\mBbbB{});f)
\mwedge{} (\mexists{}T:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
((\mforall{}i,nsteps:\mBbbN{}. ((\muparrow{}(T i nsteps)) {}\mRightarrow{} (f i i)\mdownarrow{}))
\mwedge{} (\mforall{}i:\mBbbN{}. ((f i i)\mdownarrow{} {}\mRightarrow{} (\mexists{}nsteps:\mBbbN{}. (\muparrow{}(T i nsteps)))))))))
{}\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_22
Last ObjectModification:
2012_11_27-AM-10_32_06
Home
Index