{ 
[M:Type 
Type]
[n2m:
pMsg(P.M[P])]. [l2m:Id pMsg(P.M[P])]. [S0:System(P.M[P])].
[env:pEnvType(P.M[P])].
[e:runEvents(pRun(S0;env;n2m;l2m))]
((fst(fst(run-info(pRun(S0;env;n2m;l2m);e)))) < run-event-step(e))
supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
run-initialization: run-initialization(r;G),
run-event-step: run-event-step(e),
runEvents: runEvents(r),
run-info: run-info(r;e),
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],
pi1: fst(t),
pi2: snd(t),
less_than: a < b,
function: x:A B[x],
universe: Type
Definitions :
let: let,
is-dag: is-dag(g),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
assert: 
b,
lg-all: x
G.P[x],
natural_number: $n,
axiom: Ax,
run-event-step: run-event-step(e),
run-info: run-info(r;e),
pi1: fst(t),
runEvents: runEvents(r),
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},
dataflow: dataflow(A;B),
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
bag: bag(T),
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],
ext-eq: A 
B,
set: {x:A| B[x]} ,
ldag: LabeledDAG(T),
list: type List,
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),
subtype_rel: A r B,
fulpRunType: fulpRunType(T.M[T]),
product: x:A B[x],
pi2: snd(t),
run-initialization: run-initialization(r;G),
pEnvType: pEnvType(T.M[T]),
Id: Id,
nat: ,
uimplies: b supposing a,
prop: 
,
strong-type-continuous: Continuous+(T.F[T]),
all: x:A. B[x],
isect: x:A. B[x],
so_lambda: 
x.t[x],
equal: s = t,
lambda: x.A[x],
apply: f a,
universe: Type,
uall: [x:A]. B[x],
function: x:A B[x],
pMsg: pMsg(P.M[P]),
CollapseTHEN: Error :CollapseTHEN,
so_apply: x[s],
System: System(P.M[P]),
member: t T,
AssertBY: Error :AssertBY,
Auto: Error :Auto,
CollapseTHENA: Error :CollapseTHENA,
RepUR: Error :RepUR,
Complete: Error :Complete,
Try: Error :Try,
MaAuto: Error :MaAuto,
pRun: pRun(S0;env;nat2msg;loc2msg),
pRunType: pRunType(T.M[T]),
tactic: Error :tactic,
lg-label: lg-label(g;x),
lg-size: lg-size(g),
lelt: i j < k,
int_seg: {i..j
},
exists: 
x:A. B[x],
D: Error :D,
RepeatFor: Error :RepeatFor,
length: ||as||,
btrue: tt,
eq_int: (i =
j),
bool: 
,
sq_type: SQType(T),
is-run-event: is-run-event(r;t;x),
bnot: 
b,
bor: p q,
band: p q,
bimplies: p q,
es-eq-E: e = e',
eq_lnk: a = b,
eq_id: a = b,
eq_str: Error :eq_str,
deq-all-disjoint: deq-all-disjoint(eq;ass;bs),
deq-disjoint: deq-disjoint(eq;as;bs),
deq-member: deq-member(eq;x;L),
q_le: q_le(r;s),
q_less: q_less(r;s),
qeq: qeq(r;s),
eq_atom: eq_atom$n(x;y),
eq_type: eq_type(T;T'),
b-exists: (i<n.P[i])_b,
bl-exists: (xL.P[x])_b,
bl-all: (xL.P[x])_b,
dcdr-to-bool: [d],
infix_ap: x f y,
grp_blt: a < b,
set_blt: a < b,
null: null(as),
eq_atom: x =a y,
bfalse: ff,
le_int: i z j,
lt_int: i <z j,
grp_car: |g|,
real: 
,
limited-type: LimitedType,
atom: Atom$n,
decide_bfalse: decide_bfalse{decide_bfalse_compseq_tag_def:o}(v11.g[v11]; v21.f[v21]),
atom: Atom,
pCom: pCom(P.M[P]),
squash: 
T,
component: component(P.M[P])
Lemmas :
true_wf,
squash_wf,
int_seg_properties,
subtype_rel-ldag,
pCom_wf,
product_subtype_base,
int_subtype_base,
atom2_subtype_base,
lg-label_wf_dag,
bnot_wf,
bool_cases,
eqtt_to_assert,
subtype_base_sq,
bool_subtype_base,
iff_weakening_uiff,
eqff_to_assert,
not_wf,
uiff_transitivity,
assert_of_bnot,
assert_wf,
not_functionality_wrt_uiff,
assert_of_eq_int,
eq_int_wf,
bool_wf,
pi1_wf_top,
run-info_wf,
pi1_wf,
run-event-step_wf,
lg-size_wf,
pRunType_wf,
subtype_rel_wf,
fulpRunType_wf,
member_wf,
pRun_wf,
pEnvType_wf,
System_wf,
pMsg_wf,
Id_wf,
nat_wf,
strong-type-continuous_wf,
pInTransit_wf,
ldag_wf,
top_wf,
unit_wf,
subtype_rel_function,
subtype_rel_self,
subtype_rel_simple_product,
run-initialization_wf,
runEvents_wf,
labeled-graph_wf,
pRun-invariant1
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[l2m:Id {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[S0:System(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])].
\mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))]
((fst(fst(run-info(pRun(S0;env;n2m;l2m);e)))) < run-event-step(e))
supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_40_10
Last ObjectModification:
2011_06_18-AM-11_20_40
Home
Index