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