Nuprl Definition : dl-sem
dl-sem(K;n.R[n];m.P[m]) ==
dl-ind(
dl-aprog(n)⇒ R[n];
dl-comp(alpha,beta)⇒ r1,r2.λk1,k3. ∃k2:K. ((r1 k1 k2) ∧ (r2 k2 k3));
dl-choose(alpha,beta)⇒ r1,r2.λk1,k2. ((r1 k1 k2) ∨ (r2 k1 k2));
dl-iterate(alpha)⇒ r.r^*;
dl-test(phi)⇒ p.λk1,k2. ((p k1) ∧ (k2 = k1 ∈ K));
dl-aprop(m)⇒ P[m];
dl-false⇒ λk.False;
dl-implies(phi,psi)⇒ p,q.λk.((p k) ⇒ (q k));
dl-and(phi,psi)⇒ p,q.λk.((p k) ∧ (q k));
dl-or(phi,psi)⇒ p,q.λk.((p k) ∨ (q k));
dl-box(alpha,phi)⇒ r,p.λk.∀k':K. ((r k k') ⇒ (p k'));
dl-diamond(alpha,phi)⇒ r,p.λk.∃k':K. ((r k k') ∧ (p k')))
Definitions occuring in Statement :
dl-ind: dl-ind,
rel_star: R^*,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
false: False,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
dl-ind: dl-ind,
rel_star: R^*,
equal: s = t ∈ T,
false: False,
or: P ∨ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
lambda: λx.A[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a
FDL editor aliases :
dl-sem
Latex:
dl-sem(K;n.R[n];m.P[m]) ==
dl-ind(
dl-aprog(n){}\mRightarrow{} R[n];
dl-comp(alpha,beta){}\mRightarrow{} r1,r2.\mlambda{}k1,k3. \mexists{}k2:K. ((r1 k1 k2) \mwedge{} (r2 k2 k3));
dl-choose(alpha,beta){}\mRightarrow{} r1,r2.\mlambda{}k1,k2. ((r1 k1 k2) \mvee{} (r2 k1 k2));
dl-iterate(alpha){}\mRightarrow{} r.rel\_star(K; r);
dl-test(phi){}\mRightarrow{} p.\mlambda{}k1,k2. ((p k1) \mwedge{} (k2 = k1));
dl-aprop(m){}\mRightarrow{} P[m];
dl-false{}\mRightarrow{} \mlambda{}k.False;
dl-implies(phi,psi){}\mRightarrow{} p,q.\mlambda{}k.((p k) {}\mRightarrow{} (q k));
dl-and(phi,psi){}\mRightarrow{} p,q.\mlambda{}k.((p k) \mwedge{} (q k));
dl-or(phi,psi){}\mRightarrow{} p,q.\mlambda{}k.((p k) \mvee{} (q k));
dl-box(alpha,phi){}\mRightarrow{} r,p.\mlambda{}k.\mforall{}k':K. ((r k k') {}\mRightarrow{} (p k'));
dl-diamond(alpha,phi){}\mRightarrow{} r,p.\mlambda{}k.\mexists{}k':K. ((r k k') \mwedge{} (p k')))
Date html generated:
2019_10_15-AM-11_43_31
Last ObjectModification:
2019_03_26-AM-11_28_10
Theory : dynamic!logic
Home
Index