Nuprl Definition : is_list_splitting
is_list_splitting(T;L;LL;L2;f) ==
(L = (concat(LL) @ L2) ∈ (T List))
∧ (∀L'∈LL.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
∧ ((¬↑null(L)) ⇒ (¬↑null(L2)))
∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L2 ⇒ (¬(S = L2 ∈ (T List))) ⇒ (¬↑(f S))))
Definitions occuring in Statement :
iseg: l1 ≤ l2,
l_all: (∀x∈L.P[x]),
null: null(as),
concat: concat(ll),
append: as @ bs,
list: T List,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
append: as @ bs,
concat: concat(ll),
l_all: (∀x∈L.P[x]),
and: P ∧ Q,
all: ∀x:A. B[x],
null: null(as),
iseg: l1 ≤ l2,
implies: P ⇒ Q,
equal: s = t ∈ T,
list: T List,
not: ¬A,
assert: ↑b,
apply: f a
FDL editor aliases :
is_list_splitting
Latex:
is\_list\_splitting(T;L;LL;L2;f) ==
(L = (concat(LL) @ L2))
\mwedge{} (\mforall{}L'\mmember{}LL.(\muparrow{}(f L'))
\mwedge{} (\mneg{}\muparrow{}null(L'))
\mwedge{} (\mforall{}S:T List. ((\mneg{}\muparrow{}null(S)) {}\mRightarrow{} S \mleq{} L' {}\mRightarrow{} (\mneg{}(S = L')) {}\mRightarrow{} (\mneg{}\muparrow{}(f S)))))
\mwedge{} ((\mneg{}\muparrow{}null(L)) {}\mRightarrow{} (\mneg{}\muparrow{}null(L2)))
\mwedge{} (\mforall{}S:T List. ((\mneg{}\muparrow{}null(S)) {}\mRightarrow{} S \mleq{} L2 {}\mRightarrow{} (\mneg{}(S = L2)) {}\mRightarrow{} (\mneg{}\muparrow{}(f S))))
Date html generated:
2016_05_15-PM-05_51_03
Last ObjectModification:
2015_09_23-AM-07_59_36
Theory : general
Home
Index