Nuprl Lemma : aa_kleene_fan_contra2
(
f:
. Bij(; ;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
Definitions occuring in Statement :
length: ||as||,
append: as @ bs,
biject: Bij(A;B;f),
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)
Definitions :
so_lambda: 
x.t[x],
member: t 
T,
implies: P Q,
suptype: suptype(S; T),
subtype: S 
T,
false: False,
le: A 
B,
not: A,
and: P Q,
prop: ,
exists: x:A. B[x],
all: x:A. B[x],
nat: ,
rev_implies: P 
Q,
lelt: i j < k,
int_seg: {i..j
},
iff: P Q,
top: Top,
true: True,
squash: 
T,
bfalse: ff,
ifthenelse: if b then t else f fi ,
btrue: tt,
so_apply: x[s],
uall: [x:A]. B[x],
surject: Surj(A;B;f),
inject: Inj(A;B;f),
biject: Bij(A;B;f),
uimplies: b supposing a,
uiff: uiff(P;Q),
unit: Unit,
bool: ,
guard: {T},
it: 
Lemmas :
biject_wf,
bool_wf,
nat_wf,
exists_wf,
length_wf_nat,
int_seg_wf,
le_wf,
mklist_wf,
not_wf,
append_wf,
btrue_wf,
select_wf,
bfalse_wf,
length_wf,
less_than_wf,
all_wf,
length_append,
non_neg_length,
lelt_wf,
select_append_front,
subtype_rel_self,
subtype_rel_sets,
subtype_rel_dep_function,
mklist_length,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
assert_wf,
equal_wf,
uiff_transitivity,
eqtt_to_assert,
subtype_rel_set_simple,
assert_elim,
btrue_neq_bfalse,
mklist_select,
not_assert_elim,
ifthenelse_wf,
and_wf
(\mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbB{}. Bij(\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-09_49_13
Last ObjectModification:
2012_11_27-AM-10_32_03
Home
Index