{ pi-null-trans() 
pi-process() }
{ Proof }
Definitions occuring in Statement :
pi-null-trans: pi-null-trans(),
pi-process: pi-process(),
member: t T
Definitions :
universe: Type,
member: t T,
equal: s = t,
function: x:A 
B[x],
all: 
x:A. B[x],
pi-process: pi-process(),
set: {x:A| B[x]} ,
subtype_rel: A 
r B,
unit: Unit,
piM: piM(T),
Id: Id,
so_lambda: 
x.t[x],
Com: Com(P.M[P]),
apply: f a,
product: x:A 
B[x],
list: type List,
nil: [],
lambda: x.A[x],
make-lg: make-lg(L),
it: 
,
pair: <a, b>,
so_lambda: x y.t[x; y],
rec-process: RecProcess(s0;s,m.next[s; m]),
pi-null-trans: pi-null-trans()
Lemmas :
rec-process_wf_pi_simple_state,
it_wf,
make-lg_wf,
Com_wf,
Id_wf,
piM_wf,
unit_wf,
subtype_rel_wf,
pi-process_wf
pi-null-trans() \mmember{} pi-process()
Date html generated:
2010_08_27-PM-09_43_23
Last ObjectModification:
2010_04_29-PM-12_54_17
Home
Index