### Nuprl Lemma : iseg_select

`∀[T:Type]. ∀l1,l2:T List.  (l1 ≤ l2 `⇐⇒` (||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[i] ∈ T supposing i < ||l1||))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` select: `L[n]` length: `||as||` list: `T List` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` cand: `A c∧ B` le: `A ≤ B` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` le: `A ≤ B` squash: `↓T` less_than: `a < b` and: `P ∧ Q` top: `Top` not: `¬A` implies: `P `` Q` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` nat: `ℕ` uimplies: `b supposing a` cand: `A c∧ B` prop: `ℙ` so_lambda: `λ2x.t[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` it: `⋅` nil: `[]` select: `L[n]` uiff: `uiff(P;Q)` iseg: `l1 ≤ l2` guard: `{T}` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` append: `as @ bs` sq_type: `SQType(T)` subtype_rel: `A ⊆r B` true: `True` less_than': `less_than'(a;b)` nat_plus: `ℕ+` cons: `[a / b]` subtract: `n - m`
Lemmas referenced :  int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties select_wf equal_wf less_than_wf isect_wf nat_wf length_wf le_wf iseg_wf iff_wf list_wf all_wf list_induction equal-wf-base-T nil_iseg nil_wf less_than'_wf non_neg_length base_wf stuck-spread length_of_nil_lemma false_wf int_term_value_add_lemma itermAdd_wf add-is-int-iff length_of_cons_lemma cons_wf equal-wf-T-base iseg_weakening length-append btrue_neq_bfalse bfalse_wf null_cons_lemma null_wf and_wf append_is_nil btrue_wf null_nil_lemma list_ind_cons_lemma length_wf_nat cons_iseg int_subtype_base subtype_base_sq decidable__equal_int iff_weakening_equal select_cons_hd true_wf squash_wf select_cons_tl int_term_value_subtract_lemma itermSubtract_wf subtract_wf int_formula_prop_eq_lemma intformeq_wf full-omega-unsat istype-int istype-void istype-le add_nat_plus istype-less_than nat_plus_properties istype-nat add-associates add-swap add-commutes zero-add istype-universe subtype_rel_self
Rules used in proof :  universeEquality independent_functionElimination productElimination imageElimination computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation unionElimination natural_numberEquality dependent_functionElimination independent_isectElimination rename setElimination productEquality because_Cache hypothesis cumulativity lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution equalitySymmetry equalityTransitivity axiomEquality independent_pairEquality baseClosed closedConclusion baseApply promote_hyp pointwiseFunctionality addEquality dependent_set_memberEquality applyLambdaEquality instantiate imageMemberEquality applyEquality Error :dependent_set_memberEquality_alt,  approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :isect_memberEquality_alt,  Error :universeIsType,  Error :inhabitedIsType,  Error :lambdaFormation_alt,  Error :equalityIstype,  Error :isect_memberFormation_alt

Latex:
\mforall{}[T:Type]
\mforall{}l1,l2:T  List.    (l1  \mleq{}  l2  \mLeftarrow{}{}\mRightarrow{}  (||l1||  \mleq{}  ||l2||)  c\mwedge{}  (\mforall{}i:\mBbbN{}.  l1[i]  =  l2[i]  supposing  i  <  ||l1||))

Date html generated: 2019_06_20-PM-01_28_45
Last ObjectModification: 2019_03_27-PM-01_24_20

Theory : list_1

Home Index