{ 
[M:Type 
Type]
[S1,S2:System(P.M[P])]. (system-equiv(P.M[P];S1;S2) 
)
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
system-equiv: system-equiv(T.M[T];S1;S2),
System: System(P.M[P]),
strong-type-continuous: Continuous+(T.F[T]),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s],
member: t T,
prop: ,
system-equiv: system-equiv(T.M[T];S1;S2),
and: P 
Q,
all: x:A. B[x],
cand: A c B,
so_lambda: 
x.t[x],
le: A 
B,
subtype: S 
T,
not: 
A,
implies: P 
Q,
false: False,
System: System(P.M[P]),
int_seg: {i..j
},
component: component(P.M[P]),
lelt: i j < k
Lemmas :
ldag_wf,
pInTransit_wf,
length_wf1,
component_wf,
int_seg_wf,
select_wf,
Id_wf,
Process_wf,
int_seg_properties,
process-equiv_wf,
System_wf,
strong-type-continuous_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S1,S2:System(P.M[P])]. (system-equiv(P.M[P];S1;S2) \mmember{} \mBbbP{}) supposing Continuous+(P.M[P])
Date html generated:
2011_08_16-PM-06_51_31
Last ObjectModification:
2011_06_18-AM-11_06_10
Home
Index