{ 
es:EO
[P:E 
]
d:e,e':E. Dec(es-p-immediate-pred(es;
e.P[e]) e e')
((e:E. Dec(P[e]))
SWellFounded(p-graph(E;es-r-pred{i:l}(es;d)) y x)) }
{ Proof }
Definitions occuring in Statement :
es-p-immediate-pred: es-p-immediate-pred(es;P),
es-r-pred: es-r-pred{i:l}(es;d),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
p-graph: p-graph(A;f),
strongwellfounded: SWellFounded(R[x; y])
Definitions :
subtype: S 
T,
suptype: suptype(S; T),
top: Top,
so_lambda: 
x.t[x],
axiom: Ax,
pair: <a, b>,
void: Void,
false: False,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
cand: A c
B,
assert: 
b,
rel_implies: R1 => R2,
record: record(x.T[x]),
strong-subtype: strong-subtype(A;B),
equal: s = t,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record-select: r.x,
infix_ap: x f y,
dep-isect: Error :dep-isect,
record+: record+,
le: A 
B,
ge: i 
j ,
not: 
A,
uimplies: b supposing a,
and: P Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
less_than: a < b,
es-r-pred: es-r-pred{i:l}(es;d),
p-graph: p-graph(A;f),
event_ordering: EO,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
universe: Type,
apply: f a,
exists: 
x:A. B[x],
product: x:A 
B[x],
nat: 
,
decidable: Dec(P),
or: P 
Q,
union: left + right,
strongwellfounded: SWellFounded(R[x; y]),
es-causl: (e < e'),
so_lambda: x y.t[x; y],
so_apply: x[s],
lambda: x.A[x],
es-p-immediate-pred: es-p-immediate-pred(es;P),
so_apply: x[s1;s2],
implies: P Q,
es-E: E,
all: x:A. B[x],
prop: ,
function: x:A B[x],
set: {x:A| B[x]} ,
member: t 
T,
guard: {T},
rev_implies: P 
Q,
iff: P Q,
causal-predecessor: causal-predecessor(es;p),
sq_type: SQType(T),
Auto: Error :Auto,
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
MaAuto: Error :MaAuto,
AssertBY: Error :AssertBY,
HypSubst: Error :HypSubst,
CollapseTHENA: Error :CollapseTHENA
Lemmas :
es-r-pred-property,
subtype_base_sq,
es-E_wf,
strongwf-monotone,
es-causl_wf,
p-graph_wf,
es-r-pred_wf,
es-p-immediate-pred_wf,
event_ordering_wf,
decidable_wf,
nat_wf,
strongwellfounded_wf,
p-graph_wf2,
rel_implies_wf,
assert_wf,
pair_wf,
assert_witness,
can-apply_wf,
top_wf,
member_wf,
do-apply_wf,
es-causl-swellfnd
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]
\mforall{}d:\mforall{}e,e':E. Dec(es-p-immediate-pred(es;\mlambda{}e.P[e]) e e')
((\mforall{}e:E. Dec(P[e])) {}\mRightarrow{} SWellFounded(p-graph(E;es-r-pred\{i:l\}(es;d)) y x))
Date html generated:
2011_08_16-AM-11_13_45
Last ObjectModification:
2011_06_20-AM-00_21_07
Home
Index