### Nuprl Lemma : l_before_l_index_le

`∀[T:Type]`
`  ∀dT:EqDecider(T). ∀L:T List. ∀x,y:T.`
`    ((x ∈ L) `` (y ∈ L) `` x before y ∈ L ∨ (x = y ∈ T) supposing index(L;x) ≤ index(L;y))`

Proof

Definitions occuring in Statement :  l_index: `index(L;x)` l_before: `x before y ∈ l` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` member: `t ∈ T` le: `A ≤ B` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` prop: `ℙ` squash: `↓T` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` cand: `A c∧ B` ge: `i ≥ j ` guard: `{T}` nat: `ℕ` lelt: `i ≤ j < k` true: `True` iff: `P `⇐⇒` Q`
Lemmas referenced :  le_witness_for_triv decidable__lt istype-le l_index_wf l_member_wf list_wf deq_wf istype-universe l_before_l_index l_before_wf select_wf squash_wf le_wf less_than_wf length_wf istype-int decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf intformless_wf intformle_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_le_lemma int_formula_prop_wf non_neg_length decidable__le length_wf_nat int_seg_properties nat_properties itermConstant_wf int_term_value_constant_lemma equal_wf true_wf select_l_index subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin productElimination equalityTransitivity hypothesis equalitySymmetry independent_isectElimination rename dependent_functionElimination because_Cache unionElimination hypothesisEquality applyEquality Error :lambdaEquality_alt,  setElimination Error :inhabitedIsType,  sqequalRule Error :universeIsType,  instantiate universeEquality Error :inlFormation_alt,  independent_functionElimination Error :equalityIstype,  Error :inrFormation_alt,  imageElimination productEquality natural_numberEquality approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation applyLambdaEquality imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type]
\mforall{}dT:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x,y:T.
((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  x  before  y  \mmember{}  L  \mvee{}  (x  =  y)  supposing  index(L;x)  \mleq{}  index(L;y))

Date html generated: 2019_06_20-PM-01_56_56
Last ObjectModification: 2019_01_13-PM-02_23_43

Theory : decidable!equality

Home Index