{ 
es:EO. e:E. i:Id. (loc-on-path(es;i;[e]) 
loc(e) = i) }
{ Proof }
Definitions occuring in Statement :
loc-on-path: loc-on-path(es;i;L),
es-loc: loc(e),
es-E: E,
event_ordering: EO,
Id: Id,
all: x:A. B[x],
iff: P Q,
cons: [car / cdr],
nil: [],
equal: s = t
Definitions :
atom_eq: atomeqn def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
sq_type: SQType(T),
sqequal: s ~ t,
append: as @ bs,
locl: locl(a),
Knd: Knd,
es-locl: (e <loc e'),
es-first: first(e),
null: null(as),
void: Void,
false: False,
lsrc: source(l),
ldst: destination(l),
es-init: es-init(es;e),
bool: 
,
atom: Atom,
top: Top,
token: "$token",
ifthenelse: if b then t else f fi ,
record: record(x.T[x]),
cand: A c
B,
nat: 
,
exists: 
x:A. B[x],
rationals: 
,
apply: f a,
so_apply: x[s],
int: 
,
guard: {T},
l_member: (x 
l),
pair: <a, b>,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
universe: Type,
limited-type: LimitedType,
prop: 
,
list: type List,
nil: [],
cons: [car / cdr],
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
infix_ap: x f y,
set: {x:A| B[x]} ,
assert: 
b,
record-select: r.x,
atom: Atom$n,
rev_implies: P Q,
union: left + right,
or: P 
Q,
implies: P Q,
es-loc: loc(e),
loc-on-path: loc-on-path(es;i;L),
iff: P Q,
and: P Q,
product: x:A 
B[x],
Id: Id,
es-E: E,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
event_ordering: EO,
all: x:A. B[x],
function: x:A 
B[x],
member: t T,
equal: s = t,
MaAuto: Error :MaAuto,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
CollapseTHENA: Error :CollapseTHENA
Lemmas :
loc-on-path-nil,
loc-on-path_wf,
Id_wf,
rev_implies_wf,
iff_wf,
es-E_wf,
es-loc_wf,
loc-on-path-cons,
iff_functionality_wrt_iff,
event_ordering_wf,
uiff_inversion,
subtype_rel_self,
bool_wf,
not_wf,
nat_wf,
l_member_wf,
es-loc-pred,
assert_wf,
false_wf,
assert-eq-id,
subtype_base_sq
\mforall{}es:EO. \mforall{}e:E. \mforall{}i:Id. (loc-on-path(es;i;[e]) \mLeftarrow{}{}\mRightarrow{} loc(e) = i)
Date html generated:
2011_08_16-AM-10_55_07
Last ObjectModification:
2011_06_18-AM-09_28_14
Home
Index