Nuprl Lemma : list_extensionality_iff

[T:Type]. ∀[a,b:T List].  (a b ∈ (T List) ⇐⇒ (||a|| ||b|| ∈ ℤ) ∧ (∀i:ℕ||a||. (a[i] b[i] ∈ T)))


Proof




Definitions occuring in Statement :  select: L[n] length: ||as|| list: List int_seg: {i..j-} uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T squash: T true: True all: x:A. B[x] prop: rev_implies:  Q so_lambda: λ2x.t[x] int_seg: {i..j-} uimplies: supposing a guard: {T} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top so_apply: x[s] less_than: a < b nat: le: A ≤ B ge: i ≥  subtype_rel: A ⊆B
Lemmas referenced :  length_wf int_seg_wf equal_wf list_wf all_wf select_wf int_seg_properties 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 int_formula_prop_less_lemma intformeq_wf int_formula_prop_eq_lemma less_than_wf list_extensionality squash_wf true_wf lelt_wf nat_properties iff_weakening_equal nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation lambdaFormation cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination because_Cache hypothesis hypothesisEquality equalitySymmetry natural_numberEquality sqequalRule imageMemberEquality baseClosed cumulativity productElimination productEquality setElimination rename independent_isectElimination equalityTransitivity dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll universeEquality dependent_set_memberEquality hyp_replacement applyLambdaEquality independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:T  List].    (a  =  b  \mLeftarrow{}{}\mRightarrow{}  (||a||  =  ||b||)  \mwedge{}  (\mforall{}i:\mBbbN{}||a||.  (a[i]  =  b[i])))



Date html generated: 2017_04_14-AM-09_24_54
Last ObjectModification: 2017_02_27-PM-03_59_23

Theory : list_1


Home Index