Nuprl Definition : ts-refinement
ts-refinement(ts1;ts2;f) ==
(ts-init(ts1) (ts-rel(ts1)^*) (f ts-init(ts2)))
∧ (∀x,y:ts-reachable(ts2). ((x ts-rel(ts2) y) ⇒ ((f x) (ts-rel(ts1)^*) (f y))))
∧ (∀x:ts-reachable(ts1)
((ts-final(ts1) x) ⇒ (∃y:ts-reachable(ts2). ((ts-final(ts2) y) ∧ ((f y) = x ∈ ts-type(ts1))))))
Definitions occuring in Statement :
ts-final: ts-final(ts),
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts),
ts-init: ts-init(ts),
ts-type: ts-type(ts),
rel_star: R^*,
infix_ap: x f y,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
ts-init: ts-init(ts),
infix_ap: x f y,
rel_star: R^*,
ts-rel: ts-rel(ts),
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
ts-reachable: ts-reachable(ts),
and: P ∧ Q,
ts-final: ts-final(ts),
equal: s = t ∈ T,
ts-type: ts-type(ts),
apply: f a
FDL editor aliases :
ts-refinement
Latex:
ts-refinement(ts1;ts2;f) ==
(ts-init(ts1) rel\_star(ts-type(ts1); ts-rel(ts1)) (f ts-init(ts2)))
\mwedge{} (\mforall{}x,y:ts-reachable(ts2).
((x ts-rel(ts2) y) {}\mRightarrow{} ((f x) (ts-rel(ts1)\^{}*) (f y))))
\mwedge{} (\mforall{}x:ts-reachable(ts1)
((ts-final(ts1) x) {}\mRightarrow{} (\mexists{}y:ts-reachable(ts2). ((ts-final(ts2) y) \mwedge{} ((f y) = x)))))
Date html generated:
2016_05_15-PM-05_39_53
Last ObjectModification:
2015_09_23-AM-07_57_56
Theory : general
Home
Index