add-cut-conditions(c;e) ==
((
((f e) = e)) 
f e 
c)
((
e 
prior(X)) prior(X)(e) c)
((e c) e c+e)
(c+e(loc(e)) = (c(loc(e)) @ [e]))
(c+e(loc(e)) = 
(X)(e))
((e prior(X)) (c(loc(e)) = (X)(prior(X)(e))))
(
i:Id. (((i = loc(e))) (c+e(i) = c(i))))
Definitions :
apply: f a,
fset-member: a s,
es-eq: es-eq(es),
append: as @ bs,
cons: [car / cdr],
nil: [],
and: P Q,
assert: b,
in-eclass: e X,
es-interface-predecessors: (X)(e),
eclass-val: X(e),
es-prior-interface: prior(X),
all: x:A. B[x],
implies: P Q,
not: A,
list: type List,
set: {x:A| B[x]} ,
es-E-interface: E(X),
equal: s = t,
Id: Id,
es-loc: loc(e),
es-cut-add: c+e,
es-cut-at: c(i)
FDL editor aliases :
add-cut-conditions
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:
2010_08_27-PM-03_17_12
Last ObjectModification:
2010_04_01-PM-07_09_08
Home
Index