Nuprl Definition : add-cut-conditions
add-cut-conditions(c;e) ==
((¬((f e) = e ∈ E(X))) ⇒ f e ∈ c)
∧ ((↑e ∈b prior(X)) ⇒ prior(X)(e) ∈ c)
∧ ((¬e ∈ c) ∧ e ∈ c+e)
∧ (c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List))
∧ (c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List))
∧ ((↑e ∈b prior(X)) ⇒ (c(loc(e)) = ≤(X)(prior(X)(e)) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)))
∧ (∀i:Id. ((¬(i = loc(e) ∈ Id)) ⇒ (c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id} List))))
Definitions occuring in Statement :
es-cut-add: c+e,
es-cut-at: c(i),
es-prior-interface: prior(X),
es-interface-predecessors: ≤(X)(e),
es-E-interface: E(X),
eclass-val: X(e),
in-eclass: e ∈b X,
es-eq: es-eq(es),
es-loc: loc(e),
Id: Id,
fset-member: a ∈ s,
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
add-cut-conditions
Latex:
add-cut-conditions(c;e) ==
((\mneg{}((f e) = e)) {}\mRightarrow{} f e \mmember{} c)
\mwedge{} ((\muparrow{}e \mmember{}\msubb{} prior(X)) {}\mRightarrow{} prior(X)(e) \mmember{} c)
\mwedge{} ((\mneg{}e \mmember{} c) \mwedge{} e \mmember{} c+e)
\mwedge{} (c+e(loc(e)) = (c(loc(e)) @ [e]))
\mwedge{} (c+e(loc(e)) = \mleq{}(X)(e))
\mwedge{} ((\muparrow{}e \mmember{}\msubb{} prior(X)) {}\mRightarrow{} (c(loc(e)) = \mleq{}(X)(prior(X)(e))))
\mwedge{} (\mforall{}i:Id. ((\mneg{}(i = loc(e))) {}\mRightarrow{} (c+e(i) = c(i))))
Date html generated:
2015_07_21-PM-04_02_59
Last ObjectModification:
2012_02_25-PM-03_00_03
Home
Index