Nuprl Definition : strict2

strict2(F) ==
  (∀x,y:Base.  ((F y)↓  (x)↓))
  ∧ (∀y,u,v:Base.  (F (exception(u; v)) exception(u; v)))
  ∧ (∀x,y:Base.  (is-exception(F y)  (↓(x)↓ ∨ is-exception(x))))



Definitions occuring in Statement :  has-value: (a)↓ is-exception: is-exception(t) all: x:A. B[x] squash: T implies:  Q or: P ∨ Q and: P ∧ Q apply: a base: Base sqequal: t
Definitions occuring in definition :  and: P ∧ Q sqequal: t all: x:A. B[x] base: Base implies:  Q apply: a squash: T or: P ∨ Q has-value: (a)↓ is-exception: is-exception(t)
FDL editor aliases :  strict2

Latex:
strict2(F)  ==
    (\mforall{}x,y:Base.    ((F  x  y)\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{}))
    \mwedge{}  (\mforall{}y,u,v:Base.    (F  (exception(u;  v))  y  \msim{}  exception(u;  v)))
    \mwedge{}  (\mforall{}x,y:Base.    (is-exception(F  x  y)  {}\mRightarrow{}  (\mdownarrow{}(x)\mdownarrow{}  \mvee{}  is-exception(x))))



Date html generated: 2016_05_13-PM-03_23_41
Last ObjectModification: 2015_09_22-PM-05_44_39

Theory : call!by!value_1


Home Index