{ 
[S:Type]. [s0:S]. [next:
T:{T:Type| pi-process() 
r T}
(S
piM(T)
(S 
LabeledDAG(Id (Com(T.piM(T)) T))))].
(RecProcess(s0;s,m.next[s;m]) 
pi-process()) }
{ Proof }
Definitions occuring in Statement :
pi-process: pi-process(),
piM: piM(T),
Com: Com(P.M[P]),
ldag: LabeledDAG(T),
rec-process: RecProcess(s0;s,m.next[s; m]),
Id: Id,
subtype_rel: A r B,
uall: [x:A]. B[x],
so_apply: x[s1;s2],
member: t T,
set: {x:A| B[x]} ,
apply: f a,
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
universe: Type
Definitions :
so_apply: x[s],
implies: P 
Q,
or: P 
Q,
guard: {T},
l_member: (x l),
assert: 
b,
subtype: S T,
es-E-interface: E(X),
PiDataVal: PiDataVal(),
tag-case: z:T,
isect2: T1 T2,
list: type List,
union: left + right,
labeled-graph: LabeledGraph(T),
type-continuous: Continuous(T.F[T]),
pair: <a, b>,
nat: 
,
ext-eq: A 
B,
strong-type-continuous: Continuous+(T.F[T]),
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
and: P 
Q,
uiff: uiff(P;Q),
process: process(P.M[P];P.E[P]),
Process: Process(P.M[P]),
lvprocess: lvprocess(lp.M[lp];n),
lambda: 
x.A[x],
so_lambda: 
x y.t[x; y],
uimplies: b supposing a,
all: x:A. B[x],
axiom: Ax,
uall: [x:A]. B[x],
function: x:A B[x],
ldag: LabeledDAG(T),
product: x:A B[x],
Com: Com(P.M[P]),
Id: Id,
piM: piM(T),
set: {x:A| B[x]} ,
subtype_rel: A r B,
universe: Type,
isect: x:A. B[x],
member: t T,
equal: s = t,
pi-process: pi-process(),
rec-process: RecProcess(s0;s,m.next[s; m]),
so_apply: x[s1;s2],
apply: f a,
MaAuto: Error :MaAuto,
so_lambda: x.t[x],
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto
Lemmas :
pi-process_wf,
continuous-constant,
nat_wf,
ext-eq_wf,
uall_wf,
strong-type-continuous_wf,
rec-process_wf_pi,
piM_wf,
Com_wf,
Id_wf,
ldag_wf,
subtype_rel_wf,
member_wf
\mforall{}[S:Type]. \mforall{}[s0:S]. \mforall{}[next:\mcap{}T:\{T:Type| pi-process() \msubseteq{}r T\}
(S {}\mrightarrow{} piM(T) {}\mrightarrow{} (S \mtimes{} LabeledDAG(Id \mtimes{} (Com(T.piM(T)) T))))].
(RecProcess(s0;s,m.next[s;m]) \mmember{} pi-process())
Date html generated:
2011_08_17-PM-06_58_11
Last ObjectModification:
2011_06_18-PM-12_36_55
Home
Index