{ 
[M:Type 
Type]. [r:pRunType(P.M[P])].
well-founded-run-lt-witness() 
SWellFounded(x run-lt(r) y)
supposing e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e)) }
{ Proof }
Definitions occuring in Statement :
well-founded-run-lt-witness: well-founded-run-lt-witness(),
run-lt: run-lt(r),
run-event-step: run-event-step(e),
runEvents: runEvents(r),
run-info: run-info(r;e),
pRunType: pRunType(T.M[T]),
uimplies: b supposing a,
uall: [x:A]. B[x],
infix_ap: x f y,
so_apply: x[s],
pi1: fst(t),
all: x:A. B[x],
member: t T,
less_than: a < b,
function: x:A B[x],
universe: Type,
strongwellfounded: SWellFounded(R[x; y])
Definitions :
sq_type: SQType(T),
sqequal: s ~ t,
limited-type: LimitedType,
implies: P 
Q,
guard: {T},
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
assert: 
b,
natural_number: $n,
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,
and: P 
Q,
uiff: uiff(P;Q),
exists: 
x:A. B[x],
subtype_rel: A 
r B,
l_member: (x l),
prop: 
,
so_lambda: 
x y.t[x; y],
unit: Unit,
it: 
,
spread: spread def,
pair: <a, b>,
void: Void,
set: {x:A| B[x]} ,
real: 
,
grp_car: |g|,
nat: 
,
subtype: S T,
pMsg: pMsg(P.M[P]),
Id: Id,
top: Top,
product: x:A 
B[x],
int: 
,
so_apply: x[s],
universe: Type,
uall: [x:A]. B[x],
uimplies: b supposing a,
so_lambda: x.t[x],
isect: 
x:A. B[x],
well-founded-run-lt-witness: well-founded-run-lt-witness(),
function: x:A B[x],
equal: s = t,
pRunType: pRunType(T.M[T]),
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
Try: Error :Try,
Unfold: Error :Unfold,
well-founded-run-lt,
apply: f a,
run-lt: run-lt(r),
infix_ap: x f y,
runEvents: runEvents(r),
strongwellfounded: SWellFounded(R[x; y]),
member: t T,
AssertBY: Error :AssertBY,
axiom: Ax,
lambda: x.A[x],
run-event-step: run-event-step(e),
run-info: run-info(r;e),
pi1: fst(t),
less_than: a < b,
all: x:A. B[x]
Lemmas :
strongwellfounded_wf,
runEvents_wf,
run-lt_wf,
member_wf,
unit_wf,
pRunType_wf,
pMsg_wf,
top_wf,
Id_wf,
nat_wf,
run-event-step_wf,
run-info_wf,
pi1_wf_top,
subtype_rel_wf,
uall_wf,
well-founded-run-lt,
subtype_base_sq,
product_subtype_base,
isect_subtype_base,
it_wf,
unit_subtype_base
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])].
well-founded-run-lt-witness() \mmember{} SWellFounded(x run-lt(r) y)
supposing \mforall{}e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e))
Date html generated:
2011_08_17-PM-03_38_01
Last ObjectModification:
2011_06_18-AM-11_19_24
Home
Index