Nuprl Definition : safety
safety(A;tr.P[tr]) == ∀tr1,tr2:A List. (tr1 ≤ tr2 ⇒ P[tr2] ⇒ P[tr1])
Definitions occuring in Statement :
iseg: 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,
iseg: l1 ≤ l2,
implies: P ⇒ Q
FDL editor aliases :
safety
Latex:
safety(A;tr.P[tr]) == \mforall{}tr1,tr2:A List. (tr1 \mleq{} tr2 {}\mRightarrow{} P[tr2] {}\mRightarrow{} P[tr1])
Date html generated:
2016_05_15-PM-01_54_55
Last ObjectModification:
2015_09_23-AM-07_37_27
Theory : list!
Home
Index