{ 
[M,E:Type 
Type]. [g:
T:Type. (T E[T])].
(virus-process(g) 
process(P.M[P];P.E[P])) }
{ Proof }
Definitions occuring in Statement :
virus-process: virus-process(g),
process: process(P.M[P];P.E[P]),
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
isect: x:A. B[x],
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
process: process(P.M[P];P.E[P]),
virus-process: virus-process(g),
so_lambda: 
x.t[x],
all: x:A. B[x],
implies: P 
Q
Lemmas :
ycomb_wf_corec
\mforall{}[M,E:Type {}\mrightarrow{} Type]. \mforall{}[g:\mcap{}T:Type. (T {}\mrightarrow{} E[T])]. (virus-process(g) \mmember{} process(P.M[P];P.E[P]))
Date html generated:
2011_08_16-AM-09_54_04
Last ObjectModification:
2011_06_18-AM-08_36_15
Home
Index