{ 
[l_loc:Id]. [P:Pi_term].
(pi-trans(l_loc;P) 
Id 
Name Name List pi-process()) }
{ Proof }
Definitions occuring in Statement :
pi-trans: pi-trans(l_loc;P),
pi-process: pi-process(),
pi_term: Pi_term,
Id: Id,
name: Name,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
all: x:A. B[x],
implies: P 
Q,
pi-trans: pi-trans(l_loc;P),
prop: 
,
ycomb: Y,
ifthenelse: if b then t else f fi ,
pizero?: pizero?(x),
pipar?: pipar?(x),
let: let,
pipar-left: pipar-left(x),
pipar-right: pipar-right(x),
pirep?: pirep?(x),
pirep-body: pirep-body(x),
pinew?: pinew?(x),
pinew-name: pinew-name(x),
pinew-body: pinew-body(x),
pioption?: pioption?(x),
picomm?: picomm?(x),
btrue: tt,
bfalse: ff,
so_lambda: 
x.t[x],
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
nat: 
,
pi_term: Pi_term,
unit: Unit,
l_exists: (
xL. P[x]),
exists: x:A. B[x],
and: P 
Q,
so_apply: x[s],
it: 
,
pizero: 0,
picomm: pre.body,
pioption: (left + right),
pipar: (left | right),
pirep: !body,
pinew: (new name. body)
Lemmas :
pi_term_wf,
Id_wf,
nat_wf,
pi-rank_wf,
pi-null-trans_wf,
name_wf,
pizero_wf,
pi-guarded-trans_wf,
pi-choices_wf,
picomm_wf,
l_exists_wf,
pi_prefix_wf,
le_wf,
pi2_wf,
l_member_wf,
pioption_wf,
pi-bar-trans_wf,
pipar_wf,
pi-rep-trans_wf,
pirep_wf,
pi-new-trans_wf,
pinew_wf,
nat_properties,
ge_wf,
rank-pi-choices
\mforall{}[l$_{loc}$:Id]. \mforall{}[P:Pi\_term]. (pi-trans(l$_{loc}$;P) \mmember{} Id \000C{}\mrightarrow{} Name {}\mrightarrow{} Name List {}\mrightarrow{} pi-process())
Date html generated:
2011_08_17-PM-07_04_22
Last ObjectModification:
2011_06_18-PM-12_46_34
Home
Index