Nuprl Definition : eo_axioms
eo_axioms(r) ==
(∀x,y:r."E". ((↓x r."<" y) ⇒ r."rank" x < r."rank" y))
∧ (∀e:r."E". ((r."loc" (r."pred" e)) = (r."loc" e) ∈ Id))
∧ (∀e:r."E". (¬↓e r."<" (r."pred" e)))
∧ (∀e,x:r."E".
((↓x r."<" e) ⇒ ((r."loc" x) = (r."loc" e) ∈ Id) ⇒ ((↓(r."pred" e) r."<" e) ∧ (¬↓(r."pred" e) r."<" x))))
∧ (∀x,y,z:r."E". ((↓x r."<" y) ⇒ (↓y r."<" z) ⇒ (↓x r."<" z)))
∧ (∀e1,e2:r."E".
(↓e1 r."<" e2 ⇐⇒ ↑(e1 r."locless" e2)) ∧ ((¬↓e1 r."<" e2) ⇒ (¬↓e2 r."<" e1) ⇒ (e1 = e2 ∈ r."E"))
supposing (r."loc" e1) = (r."loc" e2) ∈ Id)
Definitions occuring in Statement :
Id: Id,
assert: ↑b,
less_than: a < b,
uimplies: b supposing a,
infix_ap: x f y,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
token: "$token",
equal: s = t ∈ T,
record-select: r.x
FDL editor aliases :
eo_axioms
eo\_axioms(r) ==
(\mforall{}x,y:r."E". ((\mdownarrow{}x r."<" y) {}\mRightarrow{} r."rank" x < r."rank" y))
\mwedge{} (\mforall{}e:r."E". ((r."loc" (r."pred" e)) = (r."loc" e)))
\mwedge{} (\mforall{}e:r."E". (\mneg{}\mdownarrow{}e r."<" (r."pred" e)))
\mwedge{} (\mforall{}e,x:r."E".
((\mdownarrow{}x r."<" e)
{}\mRightarrow{} ((r."loc" x) = (r."loc" e))
{}\mRightarrow{} ((\mdownarrow{}(r."pred" e) r."<" e) \mwedge{} (\mneg{}\mdownarrow{}(r."pred" e) r."<" x))))
\mwedge{} (\mforall{}x,y,z:r."E". ((\mdownarrow{}x r."<" y) {}\mRightarrow{} (\mdownarrow{}y r."<" z) {}\mRightarrow{} (\mdownarrow{}x r."<" z)))
\mwedge{} (\mforall{}e1,e2:r."E".
(\mdownarrow{}e1 r."<" e2 \mLeftarrow{}{}\mRightarrow{} \muparrow{}(e1 r."locless" e2)) \mwedge{} ((\mneg{}\mdownarrow{}e1 r."<" e2) {}\mRightarrow{} (\mneg{}\mdownarrow{}e2 r."<" e1) {}\mRightarrow{} (e1 = e2))
supposing (r."loc" e1) = (r."loc" e2))
Date html generated:
2015_07_17-AM-08_33_51
Last ObjectModification:
2014_02_20-PM-10_35_16
Home
Index