Nuprl Lemma : split-at-first-gap
∀[T:Type]
∀f:T ⟶ ℤ. ∀L:T List.
(∃XY:{T List × (T List)| let X,Y = XY
in (L = (X @ Y) ∈ (T List))
∧ (∀i:ℕ||X|| - 1. ((f X[i + 1]) = ((f X[i]) + 1) ∈ ℤ))
∧ ((¬↑null(L))
⇒ ((¬↑null(X)) ∧ ¬((f hd(Y)) = ((f last(X)) + 1) ∈ ℤ) supposing ||Y|| ≥ 1 ))})
Proof
Definitions occuring in Statement :
last: last(L),
select: L[n],
hd: hd(l),
length: ||as||,
null: null(as),
append: as @ bs,
list: T List,
int_seg: {i..j-},
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
ge: i ≥ j ,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
implies: P ⇒ Q
Lemmas referenced :
split-at-first-rel,
equal_wf,
decidable__int_equal,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality,
intEquality,
applyEquality,
addEquality,
natural_numberEquality,
hypothesis,
independent_functionElimination,
dependent_functionElimination,
because_Cache,
functionEquality,
universeEquality
Latex:
\mforall{}[T:Type]
\mforall{}f:T {}\mrightarrow{} \mBbbZ{}. \mforall{}L:T List.
(\mexists{}XY:\{T List \mtimes{} (T List)| let X,Y = XY
in (L = (X @ Y))
\mwedge{} (\mforall{}i:\mBbbN{}||X|| - 1. ((f X[i + 1]) = ((f X[i]) + 1)))
\mwedge{} ((\mneg{}\muparrow{}null(L))
{}\mRightarrow{} ((\mneg{}\muparrow{}null(X))
\mwedge{} \mneg{}((f hd(Y)) = ((f last(X)) + 1)) supposing ||Y|| \mgeq{} 1 ))\})
Date html generated:
2016_05_15-PM-04_41_20
Last ObjectModification:
2015_12_27-PM-02_40_24
Theory : general
Home
Index