Nuprl Lemma : pi-new-trans_wf
[x:Name]. [P:Pi_term]. [g:{Q:Pi_term| pi-rank(Q) < pi-rank((new x. P))} 
Id Name Name List pi-process()].
(pi-new-trans(x;P;g) 
Id Name Name List pi-process())
Proof not projected
Definitions occuring in Statement :
pi-process: pi-process(),
pi-rank: pi-rank(p),
pinew: (new name. body),
pi_term: Pi_term,
Id: Id,
name: Name,
uall: [x:A]. B[x],
member: t T,
less_than: a < b,
set: {x:A| B[x]} ,
function: x:A B[x],
list: type List
Definitions :
ycomb: Y,
top: Top,
pi-new-trans: pi-new-trans(x;P;g),
member: t T,
uall: [x:A]. B[x],
process: process(P.M[P];P.E[P]),
Process: Process(P.M[P]),
pi-process: pi-process(),
so_lambda: 
x.t[x],
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
isect2: T1 
T2,
and: P 
Q,
true: True,
squash: 
T,
prop: 
,
pi-rank: pi-rank(p),
pMsg: pMsg(P.M[P]),
piM: piM(T),
nat: 
,
so_apply: x[s],
uimplies: b supposing a,
unit: Unit,
bool: 
,
it: 
Lemmas :
pi-process_wf,
name_wf,
pinew_wf,
nat_wf,
pi-rank_wf,
pi_term_wf,
Id_wf,
top_wf,
strong-continuous-list,
continuous-constant,
Com_wf,
ldag_wf,
piM_wf,
ycomb_wf_corec_3parameter,
bool_wf,
pi-names_wf,
name-deq_wf,
l-union_wf,
pi-rank-pi-simple-subst,
true_wf,
squash_wf,
pDVfire_wf
\mforall{}[x:Name]. \mforall{}[P:Pi\_term]. \mforall{}[g:\{Q:Pi\_term| pi-rank(Q) < pi-rank((new x. P))\}
{}\mrightarrow{} Id
{}\mrightarrow{} Name
{}\mrightarrow{} Name List
{}\mrightarrow{} pi-process()].
(pi-new-trans(x;P;g) \mmember{} Id {}\mrightarrow{} Name {}\mrightarrow{} Name List {}\mrightarrow{} pi-process())
Date html generated:
2012_01_23-PM-01_34_17
Last ObjectModification:
2011_12_11-PM-11_26_59
Home
Index