{ 
[M:Type 
Type]
[S0:System(P.M[P])]. [n2m:
pMsg(P.M[P])]. [l2m:Id pMsg(P.M[P])].
[env:pEnvType(P.M[P])]. [e:runEvents(pRun(S0;env;n2m;l2m))].
(0 < run-event-step(e))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
run-event-step: run-event-step(e),
runEvents: runEvents(r),
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
System: System(P.M[P]),
pMsg: pMsg(P.M[P]),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
less_than: a < b,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
decide_bfalse: decide_bfalse{decide_bfalse_compseq_tag_def:o}(v11.g[v11]; v21.f[v21]),
atom: Atom$n,
limited-type: LimitedType,
real: 
,
grp_car: |g|,
lt_int: i <z j,
le_int: i 
z j,
bfalse: ff,
eq_atom: x =a y,
null: null(as),
set_blt: a <
b,
grp_blt: a < b,
infix_ap: x f y,
dcdr-to-bool: [d],
bl-all: (x
L.P[x])_b,
bl-exists: (
xL.P[x])_b,
b-exists: (i<n.P[i])_b,
eq_type: eq_type(T;T'),
eq_atom: eq_atom$n(x;y),
qeq: qeq(r;s),
q_less: q_less(r;s),
q_le: q_le(r;s),
deq-member: deq-member(eq;x;L),
deq-disjoint: deq-disjoint(eq;as;bs),
deq-all-disjoint: deq-all-disjoint(eq;ass;bs),
eq_str: Error :eq_str,
eq_id: a = b,
eq_lnk: a = b,
es-eq-E: e = e',
bimplies: p 
q,
band: p 
q,
bor: p 
q,
bnot: 
b,
btrue: tt,
natural_number: $n,
eq_int: (i =
j),
sq_type: SQType(T),
bool: 
,
is-run-event: is-run-event(r;t;x),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
assert: 
b,
length: ||as||,
run-event-step: run-event-step(e),
void: Void,
nat_plus: 
,
fpf-dom: x dom(f),
false: False,
guard: {T},
pair: <a, b>,
pInTransit: pInTransit(P.M[P]),
unit: Unit,
int: 
,
subtype: S 
T,
tag-by: z
T,
rev_implies: P 
Q,
or: P Q,
implies: P Q,
iff: P Q,
labeled-graph: LabeledGraph(T),
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
top: Top,
true: True,
fpf-sub: f g,
deq: EqDecider(T),
ma-state: State(ds),
class-program: ClassProgram(T),
es-E-interface: E(X),
fpf-cap: f(x)?z,
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ext-eq: A 
B,
set: {x:A| B[x]} ,
ldag: LabeledDAG(T),
list: type List,
le: A B,
ge: i 
j ,
not: A,
less_than: a < b,
product: x:A B[x],
and: P Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
fulpRunType: fulpRunType(T.M[T]),
runEvents: runEvents(r),
pEnvType: pEnvType(T.M[T]),
Id: Id,
nat: ,
pMsg: pMsg(P.M[P]),
uimplies: b supposing a,
prop: 
,
strong-type-continuous: Continuous+(T.F[T]),
all: x:A. B[x],
function: x:A B[x],
isect: x:A. B[x],
equal: s = t,
lambda: 
x.A[x],
apply: f a,
universe: Type,
uall: [x:A]. B[x],
System: System(P.M[P]),
so_lambda: 
x.t[x],
SplitOn: Error :SplitOn,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR,
D: Error :D,
MaAuto: Error :MaAuto,
pRun: pRun(S0;env;nat2msg;loc2msg),
so_apply: x[s],
pRunType: pRunType(T.M[T]),
member: t T,
AssertBY: Error :AssertBY,
tactic: Error :tactic,
Auto: Error :Auto
Lemmas :
pRunType_wf,
subtype_rel_wf,
fulpRunType_wf,
member_wf,
pRun_wf,
pEnvType_wf,
pMsg_wf,
Id_wf,
nat_wf,
System_wf,
strong-type-continuous_wf,
pInTransit_wf,
ldag_wf,
top_wf,
unit_wf,
subtype_rel_function,
subtype_rel_self,
subtype_rel_simple_product,
runEvents_wf,
bool_cases,
bool_wf,
subtype_base_sq,
bool_subtype_base,
iff_weakening_uiff,
uiff_transitivity,
eqtt_to_assert,
assert_of_eq_int,
not_wf,
eqff_to_assert,
assert_wf,
assert_of_bnot,
not_functionality_wrt_uiff,
eq_int_wf,
bnot_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S0:System(P.M[P])]. \mforall{}[n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[l2m:Id {}\mrightarrow{} pMsg(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])]. \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].
(0 < run-event-step(e))
supposing Continuous+(P.M[P])
Date html generated:
2011_08_16-PM-06_58_58
Last ObjectModification:
2011_06_18-AM-11_13_58
Home
Index