Nuprl Definition : state-machine-spec
state-machine-spec{i:l}(Info;es;C;R;F;I;O) ==
∃X:EClass(C)
∃Q:E ─→ E ─→ ℙ
∃B:retrace(es;Q;X)
(I:λe,e'. (e <loc e') →─λe.I(e)─→ X:Q
∧ X:Q →─λe.(F map(λe'.X(e');(retracer(B) e) @ [e]))─→ O:λe,e'. ((loc(e) = loc(e') ∈ Id) ⇒ (e <loc e')))
Definitions occuring in Statement :
retracer: retracer(p),
retrace: retrace(es;Q;X),
Q-R-glued: Ia:Qa →─f─→ Ib:Rb,
eclass-val: X(e),
eclass: EClass(A[eo; e]),
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
Id: Id,
map: map(f;as),
append: as @ bs,
cons: [a / b],
nil: [],
prop: ℙ,
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
equal: s = t ∈ T
FDL editor aliases :
state-machine-spec
Latex:
state-machine-spec\{i:l\}(Info;es;C;R;F;I;O) ==
\mexists{}X:EClass(C)
\mexists{}Q:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
\mexists{}B:retrace(es;Q;X)
(I:\mlambda{}e,e'. (e <loc e') \mrightarrow{}{}\mlambda{}e.I(e){}\mrightarrow{} X:Q
\mwedge{} X:Q \mrightarrow{}{}\mlambda{}e.(F map(\mlambda{}e'.X(e');(retracer(B) e) @ [e])){}\mrightarrow{} O:\mlambda{}e,e'. ((loc(e) = loc(e'))
{}\mRightarrow{} (e <loc e')))
Date html generated:
2015_07_21-PM-04_19_14
Last ObjectModification:
2012_02_25-PM-03_10_52
Home
Index