Nuprl Lemma : cut-order-implies
∀[Info:Type]
∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X).
∀[R:E(X) ─→ E(X) ─→ ℙ]
(Refl(E(X);a,b.R[a;b])
⇒ Trans(E(X);a,b.R[a;b])
⇒ (∀b:E(X). R[f b;b] supposing ¬(loc(f b) = loc(b) ∈ Id))
⇒ (∀a,b:E(X). ((a <loc b) ⇒ R[a;b]))
⇒ (∀a,b:E(X). R[a;b] supposing a ≤(X;f) b))
Proof
Definitions occuring in Statement :
cut-order: a ≤(X;f) b,
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-loc: loc(e),
Id: Id,
trans: Trans(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
cut-order_witness,
cut-order_wf,
es-E-interface_wf,
all_wf,
es-locl_wf,
event-ordering+_subtype,
isect_wf,
not_wf,
equal_wf,
Id_wf,
es-loc_wf,
trans_wf,
refl_wf,
sys-antecedent_wf,
eclass_wf,
top_wf,
es-E_wf,
event-ordering+_wf,
cut-order-induction,
cut-order-iff,
and_wf,
cut-order-step,
es-causl_transitivity2,
es-causle_weakening_eq,
es-causle_wf,
es-causl_irreflexivity,
es-prior-interface-val,
eclass-val_wf2,
es-prior-interface_wf,
cut-order_weakening-le,
es-le_weakening,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:sys-antecedent(es;X).
\mforall{}[R:E(X) {}\mrightarrow{} E(X) {}\mrightarrow{} \mBbbP{}]
(Refl(E(X);a,b.R[a;b])
{}\mRightarrow{} Trans(E(X);a,b.R[a;b])
{}\mRightarrow{} (\mforall{}b:E(X). R[f b;b] supposing \mneg{}(loc(f b) = loc(b)))
{}\mRightarrow{} (\mforall{}a,b:E(X). ((a <loc b) {}\mRightarrow{} R[a;b]))
{}\mRightarrow{} (\mforall{}a,b:E(X). R[a;b] supposing a \mleq{}(X;f) b))
Date html generated:
2015_07_21-PM-04_06_28
Last ObjectModification:
2015_01_27-PM-05_49_18
Home
Index