Nuprl Lemma : exact-reduce-constraints_wf

[w:ℤ List]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| ||w|| ∈ ℤ}  List].
  (exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| (||w|| 1) ∈ ℤ}  List)


Proof




Definitions occuring in Statement :  exact-reduce-constraints: exact-reduce-constraints(w;j;L) length: ||as|| list: List int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T exact-reduce-constraints: exact-reduce-constraints(w;j;L) subtype_rel: A ⊆B uimplies: supposing a prop: all: x:A. B[x] implies:  Q int_seg: {i..j-} sq_stable: SqStable(P) lelt: i ≤ j < k and: P ∧ Q squash: T guard: {T} le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A true: True iff: ⇐⇒ Q rev_implies:  Q sq_type: SQType(T) top: Top so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  list_wf equal-wf-base list_subtype_base int_subtype_base int_seg_wf length_wf map_wf equal_wf int-vec-add_wf int-vec-mul_wf select_wf sq_stable__le less_than_transitivity1 le_weakening list-delete_wf squash_wf true_wf length-int-vec-add length-list-delete int_seg_subtype_nat false_wf subtract_wf iff_weakening_equal subtype_base_sq length-int-vec-mul list-valueall-type set-valueall-type int-valueall-type evalall-reduce
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination thin setEquality intEquality baseApply closedConclusion baseClosed hypothesisEquality applyEquality independent_isectElimination because_Cache isect_memberEquality natural_numberEquality lambdaEquality lambdaFormation setElimination rename dependent_functionElimination independent_functionElimination dependent_set_memberEquality minusEquality multiplyEquality productElimination imageMemberEquality imageElimination universeEquality equalityUniverse levelHypothesis independent_pairFormation instantiate cumulativity voidElimination voidEquality

Latex:
\mforall{}[w:\mBbbZ{}  List].  \mforall{}[j:\mBbbN{}||w||].  \mforall{}[L:\{l:\mBbbZ{}  List|  ||l||  =  ||w||\}    List].
    (exact-reduce-constraints(w;j;L)  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  (||w||  -  1)\}    List)



Date html generated: 2017_04_14-AM-09_05_05
Last ObjectModification: 2017_02_27-PM-03_44_47

Theory : omega


Home Index