Nuprl Lemma : bar_bwd_implies_fwd
R:
List 
. ((A: List . bar_bwd_fim(R;A)) 
bar_fwd_fim(R))
Proof
Definitions occuring in Statement :
bar_bwd_fim: bar_bwd_fim(R;A),
bar_fwd_fim: bar_fwd_fim(R),
nat: ,
prop: ,
all: x:A. B[x],
implies: P Q,
function: x:A B[x]
Definitions :
all: x:A. B[x],
prop: ,
implies: P Q,
member: t 
T,
so_lambda: 
x.t[x],
nat: ,
int_seg: {i..j
},
bar_fwd_fim: bar_fwd_fim(R),
exists: 
x:A. B[x],
mklist: mklist(n;f),
le: A 
B,
not: 
A,
false: False,
primrec: primrec(n;b;c),
top: Top,
iff: P 
Q,
squash: 
T,
true: True,
and: P 
Q,
rev_implies: P Q,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
lelt: i j < k,
bar_bwd_fim: bar_bwd_fim(R;A),
append: as @ bs
Lemmas :
all_wf,
Error :list_wf,
nat_wf,
bar_bwd_fim_wf,
subtype_rel_dep_function,
subtype_rel_weakening,
ext-eq_weakening,
exists_wf,
append_wf,
mklist_wf,
int_seg_wf,
subtype_rel_sets,
lelt_wf,
le_wf,
append-nil,
subtype_rel_list,
top_wf,
subtype_top,
Error :cons_wf,
Error :nil_wf,
append_assoc,
mklist-single,
squash_wf,
true_wf,
mklist-add
\mforall{}R:\mBbbN{} List {}\mrightarrow{} \mBbbP{}. ((\mforall{}A:\mBbbN{} List {}\mrightarrow{} \mBbbP{}. bar\_bwd\_fim(R;A)) {}\mRightarrow{} bar\_fwd\_fim(R))
Date html generated:
2013_03_20-AM-10_31_54
Last ObjectModification:
2013_02_28-PM-06_09_15
Home
Index