Nuprl Definition : strict5
strict5(F) ==
(∀x,y,z,w:Base. ((F x y z w)↓ ⇒ (x)↓))
∧ (∀u,v,y,z,w:Base. (F (exception(u; v)) y z w ~ exception(u; v)))
∧ (∀u,v,x,y,z,w:Base. ((F x y z w ~ exception(u; v)) ⇒ (↓(eval y = x in y ~ exception(u; v)) ∨ (x)↓)))
Definitions occuring in Statement :
has-value: (a)↓,
callbyvalue: callbyvalue,
all: ∀x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
base: Base,
sqequal: s ~ t
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
apply: f a,
squash: ↓T,
or: P ∨ Q,
sqequal: s ~ t,
callbyvalue: callbyvalue,
has-value: (a)↓
FDL editor aliases :
strict5
Latex:
strict5(F) ==
(\mforall{}x,y,z,w:Base. ((F x y z w)\mdownarrow{} {}\mRightarrow{} (x)\mdownarrow{}))
\mwedge{} (\mforall{}u,v,y,z,w:Base. (F (exception(u; v)) y z w \msim{} exception(u; v)))
\mwedge{} (\mforall{}u,v,x,y,z,w:Base.
((F x y z w \msim{} exception(u; v)) {}\mRightarrow{} (\mdownarrow{}(eval y = x in y \msim{} exception(u; v)) \mvee{} (x)\mdownarrow{})))
Date html generated:
2016_05_13-PM-03_23_54
Last ObjectModification:
2015_09_22-PM-05_44_42
Theory : call!by!value_1
Home
Index