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
Definitions unfolded in proof :
so_lambda: λ2x y.t[x; y],
sys-antecedent: sys-antecedent(es;Sys),
so_apply: x[s],
so_apply: x[s1;s2],
es-E-interface: E(X),
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
prop: ℙ,
member: t ∈ T,
uimplies: b supposing a,
implies: P ⇒ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
guard: {T},
or: P ∨ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
refl: Refl(T;x,y.E[x; y]),
false: False,
label: ...$L... t,
not: ¬A,
trans: Trans(T;x,y.E[x; y])
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:
2016_05_17-AM-07_46_23
Last ObjectModification:
2015_12_28-PM-11_36_38
Theory : event-ordering
Home
Index