Nuprl Lemma : rep_int_constraint_step_wf

∀[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
  rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ}  
  supposing ∀p:IntConstraints
              (0 < dim(p)
              ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))


Proof



Definitions occuring in Statement :  rep_int_constraint_step: rep_int_constraint_step(f;p),  num-eq-constraints: num-eq-constraints(p),  int-problem-dimension: dim(p),  int-constraint-problem: IntConstraints,  less_than: a < b,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  prop: ℙ,  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  subtype_rel: A ⊆r B,  and: P ∧ Q,  nat: ℕ,  or: P ∨ Q,  so_apply: x[s],  all: ∀x:A. B[x],  false: False,  ge: i ≥ j ,  guard: {T},  decidable: Dec(P),  iff: P ⇐⇒ Q,  not: ¬A,  rev_implies: P ⇐ Q,  uiff: uiff(P;Q),  subtract: n - m,  top: Top,  le: A ≤ B,  less_than': less_than'(a;b),  true: True,  sq_stable: SqStable(P),  squash: ↓T,  exists: ∃x:A. B[x],  nat_plus: ℕ+,  less_than: a < b,  rep_int_constraint_step: rep_int_constraint_step(f;p),  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  bfalse: ff,  sq_type: SQType(T),  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  assert: ↑b,  int-constraint-problem: IntConstraints,  callbyvalueall: callbyvalueall,  has-value: (a)↓,  has-valueall: has-valueall(a)
Lemmas referenced :  all_wf,  int-constraint-problem_wf,  less_than_wf,  int-problem-dimension_wf,  or_wf,  equal_wf,  num-eq-constraints_wf,  nat_wf,  nat_properties,  less_than_transitivity1,  less_than_irreflexivity,  ge_wf,  decidable__le,  subtract_wf,  false_wf,  not-ge-2,  less-iff-le,  condition-implies-le,  minus-one-mul,  zero-add,  minus-one-mul-top,  minus-add,  minus-minus,  add-associates,  add-swap,  add-commutes,  add_functionality_wrt_le,  add-zero,  le-add-cancel,  add_nat_wf,  le_wf,  sq_stable__le,  decidable__lt,  not-lt-2,  add-mul-special,  zero-mul,  subtype_rel-equal,  base_wf,  le_weakening,  le_reflexive,  one-mul,  two-mul,  mul-distributes-right,  minus-zero,  omega-shadow,  lt_int_wf,  bool_wf,  eqtt_to_assert,  assert_of_lt_int,  top_wf,  eqff_to_assert,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  valueall-type-has-valueall,  union-valueall-type,  tunion_wf,  list_wf,  equal-wf-base-T,  unit_wf2,  tunion-valueall-type,  product-valueall-type,  list-valueall-type,  set-valueall-type,  int-valueall-type,  equal-valueall-type,  evalall-reduce,  list_subtype_base,  int_subtype_base,  less_than_transitivity2,  set_subtype_base,  equal-wf-T-base,  not-less-implies-equal
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  sqequalHypSubstitution,  hypothesis,  sqequalRule,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  extract_by_obid,  isectElimination,  thin,  lambdaEquality,  functionEquality,  natural_numberEquality,  hypothesisEquality,  applyEquality,  because_Cache,  functionExtensionality,  productEquality,  intEquality,  setElimination,  rename,  isect_memberEquality,  lambdaFormation,  intWeakElimination,  independent_isectElimination,  independent_functionElimination,  voidElimination,  dependent_functionElimination,  unionElimination,  independent_pairFormation,  productElimination,  addEquality,  minusEquality,  voidEquality,  dependent_set_memberEquality,  imageMemberEquality,  baseClosed,  imageElimination,  multiplyEquality,  dependent_pairFormation,  sqequalIntensionalEquality,  applyLambdaEquality,  promote_hyp,  addLevel,  levelHypothesis,  equalityElimination,  lessCases,  sqequalAxiom,  instantiate,  cumulativity,  setEquality,  baseApply,  closedConclusion,  callbyvalueReduce
Latex:
\mforall{}[f:IntConstraints  {}\mrightarrow{}  IntConstraints].  \mforall{}[p:IntConstraints].
    rep\_int\_constraint\_step(f;p)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}   
    supposing  \mforall{}p:IntConstraints
                            (0  <  dim(p)
                            {}\mRightarrow{}  (dim(f  p)  <  dim(p)
                                  \mvee{}  ((dim(f  p)  =  dim(p))  \mwedge{}  num-eq-constraints(f  p)  <  num-eq-constraints(p))))


Date html generated: 2017_04_14-AM-09_10_51
Last ObjectModification: 2017_02_27-PM-03_48_41

Theory : omega


Home Index