### Nuprl Lemma : iseg-iff-firstn

[T:Type]. ∀L1,L2:T List.  (L1 ≤ L2 ⇐⇒ (||L1|| ≤ ||L2||) ∧ (L1 firstn(||L1||;L2) ∈ (T List)))

Proof

Definitions occuring in Statement :  iseg: l1 ≤ l2 firstn: firstn(n;as) length: ||as|| list: List uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T exists: x:A. B[x] le: A ≤ B not: ¬A false: False prop: so_lambda: λ2x.t[x] int_seg: {i..j-} so_apply: x[s] rev_implies:  Q lelt: i ≤ j < k ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top squash: T subtype_rel: A ⊆B int_iseg: {i...j} guard: {T} less_than: a < b uiff: uiff(P;Q) true: True sq_type: SQType(T)
Lemmas referenced :  less_than'_wf length_wf exists_wf int_seg_wf equal_wf list_wf firstn_wf non_neg_length decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma lelt_wf le_wf firstn_is_iseg iseg_wf iff_wf squash_wf true_wf length_firstn_eq subtype_rel_sets int_seg_properties add-is-int-iff false_wf iff_weakening_equal subtype_base_sq int_subtype_base length_firstn
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation introduction sqequalHypSubstitution productElimination thin sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination extract_by_obid isectElimination cumulativity hypothesis axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality addEquality setElimination rename dependent_pairFormation dependent_set_memberEquality because_Cache unionElimination independent_isectElimination int_eqEquality intEquality isect_memberEquality voidEquality computeAll productEquality addLevel impliesFunctionality independent_functionElimination universeEquality applyEquality imageElimination setEquality applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed imageMemberEquality hyp_replacement instantiate

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    (L1  \mleq{}  L2  \mLeftarrow{}{}\mRightarrow{}  (||L1||  \mleq{}  ||L2||)  \mwedge{}  (L1  =  firstn(||L1||;L2)))

Date html generated: 2017_04_17-AM-07_31_22
Last ObjectModification: 2017_02_27-PM-04_08_34

Theory : list_1

Home Index