Nuprl Definition : is_accum_splitting
is_accum_splitting(T;A;L;LL;L2;f;g;x) ==
(L = (concat(map(λp.(fst(p));LL)) @ (fst(L2))) ∈ (T List))
∧ (∀L'∈LL.(↑(f L'))
∧ (¬↑null(fst(L')))
∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
∧ ((¬↑null(L)) ⇒ (¬↑null(fst(L2))))
∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L2) ⇒ (¬(S = (fst(L2)) ∈ (T List))) ⇒ (¬↑(f <S, snd(L2)>))))
∧ ((snd(hd(LL @ [L2]))) = x ∈ A)
∧ (∀i:ℕ||LL||. ((snd(LL @ [L2][i + 1])) = (g LL[i]) ∈ A))
Definitions occuring in Statement :
iseg: l1 ≤ l2,
l_all: (∀x∈L.P[x]),
select: L[n],
hd: hd(l),
length: ||as||,
null: null(as),
concat: concat(ll),
map: map(f;as),
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
int_seg: {i..j-},
assert: ↑b,
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
concat: concat(ll),
map: map(f;as),
lambda: λx.A[x],
l_all: (∀x∈L.P[x]),
null: null(as),
iseg: l1 ≤ l2,
implies: P ⇒ Q,
list: T List,
pi1: fst(t),
not: ¬A,
assert: ↑b,
pair: <a, b>,
and: P ∧ Q,
hd: hd(l),
all: ∀x:A. B[x],
int_seg: {i..j-},
length: ||as||,
equal: s = t ∈ T,
pi2: snd(t),
add: n + m,
natural_number: $n,
append: as @ bs,
cons: [a / b],
nil: [],
apply: f a,
select: L[n]
FDL editor aliases :
is_accum_splitting
Latex:
is\_accum\_splitting(T;A;L;LL;L2;f;g;x) ==
(L = (concat(map(\mlambda{}p.(fst(p));LL)) @ (fst(L2))))
\mwedge{} (\mforall{}L'\mmember{}LL.(\muparrow{}(f L'))
\mwedge{} (\mneg{}\muparrow{}null(fst(L')))
\mwedge{} (\mforall{}S:T List. ((\mneg{}\muparrow{}null(S)) {}\mRightarrow{} S \mleq{} fst(L') {}\mRightarrow{} (\mneg{}(S = (fst(L')))) {}\mRightarrow{} (\mneg{}\muparrow{}(f <S, snd(L')>)))))
\mwedge{} ((\mneg{}\muparrow{}null(L)) {}\mRightarrow{} (\mneg{}\muparrow{}null(fst(L2))))
\mwedge{} (\mforall{}S:T List. ((\mneg{}\muparrow{}null(S)) {}\mRightarrow{} S \mleq{} fst(L2) {}\mRightarrow{} (\mneg{}(S = (fst(L2)))) {}\mRightarrow{} (\mneg{}\muparrow{}(f <S, snd(L2)>))))
\mwedge{} ((snd(hd(LL @ [L2]))) = x)
\mwedge{} (\mforall{}i:\mBbbN{}||LL||. ((snd(LL @ [L2][i + 1])) = (g LL[i])))
Date html generated:
2016_05_15-PM-05_53_18
Last ObjectModification:
2015_09_23-AM-07_59_55
Theory : general
Home
Index