Nuprl Lemma : split-at-first-gap-ext

∀[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 :  member: t ∈ T,  split-at-first-gap,  split-at-first-rel,  list_induction,  nil: [],  it: ⋅,  list-cases,  uall: ∀[x:A]. B[x],  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_apply: x[s1;s2;s3;s4],  so_lambda: λ2x.t[x],  top: Top,  so_apply: x[s],  uimplies: b supposing a,  strict4: strict4(F),  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  has-value: (a)↓,  prop: ℙ,  guard: {T},  or: P ∨ Q,  squash: ↓T,  colist-cases,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  colist-ext,  btrue: tt,  cons: [a / b],  bfalse: ff,  decidable__int_equal
Lemmas referenced :  split-at-first-gap,  lifting-strict-decide,  top_wf,  equal_wf,  has-value_wf_base,  base_wf,  is-exception_wf,  lifting-strict-spread,  lifting-strict-isaxiom,  lifting-strict-int_eq,  split-at-first-rel,  list_induction,  list-cases,  colist-cases,  colist-ext,  decidable__int_equal
Rules used in proof :  introduction,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  cut,  instantiate,  extract_by_obid,  hypothesis,  sqequalRule,  thin,  sqequalHypSubstitution,  isectElimination,  baseClosed,  isect_memberEquality,  voidElimination,  voidEquality,  independent_isectElimination,  independent_pairFormation,  lambdaFormation,  callbyvalueDecide,  hypothesisEquality,  equalityTransitivity,  equalitySymmetry,  unionEquality,  unionElimination,  sqleReflexivity,  dependent_functionElimination,  independent_functionElimination,  baseApply,  closedConclusion,  decideExceptionCases,  inrFormation,  because_Cache,  imageMemberEquality,  imageElimination,  exceptionSqequal,  inlFormation,  callbyvalueApply,  applyExceptionCases
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: 2018_05_21-PM-07_40_30
Last ObjectModification: 2017_07_26-PM-05_14_36

Theory : general


Home Index