dfp-meaning-in-state(dfp;x) ==
case x
of inl(s) =>
df-program-meaning(df-program-in-state(dfp;s))
| inr(z) =>
null-dataflow()
Definitions occuring in Statement :
df-program-in-state: df-program-in-state(dfp;s),
df-program-meaning: df-program-meaning(dfp),
null-dataflow: null-dataflow(),
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
df-program-meaning: df-program-meaning(dfp),
df-program-in-state: df-program-in-state(dfp;s)
FDL editor aliases :
dfp-meaning-in-state
dfp-meaning-in-state(dfp;x) ==
case x of inl(s) => df-program-meaning(df-program-in-state(dfp;s)) | inr(z) => null-dataflow()
Date html generated:
2011_08_16-AM-09_35_42
Last ObjectModification:
2011_06_07-PM-03_09_01
Home
Index