Nuprl Definition : strong_safety
strong_safety(T;tr.P[tr]) == ∀tr1,tr2:T List. (tr1 ⊆ tr2 ⇒ P[tr2] ⇒ P[tr1])
Definitions occuring in Statement :
sublist: L1 ⊆ L2,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
list: T List,
sublist: L1 ⊆ L2,
implies: P ⇒ Q
FDL editor aliases :
strong_safety
Latex:
strong\_safety(T;tr.P[tr]) == \mforall{}tr1,tr2:T List. (tr1 \msubseteq{} tr2 {}\mRightarrow{} P[tr2] {}\mRightarrow{} P[tr1])
Date html generated:
2016_05_15-PM-02_06_21
Last ObjectModification:
2015_09_23-AM-07_37_56
Theory : list!
Home
Index