{ 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: ee'.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: ee'.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: (xL.P[x])_b bl-all: (xL.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