Nuprl Definition : star-append
star-append(T;P;Q) == λL.∃LL:T List List. ∃L':T List. ((∀X∈LL.P X) ∧ (Q L') ∧ (L = (concat(LL) @ L') ∈ (T List)))
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
concat: concat(ll),
append: as @ bs,
list: T List,
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
l_all: (∀x∈L.P[x]),
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T,
list: T List,
append: as @ bs,
concat: concat(ll)
FDL editor aliases :
star-append
Latex:
star-append(T;P;Q) ==
\mlambda{}L.\mexists{}LL:T List List. \mexists{}L':T List. ((\mforall{}X\mmember{}LL.P X) \mwedge{} (Q L') \mwedge{} (L = (concat(LL) @ L')))
Date html generated:
2016_05_15-PM-04_27_03
Last ObjectModification:
2015_09_23-AM-07_48_37
Theory : general
Home
Index