Nuprl Lemma : es-interval-one-one
∀[es:EO]. ∀[d,b,a,c:E].
({(a = c ∈ E) ∧ (b = d ∈ E)}) supposing (([a, b] = [c, d] ∈ (E List)) and c ≤loc d and a ≤loc b )
Proof
Definitions occuring in Statement :
es-interval: [e, e'],
es-le: e ≤loc e' ,
es-E: E,
event_ordering: EO,
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
equal_wf,
list_wf,
es-E_wf,
es-interval_wf,
es-le_wf,
event_ordering_wf,
hd-es-interval,
hd_wf,
pos_length,
es-locl_transitivity2,
es-locl_irreflexivity,
es-locl_wf,
es-interval-nil,
es-le-loc,
equal-wf-T-base,
not_wf,
ge_wf,
length_wf,
es-interval-length-one-one,
es-le_transitivity,
es-le_weakening_eq,
and_wf
\mforall{}[es:EO]. \mforall{}[d,b,a,c:E].
(\{(a = c) \mwedge{} (b = d)\}) supposing (([a, b] = [c, d]) and c \mleq{}loc d and a \mleq{}loc b )
Date html generated:
2015_07_17-AM-08_42_27
Last ObjectModification:
2015_01_27-PM-02_41_16
Home
Index