Nuprl Definition : retrace
retrace(es;Q;X) ==
(∀e,e':E. ((Q e e') ⇒ ((↑e ∈b X) ∧ (↑e' ∈b X))))
∧ (∀e,e':E(X). ((Q e e') ∨ (e = e' ∈ E) ∨ (Q e' e)))
∧ (∀e':E. ∃L:E List. ((∀e:E. ((e ∈ L) ⇐⇒ Q e e')) ∧ (∀e1,e2:E. (e1 before e2 ∈ L ⇒ (Q e1 e2)))))
Definitions occuring in Statement :
es-E-interface: E(X),
in-eclass: e ∈b X,
es-E: E,
l_before: x before y ∈ l,
l_member: (x ∈ l),
list: T List,
assert: ↑b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
retrace
Latex:
retrace(es;Q;X) ==
(\mforall{}e,e':E. ((Q e e') {}\mRightarrow{} ((\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (\muparrow{}e' \mmember{}\msubb{} X))))
\mwedge{} (\mforall{}e,e':E(X). ((Q e e') \mvee{} (e = e') \mvee{} (Q e' e)))
\mwedge{} (\mforall{}e':E
\mexists{}L:E List. ((\mforall{}e:E. ((e \mmember{} L) \mLeftarrow{}{}\mRightarrow{} Q e e')) \mwedge{} (\mforall{}e1,e2:E. (e1 before e2 \mmember{} L {}\mRightarrow{} (Q e1 e2)))))
Date html generated:
2015_07_21-PM-04_18_10
Last ObjectModification:
2012_02_25-PM-03_10_12
Home
Index