Nuprl Lemma : fpf-rename-dom2
[A,C:Type]. [eqa:EqDecider(A)]. [eqc:EqDecider(C)]. [eqc':Top]. [r:A 
C]. [f:a:A fp-> Top]. [a:A].
{
r a 
dom(rename(r;f)) supposing a dom(f)}
Proof not projected
Definitions occuring in Statement :
fpf-rename: rename(r;f),
fpf-dom: x dom(f),
fpf: a:A fp-> B[a],
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
guard: {T},
apply: f a,
function: x:A B[x],
universe: Type,
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
guard: {T},
uimplies: b supposing a,
fpf-dom: x dom(f),
fpf-rename: rename(r;f),
member: t T,
pi1: fst(t),
so_lambda: 
x.t[x],
cand: A c
B,
prop: 
,
and: P Q,
exists: 
x:A. B[x],
fpf: a:A fp-> B[a],
implies: P 
Q,
so_apply: x[s],
rev_implies: P 
Q,
all: x:A. B[x],
iff: P Q
Lemmas :
assert_witness,
deq-member_wf,
map_wf,
assert_wf,
fpf-dom_wf,
fpf_wf,
top_wf,
deq_wf,
assert-deq-member,
l_member_wf,
member_map
\mforall{}[A,C:Type]. \mforall{}[eqa:EqDecider(A)]. \mforall{}[eqc:EqDecider(C)]. \mforall{}[eqc':Top]. \mforall{}[r:A {}\mrightarrow{} C]. \mforall{}[f:a:A fp-> Top].
\mforall{}[a:A].
\{\muparrow{}r a \mmember{} dom(rename(r;f)) supposing \muparrow{}a \mmember{} dom(f)\}
Date html generated:
2012_01_23-AM-11_55_12
Last ObjectModification:
2011_12_10-PM-12_05_51
Home
Index