{ 
[M:Type 
Type]
[S1,S2:System(P.M[P])]. S1 = S2 supposing 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]),
pInTransit: pInTransit(P.M[P]),
ldag: LabeledDAG(T),
strong-type-continuous: Continuous+(T.F[T]),
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
function: x:A B[x],
product: x:A 
B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s],
top: Top,
member: t 
T,
so_lambda: 
x.t[x],
System: System(P.M[P]),
system-equiv: system-equiv(T.M[T];S1;S2),
and: P 
Q,
prop: 
Lemmas :
equal-top,
system-equiv_wf,
System_wf,
strong-type-continuous_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S1,S2:System(P.M[P])]. S1 = S2 supposing system-equiv(P.M[P];S1;S2)
supposing Continuous+(P.M[P])
Date html generated:
2011_08_16-PM-06_51_38
Last ObjectModification:
2011_06_18-AM-11_06_20
Home
Index