{ 
es:EO
    
[T:Type]
      
e:E. 
f:{e':E| e' 
loc e }  
 (T + Top).
        (
isl(es-search-back(es;x.f[x];e)) 

 
e'
e.
isl(f[e'])) }
{ Proof }
Definitions occuring in Statement : 
existse-le:
e
e'.P[e], 
es-search-back: es-search-back(es;x.f[x];e), 
es-le: e 
loc e' , 
es-E: E, 
event_ordering: EO, 
isl: isl(x), 
assert:
b, 
uall:
[x:A]. B[x], 
top: Top, 
so_apply: x[s], 
all:
x:A. B[x], 
iff: P 

 Q, 
set: {x:A| B[x]} , 
function: x:A 
 B[x], 
union: left + right, 
universe: Type
Definitions : 
true: True, 
squash:
T, 
es-causl: (e < e'), 
apply: f a, 
limited-type: LimitedType, 
real:
, 
grp_car: |g|, 
subtype: S 
 T, 
minus: -n, 
add: n + m, 
subtract: n - m, 
void: Void, 
false: False, 
not:
A, 
natural_number: $n, 
prop:
, 
le: A 
 B, 
ge: i 
 j , 
int:
, 
less_than: a < b, 
nat:
, 
strongwellfounded: SWellFounded(R[x; y]), 
exists:
x:A. B[x], 
implies: P 
 Q, 
product: x:A 
 B[x], 
and: P 
 Q, 
isect:
x:A. B[x], 
uall:
[x:A]. B[x], 
all:
x:A. B[x], 
iff: P 

 Q, 
existse-le:
e
e'.P[e], 
so_lambda: 
x.t[x], 
assert:
b, 
union: left + right, 
top: Top, 
set: {x:A| B[x]} , 
es-le: e 
loc e' , 
es-E: E, 
universe: Type, 
function: x:A 
 B[x], 
equal: s = t, 
member: t 
 T, 
event_ordering: EO, 
Auto: Error :Auto, 
D: Error :D, 
CollapseTHENA: Error :CollapseTHENA, 
CollapseTHEN: Error :CollapseTHEN, 
tactic: Error :tactic, 
RepeatFor: Error :RepeatFor, 
lambda:
x.A[x], 
dep-isect: Error :dep-isect, 
eq_atom: x =a y, 
eq_atom: eq_atom$n(x;y), 
record+: record+, 
infix_ap: x f y, 
record-select: r.x, 
rev_implies: P 
 Q, 
isl: isl(x), 
so_apply: x[s], 
es-search-back: es-search-back(es;x.f[x];e), 
sqequal: s ~ t, 
MaAuto: Error :MaAuto, 
or: P 
 Q, 
es-locl: (e <loc e'), 
subtype_rel: A 
r B, 
uiff: uiff(P;Q), 
uimplies: b supposing a, 
ifthenelse: if b then t else f fi , 
decide: case b of inl(x) => s[x] | inr(y) => t[y], 
strong-subtype: strong-subtype(A;B), 
fpf: a:A fp-> B[a], 
guard: {T}, 
cand: A c
 B, 
axiom: Ax, 
inl: inl x , 
bool:
, 
l_member: (x 
 l), 
record: record(x.T[x]), 
sq_type: SQType(T), 
pair: <a, b>, 
unit: Unit, 
bnot: 
b, 
es-first: first(e), 
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_type: eq_type(T;T'), 
b-exists: (
i<n.P[i])_b, 
bl-exists: (
x
L.P[x])_b, 
bl-all: (
x
L.P[x])_b, 
dcdr-to-bool: [d]
, 
grp_blt: a <
 b, 
set_blt: a <
 b, 
null: null(as), 
eq_int: (i =
 j), 
le_int: i 
z j, 
lt_int: i <z j, 
eq_bool: p =b q, 
btrue: tt, 
inr: inr x , 
bfalse: ff, 
Id: Id, 
es-loc: loc(e), 
es-pred: pred(e), 
outl: outl(x), 
fpf-dom: x 
 dom(f), 
eq_knd: a = b, 
es-causle: e c
 e', 
suptype: suptype(S; T), 
fpf-cap: f(x)?z, 
list: type List, 
intensional-universe: IType, 
es-init: es-init(es;e), 
Repeat: Error :Repeat, 
Try: Error :Try, 
Complete: Error :Complete
Lemmas : 
es-le-iff, 
es-locl_transitivity2, 
es-le-pred, 
es-causle-le, 
unit_wf, 
btrue_wf, 
intensional-universe_wf, 
es-le_weakening, 
es-locl_transitivity1, 
es-pred-locl, 
subtype_rel_self, 
subtype_rel_sets, 
subtype_rel_set, 
subtype_rel_function, 
es-pred-causl, 
assert-es-first, 
es-pred_wf, 
es-search-back_wf, 
es-loc_wf, 
Id_wf, 
eqtt_to_assert, 
iff_weakening_uiff, 
uiff_transitivity, 
eqff_to_assert, 
assert_of_bnot, 
not_wf, 
bnot_wf, 
es-first_wf, 
bfalse_wf, 
bool_wf, 
isect_subtype_base, 
union_subtype_base, 
subtype_base_sq, 
ifthenelse_wf, 
false_wf, 
assert_witness, 
isl_wf, 
rev_implies_wf, 
true_wf, 
subtype_rel_wf, 
es-locl_wf, 
es-search-back-cases, 
ge_wf, 
nat_wf, 
es-E_wf, 
es-le_wf, 
top_wf, 
iff_wf, 
assert_wf, 
existse-le_wf, 
nat_properties, 
es-causl-swellfnd, 
uall_wf, 
event_ordering_wf, 
le_wf, 
member_wf, 
es-causl_wf
\mforall{}es:EO
    \mforall{}[T:Type]
        \mforall{}e:E.  \mforall{}f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top).
            (\muparrow{}isl(es-search-back(es;x.f[x];e))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}isl(f[e']))
Date html generated:
2011_08_16-AM-10_49_23
Last ObjectModification:
2011_06_18-AM-09_23_32
Home
Index