Nuprl Lemma : list_split_iseg2

[T:Type]
  ∀f:(T List) ⟶ 𝔹. ∀L1,L2:T List.
    (L1 ≤ L2
     (∀LL1,LL2:T List List. ∀X,Y:T List.
          (((LL1 LL2 ∈ (T List List)) ∧ X ≤ Y)
             ∨ (∃Z:T List. ∃ZZ:T List List. (((LL1 [Z ZZ]) LL2 ∈ (T List List)) ∧ X ≤ Z))) supposing 
             ((list_split(f;L2) = <LL2, Y> ∈ (T List List × (T List))) and 
             (list_split(f;L1) = <LL1, X> ∈ (T List List × (T List))))))


Proof




Definitions occuring in Statement :  list_split: list_split(f;L) iseg: l1 ≤ l2 append: as bs cons: [a b] list: List bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q function: x:A ⟶ B[x] pair: <a, b> product: x:A × B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q uimplies: supposing a prop: and: P ∧ Q so_lambda: λ2x.t[x] top: Top so_apply: x[s] exists: x:A. B[x] or: P ∨ Q guard: {T} iff: ⇐⇒ Q subtype_rel: A ⊆B
Lemmas referenced :  list_split_iseg or_wf equal_wf list_wf length_wf iseg_wf exists_wf append_wf cons_wf length-append iff_weakening_equal list_split_wf is_list_splitting_wf bool_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination independent_functionElimination axiomEquality rename spreadEquality equalityTransitivity equalitySymmetry productEquality cumulativity applyLambdaEquality sqequalRule lambdaEquality isect_memberEquality voidElimination voidEquality independent_isectElimination productElimination hyp_replacement because_Cache functionExtensionality applyEquality setElimination setEquality independent_pairEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type]
    \mforall{}f:(T  List)  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L1,L2:T  List.
        (L1  \mleq{}  L2
        {}\mRightarrow{}  (\mforall{}LL1,LL2:T  List  List.  \mforall{}X,Y:T  List.
                    (((LL1  =  LL2)  \mwedge{}  X  \mleq{}  Y)
                          \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((LL1  @  [Z  /  ZZ])  =  LL2)  \mwedge{}  X  \mleq{}  Z)))  supposing 
                          ((list\_split(f;L2)  =  <LL2,  Y>)  and 
                          (list\_split(f;L1)  =  <LL1,  X>))))



Date html generated: 2018_05_21-PM-08_05_26
Last ObjectModification: 2017_07_26-PM-05_41_24

Theory : general


Home Index